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

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.

Equations

• S.toNonUnitalSubalgebra = { carrier := S.carrier, add_mem' := ⋯, zero_mem' := ⋯, mul_mem' := ⋯, smul_mem' := ⋯ }

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 ∈ S.toNonUnitalSubalgebra

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.

Equations

• S.toSubalgebra h1 = { carrier := S.carrier, mul_mem' := ⋯, one_mem' := h1, add_mem' := ⋯, zero_mem' := ⋯, algebraMap_mem' := ⋯ }

theorem Subalgebra.toNonUnitalSubalgebra_toSubalgebra {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) : S.toNonUnitalSubalgebra.toSubalgebra ⋯ = 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) : (S.toSubalgebra h1).toNonUnitalSubalgebra = S

theorem Algebra.adjoin_nonUnitalSubalgebra_eq_span {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (s : NonUnitalSubalgebra R A) : Subalgebra.toSubmodule (Algebra.adjoin R ↑s) = Submodule.span R {1} ⊔ s.toSubmodule

theorem NonUnitalAlgebra.adjoin_le_algebra_adjoin (R : Type u_1) {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (s : Set A) : NonUnitalAlgebra.adjoin R s ≤ (Algebra.adjoin R s).toNonUnitalSubalgebra

theorem Algebra.adjoin_nonUnitalSubalgebra (R : Type u_1) {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (s : Set A) : Algebra.adjoin R ↑(NonUnitalAlgebra.adjoin R s) = Algebra.adjoin R 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} : (Unitization.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) : (Unitization.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) : (NonUnitalSubalgebra.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) : (NonUnitalSubalgebra.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 ⇑(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 ↥s) : ↑((NonUnitalSubalgebra.unitizationAlgEquiv s h1) a) = (algebraMap R A) a.fst + ↑a.snd

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) ⋯) ⋯

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.

Equations

• S.toNonUnitalSubsemiring = { carrier := S.carrier, add_mem' := ⋯, zero_mem' := ⋯, mul_mem' := ⋯ }

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

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.

Equations

• S.toSubsemiring h1 = { carrier := S.carrier, mul_mem' := ⋯, one_mem' := h1, add_mem' := ⋯, zero_mem' := ⋯ }

theorem Subsemiring.toNonUnitalSubsemiring_toSubsemiring {R : Type u_1} [NonAssocSemiring R] (S : Subsemiring R) : S.toNonUnitalSubsemiring.toSubsemiring ⋯ = S

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

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

Equations

• S.toNonUnitalSubring = { carrier := S.carrier, add_mem' := ⋯, zero_mem' := ⋯, mul_mem' := ⋯, neg_mem' := ⋯ }

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

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.

Equations

• S.toSubring h1 = { carrier := S.carrier, mul_mem' := ⋯, one_mem' := h1, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }

theorem Subring.toNonUnitalSubring_toSubring {R : Type u_1} [Ring R] (S : Subring R) : S.toNonUnitalSubring.toSubring ⋯ = S

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

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

Equations

• S.toNonUnitalStarSubalgebra = { carrier := S.carrier, add_mem' := ⋯, zero_mem' := ⋯, mul_mem' := ⋯, smul_mem' := ⋯, star_mem' := ⋯ }

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 ∈ S.toNonUnitalStarSubalgebra

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.

Equations

• S.toStarSubalgebra h1 = { carrier := S.carrier, mul_mem' := ⋯, one_mem' := h1, add_mem' := ⋯, zero_mem' := ⋯, algebraMap_mem' := ⋯, star_mem' := ⋯ }

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) : S.toNonUnitalStarSubalgebra.toStarSubalgebra ⋯ = 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) : (S.toStarSubalgebra h1).toNonUnitalStarSubalgebra = S

theorem StarAlgebra.adjoin_nonUnitalStarSubalgebra_eq_span {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) : Subalgebra.toSubmodule (StarAlgebra.adjoin R ↑s).toSubalgebra = Submodule.span R {1} ⊔ s.toSubmodule

theorem NonUnitalStarAlgebra.adjoin_le_starAlgebra_adjoin (R : Type u_1) {A : Type u_2} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] (s : Set A) : NonUnitalStarAlgebra.adjoin R s ≤ (StarAlgebra.adjoin R s).toNonUnitalStarSubalgebra

theorem StarAlgebra.adjoin_nonUnitalStarSubalgebra (R : Type u_1) {A : Type u_2} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] (s : Set A) : StarAlgebra.adjoin R ↑(NonUnitalStarAlgebra.adjoin R s) = StarAlgebra.adjoin R 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} : (Unitization.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) : (Unitization.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) : (NonUnitalStarSubalgebra.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) : (NonUnitalStarSubalgebra.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 ⇑(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 ↥s) : ↑((NonUnitalStarSubalgebra.unitizationStarAlgEquiv s h1) a) = (algebraMap R A) a.fst + ↑a.snd

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) ⋯) ⋯