# Documentation

Mathlib.Algebra.Algebra.Subalgebra.Unitization

# 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} [] [] [Algebra R A] (S : ) :

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

Instances For
theorem Subalgebra.one_mem_toNonUnitalSubalgebra {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (S : ) :
def NonUnitalSubalgebra.toSubalgebra {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (S : ) (h1 : 1 S) :

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

Instances For
theorem Subalgebra.toNonUnitalSubalgebra_toSubalgebra {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (S : ) :
= S
theorem NonUnitalSubalgebra.toSubalgebra_toNonUnitalSubalgebra {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (S : ) (h1 : 1 S) :
theorem Unitization.lift_range_le {R : Type u_1} {A : Type u_2} {C : Type u_3} [] [Module R A] [] [] [] [Algebra R C] {f : A →ₙₐ[R] C} {S : } :
AlgHom.range (Unitization.lift f) S
theorem Unitization.lift_range {R : Type u_1} {A : Type u_2} {C : Type u_3} [] [Module R A] [] [] [] [Algebra R C] (f : A →ₙₐ[R] C) :
AlgHom.range (Unitization.lift f) =
def NonUnitalSubalgebra.unitization {R : Type u_1} {S : Type u_2} {A : Type u_3} [] [] [Algebra R A] [SetLike S A] [hSA : ] [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.

Instances For
@[simp]
theorem NonUnitalSubalgebra.unitization_apply {R : Type u_1} {S : Type u_2} {A : Type u_3} [] [] [Algebra R A] [SetLike S A] [hSA : ] [hSRA : SMulMemClass S R A] (s : S) (x : Unitization R { x // x s }) :
= ↑() () + ↑()
theorem NonUnitalSubalgebra.unitization_range {R : Type u_1} {S : Type u_2} {A : Type u_3} [] [] [Algebra R A] [SetLike S A] [hSA : ] [hSRA : SMulMemClass S R A] (s : S) :
theorem AlgHomClass.unitization_injective' {F : Type u_1} {R : Type u_2} {S : Type u_3} {A : Type u_4} [] [Ring A] [Algebra R A] [SetLike S A] [hSA : ] [hSRA : SMulMemClass S R A] (s : S) (h : ∀ (r : R), r 0¬↑() r s) [AlgHomClass F R (Unitization R { x // x s }) A] (f : F) (hf : ∀ (x : { x // x s }), f x = x) :

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} [] [Ring A] [Algebra R A] [SetLike S A] [hSA : ] [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) :

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} [] [Ring A] [Algebra R A] [SetLike S A] [hSA : ] [hSRA : SMulMemClass S R A] (s : S) (h1 : ¬1 s) :
@[simp]
theorem NonUnitalSubalgebra.unitizationAlgEquiv_apply_coe {R : Type u_1} {S : Type u_2} {A : Type u_3} [] [Ring A] [Algebra R A] [SetLike S A] [hSA : ] [hSRA : SMulMemClass S R A] (s : S) (h1 : ¬1 s) :
∀ (a : Unitization R { x // x s }), ↑() = ↑() () + ↑()
noncomputable def NonUnitalSubalgebra.unitizationAlgEquiv {R : Type u_1} {S : Type u_2} {A : Type u_3} [] [Ring A] [Algebra R A] [SetLike S A] [hSA : ] [hSRA : SMulMemClass S R A] (s : S) (h1 : ¬1 s) :
Unitization R { x // x s } ≃ₐ[R] { x // x }

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

Instances For

## Subsemirings #

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

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

Instances For
def NonUnitalSubsemiring.toSubsemiring {R : Type u_1} [] (S : ) (h1 : 1 S) :

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

Instances For
def NonUnitalSubsemiring.unitization {R : Type u_1} {S : Type u_2} [] [SetLike S R] [hSR : ] (s : S) :

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

Instances For
@[simp]
theorem NonUnitalSubsemiring.unitization_apply {R : Type u_1} {S : Type u_2} [] [SetLike S R] [hSR : ] (s : S) (x : Unitization { x // x s }) :
= ↑() + ↑()
theorem NonUnitalSubsemiring.unitization_range {R : Type u_1} {S : Type u_2} [] [SetLike S R] [hSR : ] (s : S) :

## Subrings #

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

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

Instances For
theorem Subring.one_mem_toNonUnitalSubring {R : Type u_1} [Ring R] (S : ) :
def NonUnitalSubring.toSubring {R : Type u_1} [Ring R] (S : ) (h1 : 1 S) :

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

Instances For
theorem NonUnitalSubring.toSubring_toNonUnitalSubring {R : Type u_1} [Ring R] (S : ) (h1 : 1 S) :
def NonUnitalSubring.unitization {R : Type u_1} {S : Type u_2} [Ring R] [SetLike S R] [hSR : ] (s : S) :

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

Instances For
@[simp]
theorem NonUnitalSubring.unitization_apply {R : Type u_1} {S : Type u_2} [Ring R] [SetLike S R] [hSR : ] (s : S) (x : Unitization { x // x s }) :
= ↑() + ↑()
theorem NonUnitalSubring.unitization_range {R : Type u_1} {S : Type u_2} [Ring R] [SetLike S R] [hSR : ] (s : S) :

## Star subalgebras #

def StarSubalgebra.toNonUnitalStarSubalgebra {R : Type u_1} {A : Type u_2} [] [] [] [] [Algebra R A] [] (S : ) :

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

Instances For
theorem StarSubalgebra.one_mem_toNonUnitalStarSubalgebra {R : Type u_1} {A : Type u_2} [] [] [] [] [Algebra R A] [] (S : ) :
def NonUnitalStarSubalgebra.toStarSubalgebra {R : Type u_1} {A : Type u_2} [] [] [] [] [Algebra R A] [] (S : ) (h1 : 1 S) :

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

Instances For
theorem StarSubalgebra.toNonUnitalStarSubalgebra_toStarSubalgebra {R : Type u_1} {A : Type u_2} [] [] [] [] [Algebra R A] [] (S : ) :
theorem NonUnitalStarSubalgebra.toStarSubalgebra_toNonUnitalStarSubalgebra {R : Type u_1} {A : Type u_2} [] [] [] [] [Algebra R A] [] (S : ) (h1 : 1 S) :
theorem Unitization.starLift_range_le {R : Type u_1} {A : Type u_2} {C : Type u_3} [] [] [] [Module R A] [] [] [] [] [] [Algebra R C] [] {f : A →⋆ₙₐ[R] C} {S : } :
StarAlgHom.range (Unitization.starLift f) S
theorem Unitization.starLift_range {R : Type u_1} {A : Type u_2} {C : Type u_3} [] [] [] [Module R A] [] [] [] [] [] [Algebra R C] [] (f : A →⋆ₙₐ[R] C) :
StarAlgHom.range (Unitization.starLift f) =
def NonUnitalStarSubalgebra.unitization {R : Type u_1} {S : Type u_2} {A : Type u_3} [] [] [] [] [Algebra R A] [] [SetLike S A] [hSA : ] [hSRA : SMulMemClass S R 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.

Instances For
@[simp]
theorem NonUnitalStarSubalgebra.unitization_apply {R : Type u_1} {S : Type u_2} {A : Type u_3} [] [] [] [] [Algebra R A] [] [SetLike S A] [hSA : ] [hSRA : SMulMemClass S R A] [] (s : S) (x : Unitization R { x // x s }) :
= ↑() () + ↑()
theorem NonUnitalStarSubalgebra.unitization_range {R : Type u_1} {S : Type u_2} {A : Type u_3} [] [] [] [] [Algebra R A] [] [SetLike S A] [hSA : ] [hSRA : SMulMemClass S R A] [] (s : S) :
theorem NonUnitalStarSubalgebra.unitization_injective {R : Type u_1} {S : Type u_2} {A : Type u_3} [] [] [Ring A] [] [Algebra R A] [] [SetLike S A] [hSA : ] [hSRA : SMulMemClass S R A] [] (s : S) (h1 : ¬1 s) :
@[simp]
theorem NonUnitalStarSubalgebra.unitizationStarAlgEquiv_apply_coe {R : Type u_1} {S : Type u_2} {A : Type u_3} [] [] [Ring A] [] [Algebra R A] [] [SetLike S A] [hSA : ] [hSRA : SMulMemClass S R A] [] (s : S) (h1 : ¬1 s) (a : Unitization R { x // x s }) :
↑() = ↑() () + ↑()
noncomputable def NonUnitalStarSubalgebra.unitizationStarAlgEquiv {R : Type u_1} {S : Type u_2} {A : Type u_3} [] [] [Ring A] [] [Algebra R A] [] [SetLike S A] [hSA : ] [hSRA : SMulMemClass S R A] [] (s : S) (h1 : ¬1 s) :
Unitization R { x // x s } ≃⋆ₐ[R] { x // x }

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

Instances For