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) : ↥(adjoin A {b}) →+* ↥(adjoin 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 (Algebra.adjoin A {b}).val)).codRestrict (Algebra.adjoin A {(algebraMap B C) b}) ⋯

@[simp]

theorem Algebra.RingHom.adjoin_algebraMap_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 : ↥(adjoin A {b})) : ↑((adjoinAlgebraMap b) x) = (algebraMap B C) ↑x

theorem Algebra.RingHom.adjoin_algebraMap_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 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 ↥(adjoin A {b}) ↥(adjoin 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 (↥(adjoin A {b})) (↥(adjoin 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] : ↥(adjoin A {b}) ≃+* ↥(adjoin 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) ⋯