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 StarAlgebra.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] StarAlgebra.adjoin R (s : Set A): a version of NonUnitalSubalgebra.unitizationAlgEquiv for star algebras.

Subalgebras

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} : (lift f).range ≤ S ↔ NonUnitalAlgHom.range f ≤ S.toNonUnitalSubalgebra

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) : (lift f).range = 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 ↥s →ₐ[R] A

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

Equations

• NonUnitalSubalgebra.unitization s = Unitization.lift (NonUnitalSubalgebraClass.subtype s)

@[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 ↥s) : (unitization s) x = (algebraMap R A) x.fst + ↑x.snd

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) : (unitization s).range = 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) [FunLike F (Unitization R ↥s) A] [AlgHomClass F R (Unitization R ↥s) A] (f : F) (hf : ∀ (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) [FunLike F (Unitization R ↥s) A] [AlgHomClass F R (Unitization R ↥s) A] (f : F) (hf : ∀ (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 ⇑(unitization s)

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 ↥s ≃ₐ[R] ↥(Algebra.adjoin R ↑s)

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

Equations

• NonUnitalSubalgebra.unitizationAlgEquiv s h1 = AlgEquiv.ofBijective ((NonUnitalSubalgebra.unitization s).codRestrict (Algebra.adjoin R ↑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 ↥s) : ↑((unitizationAlgEquiv s h1) a) = (algebraMap R A) a.fst + ↑a.snd

Subsemirings

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

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

Equations

• NonUnitalSubsemiring.unitization s = NonUnitalSubalgebra.unitization s

@[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 ℕ ↥s) : (unitization s) x = ↑x.fst + ↑x.snd

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

Subrings

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

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

Equations

• NonUnitalSubring.unitization s = NonUnitalSubalgebra.unitization s

@[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 ℤ ↥s) : (unitization s) x = ↑x.fst + ↑x.snd

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

Star subalgebras

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} : (starLift f).range ≤ S ↔ NonUnitalStarAlgHom.range f ≤ S.toNonUnitalStarSubalgebra

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) : (starLift f).range = StarAlgebra.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 ↥s →⋆ₐ[R] A

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

Equations

• NonUnitalStarSubalgebra.unitization s = Unitization.starLift (NonUnitalStarSubalgebraClass.subtype s)

@[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 ↥s) : (unitization s) x = (algebraMap R A) x.fst + ↑x.snd

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) : (unitization s).range = StarAlgebra.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 ⇑(unitization s)

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 ↥s ≃⋆ₐ[R] ↥(StarAlgebra.adjoin R ↑s)

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

Equations

• NonUnitalStarSubalgebra.unitizationStarAlgEquiv s h1 = StarAlgEquiv.ofBijective ((NonUnitalStarSubalgebra.unitization s).codRestrict (StarAlgebra.adjoin R ↑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 ↥s) : ↑((unitizationStarAlgEquiv s h1) a) = (algebraMap R A) a.fst + ↑a.snd