Adjoin one single element

This file contains basic results on Algebra.adjoin, specifically on adjoining singletons.

Tags

adjoin, algebra, ringhom

def Algebra.RingHom.adjoinAlgebraMap {A : Type u_1} {B : Type u_2} {C : Type u_3} [CommSemiring A] [CommSemiring B] [CommSemiring C] [Algebra A B] [Algebra B C] [Algebra A C] [IsScalarTower A B C] (b : B) : ↥A[b] →+* ↥A[(algebraMap B C) b]

Ring homomorphism between A[b] and A[↑b].

Equations

• Algebra.RingHom.adjoinAlgebraMap b = (↑((AlgHom.restrictScalars A (Algebra.ofId B C)).comp A[b].val)).codRestrict A[(algebraMap B C) b] ⋯

@[simp]

theorem Algebra.RingHom.adjoinAlgebraMap_apply {A : Type u_1} {B : Type u_2} {C : Type u_3} [CommSemiring A] [CommSemiring B] [CommSemiring C] [Algebra A B] [Algebra B C] [Algebra A C] [IsScalarTower A B C] (b : B) (x : ↥A[b]) : ↑((adjoinAlgebraMap b) x) = (algebraMap B C) ↑x

theorem Algebra.RingHom.adjoinAlgebraMap_surjective {A : Type u_1} {B : Type u_2} {C : Type u_3} [CommSemiring A] [CommSemiring B] [CommSemiring C] [Algebra A B] [Algebra B C] [Algebra A C] [IsScalarTower A B C] (b : B) : Function.Surjective ⇑(adjoinAlgebraMap b)

@[instance_reducible]

instance Algebra.instSubtypeMemSubalgebraAdjoinSingletonSetCoeRingHomAlgebraMap {A : Type u_1} {B : Type u_2} {C : Type u_3} [CommSemiring A] [CommSemiring B] [CommSemiring C] [Algebra A B] [Algebra B C] [Algebra A C] [IsScalarTower A B C] (b : B) : Algebra ↥A[b] ↥A[(algebraMap B C) b]

Equations

• Algebra.instSubtypeMemSubalgebraAdjoinSingletonSetCoeRingHomAlgebraMap b = (Algebra.RingHom.adjoinAlgebraMap b).toAlgebra

instance Algebra.instIsScalarTowerSubtypeMemSubalgebraAdjoinSingletonSetCoeRingHomAlgebraMap {A : Type u_1} {B : Type u_2} {C : Type u_3} [CommSemiring A] [CommSemiring B] [CommSemiring C] [Algebra A B] [Algebra B C] [Algebra A C] [IsScalarTower A B C] (b : B) : IsScalarTower (↥A[b]) (↥A[(algebraMap B C) b]) C

noncomputable def Algebra.RingHom.adjoinAlgebraMapEquiv {A : Type u_1} {B : Type u_2} {C : Type u_3} [CommSemiring A] [CommSemiring B] [CommSemiring C] [Algebra A B] [Algebra B C] [Algebra A C] [IsScalarTower A B C] (b : B) [FaithfulSMul B C] : ↥A[b] ≃+* ↥A[(algebraMap B C) b]

If the algebraMap injective then we have a Ring isomorphism between A[b] and A[↑b].

Equations

• Algebra.RingHom.adjoinAlgebraMapEquiv b = RingEquiv.ofBijective (Algebra.RingHom.adjoinAlgebraMap b) ⋯