Relating unital and non-unital substructures

This file relates various algebraic structures and provides maps (generally algebra homomorphisms), from the unitization of a non-unital subobject into the full structure. The range of this map is the unital closure of the non-unital subobject (e.g., Algebra.adjoin, Subring.closure, Subsemiring.closure or StarSubalgebra.adjoin). When the underlying scalar ring is a field, for this map to be injective it suffices that the range omits 1. In this setting we provide suitable AlgEquiv (or StarAlgEquiv) onto the range.

Main declarations

• NonUnitalSubalgebra.unitization s : Unitization R s →ₐ[R] A: where s is a non-unital subalgebra of a unital R-algebra A, this is the natural algebra homomorphism sending (r, a) to r • 1 + a. The range of this map is Algebra.adjoin R (s : Set A).
• NonUnitalSubalgebra.unitizationAlgEquiv s : Unitization R s ≃ₐ[R] Algebra.adjoin R (s : Set A) when R is a field and 1 ∉ s. This is NonUnitalSubalgebra.unitization upgraded to an AlgEquiv onto its range.
• NonUnitalSubsemiring.unitization : Unitization ℕ s →ₐ[ℕ] R: the natural ℕ-algebra homomorphism from the unitization of a non-unital subsemiring s into the ring containing it. The range of this map is subalgebraOfSubsemiring (Subsemiring.closure s). This is just NonUnitalSubalgebra.unitization s but we provide a separate declaration because there is an instance Lean can't find on its own due to outParam.
• NonUnitalSubring.unitization : Unitization ℤ s →ₐ[ℤ] R: the natural ℤ-algebra homomorphism from the unitization of a non-unital subring s into the ring containing it. The range of this map is subalgebraOfSubring (Subring.closure s). This is just NonUnitalSubalgebra.unitization s but we provide a separate declaration because there is an instance Lean can't find on its own due to outParam.
• NonUnitalStarSubalgebra s : Unitization R s →⋆ₐ[R] A: a version of NonUnitalSubalgebra.unitization for star algebras.
• NonUnitalStarSubalgebra.unitizationStarAlgEquiv s : Unitization R s ≃⋆ₐ[R] StarSubalgebra.adjoin R (s : Set A): a version of NonUnitalSubalgebra.unitizationAlgEquiv for star algebras.

Subalgebras

def Subalgebra.toNonUnitalSubalgebra {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) : NonUnitalSubalgebra R A

Turn a Subalgebra into a NonUnitalSubalgebra by forgetting that it contains 1.

theorem Subalgebra.one_mem_toNonUnitalSubalgebra {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) : 1 ∈ Subalgebra.toNonUnitalSubalgebra S

def NonUnitalSubalgebra.toSubalgebra {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (S : NonUnitalSubalgebra R A) (h1 : 1 ∈ S) : Subalgebra R A

Turn a non-unital subalgebra containing 1 into a subalgebra.

theorem Subalgebra.toNonUnitalSubalgebra_toSubalgebra {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) : NonUnitalSubalgebra.toSubalgebra (Subalgebra.toNonUnitalSubalgebra S) (_ : 1 ∈ S) = S

theorem NonUnitalSubalgebra.toSubalgebra_toNonUnitalSubalgebra {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (S : NonUnitalSubalgebra R A) (h1 : 1 ∈ S) : Subalgebra.toNonUnitalSubalgebra (NonUnitalSubalgebra.toSubalgebra S h1) = S

theorem Unitization.lift_range_le {R : Type u_1} {A : Type u_2} {C : Type u_3} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [Semiring C] [Algebra R C] {f : A →ₙₐ[R] C} {S : Subalgebra R C} : AlgHom.range (↑Unitization.lift f) ≤ S ↔ NonUnitalAlgHom.range f ≤ Subalgebra.toNonUnitalSubalgebra S

theorem Unitization.lift_range {R : Type u_1} {A : Type u_2} {C : Type u_3} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [Semiring C] [Algebra R C] (f : A →ₙₐ[R] C) : AlgHom.range (↑Unitization.lift f) = Algebra.adjoin R ↑(NonUnitalAlgHom.range f)

def NonUnitalSubalgebra.unitization {R : Type u_1} {S : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [SetLike S A] [hSA : NonUnitalSubsemiringClass S A] [hSRA : SMulMemClass S R A] (s : S) : Unitization R { x // x ∈ s } →ₐ[R] A

The natural R-algebra homomorphism from the unitization of a non-unital subalgebra into the algebra containing it.

@[simp]

theorem NonUnitalSubalgebra.unitization_apply {R : Type u_1} {S : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [SetLike S A] [hSA : NonUnitalSubsemiringClass S A] [hSRA : SMulMemClass S R A] (s : S) (x : Unitization R { x // x ∈ s }) : ↑(NonUnitalSubalgebra.unitization s) x = ↑(algebraMap R A) (Unitization.fst x) + ↑(Unitization.snd x)

theorem NonUnitalSubalgebra.unitization_range {R : Type u_1} {S : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [SetLike S A] [hSA : NonUnitalSubsemiringClass S A] [hSRA : SMulMemClass S R A] (s : S) : AlgHom.range (NonUnitalSubalgebra.unitization s) = Algebra.adjoin R ↑s

theorem AlgHomClass.unitization_injective' {F : Type u_1} {R : Type u_2} {S : Type u_3} {A : Type u_4} [CommRing R] [Ring A] [Algebra R A] [SetLike S A] [hSA : NonUnitalSubringClass S A] [hSRA : SMulMemClass S R A] (s : S) (h : ∀ (r : R), r ≠ 0 → ¬↑(algebraMap R A) r ∈ s) [AlgHomClass F R (Unitization R { x // x ∈ s }) A] (f : F) (hf : ∀ (x : { x // x ∈ s }), ↑f ↑x = ↑x) : Function.Injective ↑f

A sufficient condition for injectivity of NonUnitalSubalgebra.unitization when the scalars are a commutative ring. When the scalars are a field, one should use the more natural NonUnitalStarSubalgebra.unitization_injective whose hypothesis is easier to verify.

theorem AlgHomClass.unitization_injective {F : Type u_1} {R : Type u_2} {S : Type u_3} {A : Type u_4} [Field R] [Ring A] [Algebra R A] [SetLike S A] [hSA : NonUnitalSubringClass S A] [hSRA : SMulMemClass S R A] (s : S) (h1 : ¬1 ∈ s) [AlgHomClass F R (Unitization R { x // x ∈ s }) A] (f : F) (hf : ∀ (x : { x // x ∈ s }), ↑f ↑x = ↑x) : Function.Injective ↑f

This is a generic version which allows us to prove both NonUnitalSubalgebra.unitization_injective and NonUnitalStarSubalgebra.unitization_injective.

theorem NonUnitalSubalgebra.unitization_injective {R : Type u_1} {S : Type u_2} {A : Type u_3} [Field R] [Ring A] [Algebra R A] [SetLike S A] [hSA : NonUnitalSubringClass S A] [hSRA : SMulMemClass S R A] (s : S) (h1 : ¬1 ∈ s) : Function.Injective ↑(NonUnitalSubalgebra.unitization s)

@[simp]

theorem NonUnitalSubalgebra.unitizationAlgEquiv_apply_coe {R : Type u_1} {S : Type u_2} {A : Type u_3} [Field R] [Ring A] [Algebra R A] [SetLike S A] [hSA : NonUnitalSubringClass S A] [hSRA : SMulMemClass S R A] (s : S) (h1 : ¬1 ∈ s) : ∀ (a : Unitization R { x // x ∈ s }), ↑(↑(NonUnitalSubalgebra.unitizationAlgEquiv s h1) a) = ↑(algebraMap R A) (Unitization.fst a) + ↑(Unitization.snd a)

noncomputable def NonUnitalSubalgebra.unitizationAlgEquiv {R : Type u_1} {S : Type u_2} {A : Type u_3} [Field R] [Ring A] [Algebra R A] [SetLike S A] [hSA : NonUnitalSubringClass S A] [hSRA : SMulMemClass S R A] (s : S) (h1 : ¬1 ∈ s) : Unitization R { x // x ∈ s } ≃ₐ[R] { x // x ∈ Algebra.adjoin R ↑s }

If a NonUnitalSubalgebra over a field does not contain 1, then its unitization is isomorphic to its Algebra.adjoin.

Subsemirings

def Subsemiring.toNonUnitalSubsemiring {R : Type u_1} [NonAssocSemiring R] (S : Subsemiring R) : NonUnitalSubsemiring R

Turn a Subsemiring into a NonUnitalSubsemiring by forgetting that it contains 1.

theorem Subsemiring.one_mem_toNonUnitalSubsemiring {R : Type u_1} [NonAssocSemiring R] (S : Subsemiring R) : 1 ∈ Subsemiring.toNonUnitalSubsemiring S

def NonUnitalSubsemiring.toSubsemiring {R : Type u_1} [NonAssocSemiring R] (S : NonUnitalSubsemiring R) (h1 : 1 ∈ S) : Subsemiring R

Turn a non-unital subsemiring containing 1 into a subsemiring.

theorem Subsemiring.toNonUnitalSubsemiring_toSubsemiring {R : Type u_1} [NonAssocSemiring R] (S : Subsemiring R) : NonUnitalSubsemiring.toSubsemiring (Subsemiring.toNonUnitalSubsemiring S) (_ : 1 ∈ S) = S

theorem NonUnitalSubsemiring.toSubsemiring_toNonUnitalSubsemiring {R : Type u_1} [NonAssocSemiring R] (S : NonUnitalSubsemiring R) (h1 : 1 ∈ S) : Subsemiring.toNonUnitalSubsemiring (NonUnitalSubsemiring.toSubsemiring S h1) = S

def NonUnitalSubsemiring.unitization {R : Type u_1} {S : Type u_2} [Semiring R] [SetLike S R] [hSR : NonUnitalSubsemiringClass S R] (s : S) : Unitization ℕ { x // x ∈ s } →ₐ[ℕ] R

The natural ℕ-algebra homomorphism from the unitization of a non-unital subsemiring to its Subsemiring.closure.

@[simp]

theorem NonUnitalSubsemiring.unitization_apply {R : Type u_1} {S : Type u_2} [Semiring R] [SetLike S R] [hSR : NonUnitalSubsemiringClass S R] (s : S) (x : Unitization ℕ { x // x ∈ s }) : ↑(NonUnitalSubsemiring.unitization s) x = ↑(Unitization.fst x) + ↑(Unitization.snd x)

theorem NonUnitalSubsemiring.unitization_range {R : Type u_1} {S : Type u_2} [Semiring R] [SetLike S R] [hSR : NonUnitalSubsemiringClass S R] (s : S) : AlgHom.range (NonUnitalSubsemiring.unitization s) = subalgebraOfSubsemiring (Subsemiring.closure ↑s)

Subrings

def Subring.toNonUnitalSubring {R : Type u_1} [Ring R] (S : Subring R) : NonUnitalSubring R

Turn a Subring into a NonUnitalSubring by forgetting that it contains 1.

theorem Subring.one_mem_toNonUnitalSubring {R : Type u_1} [Ring R] (S : Subring R) : 1 ∈ Subring.toNonUnitalSubring S

def NonUnitalSubring.toSubring {R : Type u_1} [Ring R] (S : NonUnitalSubring R) (h1 : 1 ∈ S) : Subring R

Turn a non-unital subring containing 1 into a subring.

theorem Subring.toNonUnitalSubring_toSubring {R : Type u_1} [Ring R] (S : Subring R) : NonUnitalSubring.toSubring (Subring.toNonUnitalSubring S) (_ : 1 ∈ S) = S

theorem NonUnitalSubring.toSubring_toNonUnitalSubring {R : Type u_1} [Ring R] (S : NonUnitalSubring R) (h1 : 1 ∈ S) : Subring.toNonUnitalSubring (NonUnitalSubring.toSubring S h1) = S

def NonUnitalSubring.unitization {R : Type u_1} {S : Type u_2} [Ring R] [SetLike S R] [hSR : NonUnitalSubringClass S R] (s : S) : Unitization ℤ { x // x ∈ s } →ₐ[ℤ] R

The natural ℤ-algebra homomorphism from the unitization of a non-unital subring to its Subring.closure.

@[simp]

theorem NonUnitalSubring.unitization_apply {R : Type u_1} {S : Type u_2} [Ring R] [SetLike S R] [hSR : NonUnitalSubringClass S R] (s : S) (x : Unitization ℤ { x // x ∈ s }) : ↑(NonUnitalSubring.unitization s) x = ↑(Unitization.fst x) + ↑(Unitization.snd x)

theorem NonUnitalSubring.unitization_range {R : Type u_1} {S : Type u_2} [Ring R] [SetLike S R] [hSR : NonUnitalSubringClass S R] (s : S) : AlgHom.range (NonUnitalSubring.unitization s) = subalgebraOfSubring (Subring.closure ↑s)

Star subalgebras

def StarSubalgebra.toNonUnitalStarSubalgebra {R : Type u_1} {A : Type u_2} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] (S : StarSubalgebra R A) : NonUnitalStarSubalgebra R A

Turn a StarSubalgebra into a NonUnitalStarSubalgebra by forgetting that it contains 1.

theorem StarSubalgebra.one_mem_toNonUnitalStarSubalgebra {R : Type u_1} {A : Type u_2} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] (S : StarSubalgebra R A) : 1 ∈ StarSubalgebra.toNonUnitalStarSubalgebra S

def NonUnitalStarSubalgebra.toStarSubalgebra {R : Type u_1} {A : Type u_2} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] (S : NonUnitalStarSubalgebra R A) (h1 : 1 ∈ S) : StarSubalgebra R A

Turn a non-unital star subalgebra containing 1 into a StarSubalgebra.

theorem StarSubalgebra.toNonUnitalStarSubalgebra_toStarSubalgebra {R : Type u_1} {A : Type u_2} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] (S : StarSubalgebra R A) : NonUnitalStarSubalgebra.toStarSubalgebra (StarSubalgebra.toNonUnitalStarSubalgebra S) (_ : 1 ∈ S.carrier) = S

theorem NonUnitalStarSubalgebra.toStarSubalgebra_toNonUnitalStarSubalgebra {R : Type u_1} {A : Type u_2} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] (S : NonUnitalStarSubalgebra R A) (h1 : 1 ∈ S) : StarSubalgebra.toNonUnitalStarSubalgebra (NonUnitalStarSubalgebra.toStarSubalgebra S h1) = S

theorem Unitization.starLift_range_le {R : Type u_1} {A : Type u_2} {C : Type u_3} [CommSemiring R] [NonUnitalSemiring A] [StarRing R] [StarRing A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [StarModule R A] [Semiring C] [StarRing C] [Algebra R C] [StarModule R C] {f : A →⋆ₙₐ[R] C} {S : StarSubalgebra R C} : StarAlgHom.range (↑Unitization.starLift f) ≤ S ↔ NonUnitalStarAlgHom.range f ≤ StarSubalgebra.toNonUnitalStarSubalgebra S

theorem Unitization.starLift_range {R : Type u_1} {A : Type u_2} {C : Type u_3} [CommSemiring R] [NonUnitalSemiring A] [StarRing R] [StarRing A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [StarModule R A] [Semiring C] [StarRing C] [Algebra R C] [StarModule R C] (f : A →⋆ₙₐ[R] C) : StarAlgHom.range (↑Unitization.starLift f) = StarSubalgebra.adjoin R ↑(NonUnitalStarAlgHom.range f)

def NonUnitalStarSubalgebra.unitization {R : Type u_1} {S : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] [SetLike S A] [hSA : NonUnitalSubsemiringClass S A] [hSRA : SMulMemClass S R A] [StarMemClass S A] (s : S) : Unitization R { x // x ∈ s } →⋆ₐ[R] A

The natural star R-algebra homomorphism from the unitization of a non-unital star subalgebra to its StarSubalgebra.adjoin.

@[simp]

theorem NonUnitalStarSubalgebra.unitization_apply {R : Type u_1} {S : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] [SetLike S A] [hSA : NonUnitalSubsemiringClass S A] [hSRA : SMulMemClass S R A] [StarMemClass S A] (s : S) (x : Unitization R { x // x ∈ s }) : ↑(NonUnitalStarSubalgebra.unitization s) x = ↑(algebraMap R A) (Unitization.fst x) + ↑(Unitization.snd x)

theorem NonUnitalStarSubalgebra.unitization_range {R : Type u_1} {S : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] [SetLike S A] [hSA : NonUnitalSubsemiringClass S A] [hSRA : SMulMemClass S R A] [StarMemClass S A] (s : S) : StarAlgHom.range (NonUnitalStarSubalgebra.unitization s) = StarSubalgebra.adjoin R ↑s

theorem NonUnitalStarSubalgebra.unitization_injective {R : Type u_1} {S : Type u_2} {A : Type u_3} [Field R] [StarRing R] [Ring A] [StarRing A] [Algebra R A] [StarModule R A] [SetLike S A] [hSA : NonUnitalSubringClass S A] [hSRA : SMulMemClass S R A] [StarMemClass S A] (s : S) (h1 : ¬1 ∈ s) : Function.Injective ↑(NonUnitalStarSubalgebra.unitization s)

@[simp]

theorem NonUnitalStarSubalgebra.unitizationStarAlgEquiv_apply_coe {R : Type u_1} {S : Type u_2} {A : Type u_3} [Field R] [StarRing R] [Ring A] [StarRing A] [Algebra R A] [StarModule R A] [SetLike S A] [hSA : NonUnitalSubringClass S A] [hSRA : SMulMemClass S R A] [StarMemClass S A] (s : S) (h1 : ¬1 ∈ s) (a : Unitization R { x // x ∈ s }) : ↑(↑(NonUnitalStarSubalgebra.unitizationStarAlgEquiv s h1) a) = ↑(algebraMap R A) (Unitization.fst a) + ↑(Unitization.snd a)

noncomputable def NonUnitalStarSubalgebra.unitizationStarAlgEquiv {R : Type u_1} {S : Type u_2} {A : Type u_3} [Field R] [StarRing R] [Ring A] [StarRing A] [Algebra R A] [StarModule R A] [SetLike S A] [hSA : NonUnitalSubringClass S A] [hSRA : SMulMemClass S R A] [StarMemClass S A] (s : S) (h1 : ¬1 ∈ s) : Unitization R { x // x ∈ s } ≃⋆ₐ[R] { x // x ∈ StarSubalgebra.adjoin R ↑s }

If a NonUnitalStarSubalgebra over a field does not contain 1, then its unitization is isomorphic to its StarSubalgebra.adjoin.