The unitization (over R) of C₀(X, R) is C(OnePoint X, R)

Given a topological space X and a topological ring R one can extend an element C₀(X, R), the continuous functions vanishing at infinity, to C(OnePoint X, R), the continuous functions on the one-point compactification of X, by taking the value 0 at ∞. This can be lifted to an equivalence between Unitization R C₀(X, R) and C(OnePoint X, R).

Main definitions

• ZeroAtInftyContinuousMap.toOnePoint : C₀(X, R) → C(OnePoint X, R) : the extension of f : C₀(X, R) to the function which takes the value 0 at ∞
• ContinuousMap.toZeroAtInfty: C(OnePoint X, R) → C₀(X, R) : f ↦ fun x ↦ g x - g ∞

• ZeroAtInftyContinuousMap.unitizationEquiv : Unitization R C₀(X, R) ≃ C(OnePoint X, R) : lift ZeroAtInftyContinuousMap.toOnePoint to an equivalence from the Unitization, with inverse given by f ↦ .mk (f ∞, f.toZeroAtInfty)
• Various bundled versions of all of the above.

Implementation notes

The simp normal form of each bundled morphism is the unbundled map, so the unbundled maps have their own simp lemmas for various operatoins.

def ZeroAtInftyContinuousMap.toOnePoint {X : Type u_1} {R : Type u_2} [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [Zero R] (f : ZeroAtInftyContinuousMap X R) : C(OnePoint X, R)

Extension by zero of a continuous function vanishing at infinity, as a continuous function on the one-point compactification.

Equations

• f.toOnePoint = OnePoint.continuousMapMk f.toContinuousMap 0 ⋯

@[simp]

theorem ZeroAtInftyContinuousMap.toOnePoint_infty {X : Type u_1} {R : Type u_2} [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [Zero R] (f : ZeroAtInftyContinuousMap X R) : f.toOnePoint OnePoint.infty = 0

@[simp]

theorem ZeroAtInftyContinuousMap.toOnePoint_coe {X : Type u_1} {R : Type u_2} [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [Zero R] (f : ZeroAtInftyContinuousMap X R) (x : X) : f.toOnePoint ↑x = f x

theorem ZeroAtInftyContinuousMap.toOnePoint_injective {X : Type u_1} {R : Type u_2} [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [Zero R] : Function.Injective toOnePoint

@[simp]

theorem ZeroAtInftyContinuousMap.toOnePoint_zero {X : Type u_1} {R : Type u_2} [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [Zero R] : toOnePoint 0 = 0

@[simp]

theorem ZeroAtInftyContinuousMap.toOnePoint_add {X : Type u_1} {R : Type u_2} [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [AddZeroClass R] [ContinuousAdd R] (f g : ZeroAtInftyContinuousMap X R) : (f + g).toOnePoint = f.toOnePoint + g.toOnePoint

@[simp]

theorem ZeroAtInftyContinuousMap.toOnePoint_neg {X : Type u_1} {R : Type u_2} [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [AddGroup R] [IsTopologicalAddGroup R] (f : ZeroAtInftyContinuousMap X R) : (-f).toOnePoint = -f.toOnePoint

@[simp]

theorem ZeroAtInftyContinuousMap.toOnePoint_sub {X : Type u_1} {R : Type u_2} [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [AddGroup R] [IsTopologicalAddGroup R] (f g : ZeroAtInftyContinuousMap X R) : (f - g).toOnePoint = f.toOnePoint - g.toOnePoint

@[simp]

theorem ZeroAtInftyContinuousMap.toOnePoint_mul {X : Type u_1} {R : Type u_2} [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [MulZeroClass R] [ContinuousMul R] (f g : ZeroAtInftyContinuousMap X R) : (f * g).toOnePoint = f.toOnePoint * g.toOnePoint

@[simp]

theorem ZeroAtInftyContinuousMap.toOnePoint_smul {X : Type u_1} {R : Type u_2} {S : Type u_3} [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [Zero R] [Zero S] [SMulWithZero S R] [ContinuousConstSMul S R] (s : S) (f : ZeroAtInftyContinuousMap X R) : (s • f).toOnePoint = s • f.toOnePoint

@[simp]

theorem ZeroAtInftyContinuousMap.toOnePoint_star {X : Type u_1} {R : Type u_2} [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [AddMonoid R] [StarAddMonoid R] [ContinuousStar R] (f : ZeroAtInftyContinuousMap X R) : (star f).toOnePoint = star f.toOnePoint

def ZeroAtInftyContinuousMap.toOnePointAddMonoidHom (X : Type u_1) (R : Type u_2) [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [AddMonoid R] [ContinuousAdd R] : ZeroAtInftyContinuousMap X R →+ C(OnePoint X, R)

ZeroAtInftyContinuousMap.toOnePoint as an AddMonoidHom.

Equations

• ZeroAtInftyContinuousMap.toOnePointAddMonoidHom X R = { toFun := ZeroAtInftyContinuousMap.toOnePoint, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem ZeroAtInftyContinuousMap.toOnePointAddMonoidHom_apply (X : Type u_1) (R : Type u_2) [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [AddMonoid R] [ContinuousAdd R] (f : ZeroAtInftyContinuousMap X R) : (toOnePointAddMonoidHom X R) f = f.toOnePoint

def ZeroAtInftyContinuousMap.toOnePointLinearMap (X : Type u_1) (R : Type u_2) (S : Type u_3) [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [Semiring S] [AddCommMonoid R] [ContinuousAdd R] [Module S R] [ContinuousConstSMul S R] : ZeroAtInftyContinuousMap X R →ₗ[S] C(OnePoint X, R)

ZeroAtInftyContinuousMap.toOnePoint as a LinearMap.

Equations

• ZeroAtInftyContinuousMap.toOnePointLinearMap X R S = { toFun := ZeroAtInftyContinuousMap.toOnePoint, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem ZeroAtInftyContinuousMap.toOnePointLinearMap_apply (X : Type u_1) (R : Type u_2) (S : Type u_3) [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [Semiring S] [AddCommMonoid R] [ContinuousAdd R] [Module S R] [ContinuousConstSMul S R] (f : ZeroAtInftyContinuousMap X R) : (toOnePointLinearMap X R S) f = f.toOnePoint

@[simp]

theorem ZeroAtInftyContinuousMap.toAddMonoidHom_toOnePointLinearMap (X : Type u_1) (R : Type u_2) (S : Type u_3) [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [Semiring S] [AddCommMonoid R] [ContinuousAdd R] [Module S R] [ContinuousConstSMul S R] : (toOnePointLinearMap X R S).toAddMonoidHom = toOnePointAddMonoidHom X R

def ZeroAtInftyContinuousMap.toOnePointNonUnitalRingHom (X : Type u_1) (R : Type u_2) [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [NonUnitalNonAssocSemiring R] [IsTopologicalSemiring R] : ZeroAtInftyContinuousMap X R →ₙ+* C(OnePoint X, R)

ZeroAtInftyContinuousMap.toOnePoint as a NonUnitalRingHom.

Equations

• ZeroAtInftyContinuousMap.toOnePointNonUnitalRingHom X R = { toFun := ZeroAtInftyContinuousMap.toOnePoint, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem ZeroAtInftyContinuousMap.toOnePointNonUnitalRingHom_apply (X : Type u_1) (R : Type u_2) [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [NonUnitalNonAssocSemiring R] [IsTopologicalSemiring R] (f : ZeroAtInftyContinuousMap X R) : (toOnePointNonUnitalRingHom X R) f = f.toOnePoint

@[simp]

theorem ZeroAtInftyContinuousMap.toAddMonoidHom_toOnePointNonUnitalRingHom (X : Type u_1) (R : Type u_2) [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [NonUnitalNonAssocSemiring R] [IsTopologicalSemiring R] : (toOnePointNonUnitalRingHom X R).toAddMonoidHom = toOnePointAddMonoidHom X R

def ZeroAtInftyContinuousMap.toOnePointNonUnitalAlgHom (X : Type u_1) (R : Type u_2) (S : Type u_3) [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [NonUnitalNonAssocSemiring R] [IsTopologicalSemiring R] [Semiring S] [Module S R] [ContinuousConstSMul S R] : ZeroAtInftyContinuousMap X R →ₙₐ[S] C(OnePoint X, R)

ZeroAtInftyContinuousMap.toOnePoint as a NonUnitalAlgHom.

Equations

• ZeroAtInftyContinuousMap.toOnePointNonUnitalAlgHom X R S = { toFun := ZeroAtInftyContinuousMap.toOnePoint, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯ }

@[simp]

theorem ZeroAtInftyContinuousMap.toOnePointNonUnitalAlgHom_apply (X : Type u_1) (R : Type u_2) (S : Type u_3) [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [NonUnitalNonAssocSemiring R] [IsTopologicalSemiring R] [Semiring S] [Module S R] [ContinuousConstSMul S R] (f : ZeroAtInftyContinuousMap X R) : (toOnePointNonUnitalAlgHom X R S) f = f.toOnePoint

def ZeroAtInftyContinuousMap.toOnePointNonUnitalStarAlgHom (X : Type u_1) (R : Type u_2) (S : Type u_3) [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [NonUnitalNonAssocSemiring R] [IsTopologicalSemiring R] [Semiring S] [Module S R] [ContinuousConstSMul S R] [StarRing R] [ContinuousStar R] : ZeroAtInftyContinuousMap X R →⋆ₙₐ[S] C(OnePoint X, R)

ZeroAtInftyContinuousMap.toOnePoint as a NonUnitalStarAlgHom.

Equations

• ZeroAtInftyContinuousMap.toOnePointNonUnitalStarAlgHom X R S = { toFun := ZeroAtInftyContinuousMap.toOnePoint, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯, map_star' := ⋯ }

@[simp]

theorem ZeroAtInftyContinuousMap.toOnePointNonUnitalStarAlgHom_apply (X : Type u_1) (R : Type u_2) (S : Type u_3) [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [NonUnitalNonAssocSemiring R] [IsTopologicalSemiring R] [Semiring S] [Module S R] [ContinuousConstSMul S R] [StarRing R] [ContinuousStar R] (f : ZeroAtInftyContinuousMap X R) : (toOnePointNonUnitalStarAlgHom X R S) f = f.toOnePoint

@[simp]

theorem ZeroAtInftyContinuousMap.toNonUnitalAlgHom_toOnePointNonUnitalStarAlgHom (X : Type u_1) (R : Type u_2) (S : Type u_3) [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [NonUnitalNonAssocSemiring R] [IsTopologicalSemiring R] [Semiring S] [Module S R] [ContinuousConstSMul S R] [StarRing R] [ContinuousStar R] : (toOnePointNonUnitalStarAlgHom X R S).toNonUnitalAlgHom = toOnePointNonUnitalAlgHom X R S

def ContinuousMap.toZeroAtInfty {X : Type u_1} {R : Type u_2} [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [AddCommGroup R] [IsTopologicalAddGroup R] (g : C(OnePoint X, R)) : ZeroAtInftyContinuousMap X R

The continuous function vanishing at infinity obtained by taking g : C(OnePoint X, R) and restricting g to X and subtracting the constant g ∞.

Equations

• g.toZeroAtInfty = { toFun := fun (x : X) => g ↑x - g OnePoint.infty, continuous_toFun := ⋯, zero_at_infty' := ⋯ }

@[simp]

theorem ContinuousMap.toZeroAtInfty_apply {X : Type u_1} {R : Type u_2} [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [AddCommGroup R] [IsTopologicalAddGroup R] (g : C(OnePoint X, R)) (x : X) : g.toZeroAtInfty x = g ↑x - g OnePoint.infty

@[simp]

theorem ContinuousMap.toZeroAtInfty_const {X : Type u_1} {R : Type u_2} [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [AddCommGroup R] [IsTopologicalAddGroup R] (r : R) : (const (OnePoint X) r).toZeroAtInfty = 0

@[simp]

theorem ContinuousMap.toZeroAtInfty_zero {X : Type u_1} {R : Type u_2} [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [AddCommGroup R] [IsTopologicalAddGroup R] : toZeroAtInfty 0 = 0

@[simp]

theorem ContinuousMap.toZeroAtInfty_add {X : Type u_1} {R : Type u_2} [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [AddCommGroup R] [IsTopologicalAddGroup R] (g h : C(OnePoint X, R)) : (g + h).toZeroAtInfty = g.toZeroAtInfty + h.toZeroAtInfty

@[simp]

theorem ContinuousMap.toZeroAtInfty_neg {X : Type u_1} {R : Type u_2} [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [AddCommGroup R] [IsTopologicalAddGroup R] (g : C(OnePoint X, R)) : (-g).toZeroAtInfty = -g.toZeroAtInfty

@[simp]

theorem ContinuousMap.toZeroAtInfty_sub {X : Type u_1} {R : Type u_2} [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [AddCommGroup R] [IsTopologicalAddGroup R] (g h : C(OnePoint X, R)) : (g - h).toZeroAtInfty = g.toZeroAtInfty - h.toZeroAtInfty

@[simp]

theorem ContinuousMap.toZeroAtInfty_smul {X : Type u_1} {R : Type u_2} {S : Type u_3} [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [AddCommGroup R] [IsTopologicalAddGroup R] [Semiring S] [Module S R] [ContinuousConstSMul S R] (s : S) (g : C(OnePoint X, R)) : (s • g).toZeroAtInfty = s • g.toZeroAtInfty

@[simp]

theorem ContinuousMap.toZeroAtInfty_star {X : Type u_1} {R : Type u_2} [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [AddCommGroup R] [IsTopologicalAddGroup R] [StarAddMonoid R] [ContinuousStar R] (g : C(OnePoint X, R)) : (star g).toZeroAtInfty = star g.toZeroAtInfty

def ContinuousMap.toZeroAtInftyAddMonoidHom (X : Type u_1) (R : Type u_2) [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [AddCommGroup R] [IsTopologicalAddGroup R] : C(OnePoint X, R) →+ ZeroAtInftyContinuousMap X R

ContinuousMap.toZeroAtInfty as an AddMonoidHom.

Equations

• ContinuousMap.toZeroAtInftyAddMonoidHom X R = { toFun := ContinuousMap.toZeroAtInfty, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem ContinuousMap.toZeroAtInftyAddMonoidHom_apply (X : Type u_1) (R : Type u_2) [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [AddCommGroup R] [IsTopologicalAddGroup R] (g : C(OnePoint X, R)) : (toZeroAtInftyAddMonoidHom X R) g = g.toZeroAtInfty

def ContinuousMap.toZeroAtInftyLinearMap (X : Type u_1) (R : Type u_2) (S : Type u_3) [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [AddCommGroup R] [IsTopologicalAddGroup R] [Semiring S] [Module S R] [ContinuousConstSMul S R] : C(OnePoint X, R) →ₗ[S] ZeroAtInftyContinuousMap X R

ContinuousMap.toZeroAtInfty as a LinearMap.

Equations

• ContinuousMap.toZeroAtInftyLinearMap X R S = { toFun := ContinuousMap.toZeroAtInfty, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem ContinuousMap.toZeroAtInftyLinearMap_apply (X : Type u_1) (R : Type u_2) (S : Type u_3) [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [AddCommGroup R] [IsTopologicalAddGroup R] [Semiring S] [Module S R] [ContinuousConstSMul S R] (g : C(OnePoint X, R)) : (toZeroAtInftyLinearMap X R S) g = g.toZeroAtInfty

@[simp]

theorem ContinuousMap.toAddMonoidHom_toZeroAtInftyLinearMap (X : Type u_1) (R : Type u_2) (S : Type u_3) [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [AddCommGroup R] [IsTopologicalAddGroup R] [Semiring S] [Module S R] [ContinuousConstSMul S R] : (toZeroAtInftyLinearMap X R S).toAddMonoidHom = toZeroAtInftyAddMonoidHom X R

def ZeroAtInftyContinuousMap.unitizationEquiv (X : Type u_1) (R : Type u_2) [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [AddCommGroup R] [IsTopologicalAddGroup R] : Unitization R (ZeroAtInftyContinuousMap X R) ≃ C(OnePoint X, R)

The canonical equivalence Unitization R C₀(X, R) ≃ C(OnePoint X, R) mapping (r, f) to the function taking the value r at ∞ and r + f x at x : X. Its inverse maps g to (g ∞, fun x ↦ g x - g ∞). This is the lift of ZeroAtInftyContinuousMap.toOnePoint.

Various bundlings are available including unitizationAddEquiv, unitizationLinearEquiv, unitizationRingEquiv, unitizationAlgEquiv, unitizationStarAlgEquiv.

Equations

• One or more equations did not get rendered due to their size.

theorem ZeroAtInftyContinuousMap.unitizationEquiv_apply {X : Type u_1} {R : Type u_2} [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [AddCommGroup R] [IsTopologicalAddGroup R] (f : Unitization R (ZeroAtInftyContinuousMap X R)) : (unitizationEquiv X R) f = ContinuousMap.const (OnePoint X) f.toProd.1 + f.toProd.2.toOnePoint

theorem ZeroAtInftyContinuousMap.unitizationEquiv_symm_apply {X : Type u_1} {R : Type u_2} [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [AddCommGroup R] [IsTopologicalAddGroup R] (g : C(OnePoint X, R)) : (unitizationEquiv X R).symm g = Unitization.mk (g OnePoint.infty, g.toZeroAtInfty)

@[simp]

theorem ZeroAtInftyContinuousMap.unitizationEquiv_apply_infty {X : Type u_1} {R : Type u_2} [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [AddCommGroup R] [IsTopologicalAddGroup R] (f : Unitization R (ZeroAtInftyContinuousMap X R)) : ((unitizationEquiv X R) f) OnePoint.infty = f.toProd.1

@[simp]

theorem ZeroAtInftyContinuousMap.unitizationEquiv_apply_coe {X : Type u_1} {R : Type u_2} [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [AddCommGroup R] [IsTopologicalAddGroup R] (f : Unitization R (ZeroAtInftyContinuousMap X R)) (x : X) : ((unitizationEquiv X R) f) ↑x = f.toProd.1 + f.toProd.2 x

@[simp]

theorem ZeroAtInftyContinuousMap.unitizationEquiv_inl {X : Type u_1} {R : Type u_2} [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [AddCommGroup R] [IsTopologicalAddGroup R] (r : R) : (unitizationEquiv X R) (Unitization.inl r) = ContinuousMap.const (OnePoint X) r

@[simp]

theorem ZeroAtInftyContinuousMap.unitizationEquiv_inr {X : Type u_1} {R : Type u_2} [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [AddCommGroup R] [IsTopologicalAddGroup R] (f : ZeroAtInftyContinuousMap X R) : (unitizationEquiv X R) ↑f = f.toOnePoint

@[simp]

theorem ZeroAtInftyContinuousMap.unitizationEquiv_zero {X : Type u_1} {R : Type u_2} [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [AddCommGroup R] [IsTopologicalAddGroup R] : (unitizationEquiv X R) 0 = 0

@[simp]

theorem ZeroAtInftyContinuousMap.unitizationEquiv_add {X : Type u_1} {R : Type u_2} [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [AddCommGroup R] [IsTopologicalAddGroup R] (f g : Unitization R (ZeroAtInftyContinuousMap X R)) : (unitizationEquiv X R) (f + g) = (unitizationEquiv X R) f + (unitizationEquiv X R) g

@[simp]

theorem ZeroAtInftyContinuousMap.unitizationEquiv_neg {X : Type u_1} {R : Type u_2} [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [AddCommGroup R] [IsTopologicalAddGroup R] (f : Unitization R (ZeroAtInftyContinuousMap X R)) : (unitizationEquiv X R) (-f) = -(unitizationEquiv X R) f

@[simp]

theorem ZeroAtInftyContinuousMap.unitizationEquiv_sub {X : Type u_1} {R : Type u_2} [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [AddCommGroup R] [IsTopologicalAddGroup R] (f g : Unitization R (ZeroAtInftyContinuousMap X R)) : (unitizationEquiv X R) (f - g) = (unitizationEquiv X R) f - (unitizationEquiv X R) g

@[simp]

theorem ZeroAtInftyContinuousMap.unitizationEquiv_star {X : Type u_1} {R : Type u_2} [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [AddCommGroup R] [IsTopologicalAddGroup R] [StarAddMonoid R] [ContinuousStar R] (f : Unitization R (ZeroAtInftyContinuousMap X R)) : (unitizationEquiv X R) (star f) = star ((unitizationEquiv X R) f)

def ZeroAtInftyContinuousMap.unitizationAddEquiv (X : Type u_1) (R : Type u_2) [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [AddCommGroup R] [IsTopologicalAddGroup R] : Unitization R (ZeroAtInftyContinuousMap X R) ≃+ C(OnePoint X, R)

ZeroAtInftyContinuousMap.unitizationEquiv as an AddEquiv.

Equations

• ZeroAtInftyContinuousMap.unitizationAddEquiv X R = { toEquiv := ZeroAtInftyContinuousMap.unitizationEquiv X R, map_add' := ⋯ }

@[simp]

theorem ZeroAtInftyContinuousMap.coe_unitizationAddEquiv {X : Type u_1} {R : Type u_2} [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [AddCommGroup R] [IsTopologicalAddGroup R] : ⇑(unitizationAddEquiv X R) = ⇑(unitizationEquiv X R)

@[simp]

theorem ZeroAtInftyContinuousMap.coe_unitizationAddEquiv_symm {X : Type u_1} {R : Type u_2} [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [AddCommGroup R] [IsTopologicalAddGroup R] : ⇑(unitizationAddEquiv X R).symm = ⇑(unitizationEquiv X R).symm

theorem ZeroAtInftyContinuousMap.toEquiv_unitizationAddEquiv {X : Type u_1} {R : Type u_2} [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [AddCommGroup R] [IsTopologicalAddGroup R] : (unitizationAddEquiv X R).toEquiv = unitizationEquiv X R

@[simp]

theorem ZeroAtInftyContinuousMap.unitizationEquiv_smul {X : Type u_1} {R : Type u_2} {S : Type u_3} [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [AddCommGroup R] [IsTopologicalAddGroup R] [Semiring S] [Module S R] [ContinuousConstSMul S R] (s : S) (f : Unitization R (ZeroAtInftyContinuousMap X R)) : (unitizationEquiv X R) (s • f) = s • (unitizationEquiv X R) f

def ZeroAtInftyContinuousMap.unitizationLinearEquiv (X : Type u_1) (R : Type u_2) (S : Type u_3) [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [AddCommGroup R] [IsTopologicalAddGroup R] [Semiring S] [Module S R] [ContinuousConstSMul S R] : Unitization R (ZeroAtInftyContinuousMap X R) ≃ₗ[S] C(OnePoint X, R)

ZeroAtInftyContinuousMap.unitizationEquiv as a LinearEquiv.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ZeroAtInftyContinuousMap.coe_unitizationLinearEquiv {X : Type u_1} {R : Type u_2} {S : Type u_3} [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [AddCommGroup R] [IsTopologicalAddGroup R] [Semiring S] [Module S R] [ContinuousConstSMul S R] : ⇑(unitizationLinearEquiv X R S) = ⇑(unitizationEquiv X R)

@[simp]

theorem ZeroAtInftyContinuousMap.coe_unitizationLinearEquiv_symm {X : Type u_1} {R : Type u_2} {S : Type u_3} [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [AddCommGroup R] [IsTopologicalAddGroup R] [Semiring S] [Module S R] [ContinuousConstSMul S R] : ⇑(unitizationLinearEquiv X R S).symm = ⇑(unitizationEquiv X R).symm

@[simp]

theorem ZeroAtInftyContinuousMap.toAddEquiv_unitizationLinearEquiv {X : Type u_1} {R : Type u_2} {S : Type u_3} [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [AddCommGroup R] [IsTopologicalAddGroup R] [Semiring S] [Module S R] [ContinuousConstSMul S R] : (unitizationLinearEquiv X R S).toAddEquiv = unitizationAddEquiv X R

@[simp]

theorem ZeroAtInftyContinuousMap.unitizationEquiv_one {X : Type u_1} {R : Type u_2} [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [CommRing R] [IsTopologicalRing R] : (unitizationEquiv X R) 1 = 1

@[simp]

theorem ZeroAtInftyContinuousMap.unitizationEquiv_mul {X : Type u_1} {R : Type u_2} [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [CommRing R] [IsTopologicalRing R] (f g : Unitization R (ZeroAtInftyContinuousMap X R)) : (unitizationEquiv X R) (f * g) = (unitizationEquiv X R) f * (unitizationEquiv X R) g

def ZeroAtInftyContinuousMap.unitizationRingEquiv (X : Type u_1) (R : Type u_2) [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [CommRing R] [IsTopologicalRing R] : Unitization R (ZeroAtInftyContinuousMap X R) ≃+* C(OnePoint X, R)

ZeroAtInftyContinuousMap.unitizationEquiv as a RingEquiv.

Equations

• ZeroAtInftyContinuousMap.unitizationRingEquiv X R = { toEquiv := (ZeroAtInftyContinuousMap.unitizationAddEquiv X R).toEquiv, map_mul' := ⋯, map_add' := ⋯ }

@[simp]

theorem ZeroAtInftyContinuousMap.coe_unitizationRingEquiv {X : Type u_1} {R : Type u_2} [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [CommRing R] [IsTopologicalRing R] : ⇑(unitizationRingEquiv X R) = ⇑(unitizationEquiv X R)

@[simp]

theorem ZeroAtInftyContinuousMap.coe_unitizationRingEquiv_symm {X : Type u_1} {R : Type u_2} [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [CommRing R] [IsTopologicalRing R] : ⇑(unitizationRingEquiv X R).symm = ⇑(unitizationEquiv X R).symm

theorem ZeroAtInftyContinuousMap.toAddEquiv_unitizationRingEquiv {X : Type u_1} {R : Type u_2} [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [CommRing R] [IsTopologicalRing R] : (unitizationRingEquiv X R).toAddEquiv = unitizationAddEquiv X R

@[simp]

theorem ZeroAtInftyContinuousMap.unitizationEquiv_algebraMap {X : Type u_1} {R : Type u_2} {S : Type u_3} [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [CommRing R] [IsTopologicalRing R] [CommSemiring S] [Algebra S R] (s : S) : (unitizationEquiv X R) ((algebraMap S (Unitization R (ZeroAtInftyContinuousMap X R))) s) = (algebraMap S C(OnePoint X, R)) s

def ZeroAtInftyContinuousMap.unitizationAlgEquiv (X : Type u_1) (R : Type u_2) (S : Type u_3) [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [CommRing R] [IsTopologicalRing R] [CommSemiring S] [Algebra S R] : Unitization R (ZeroAtInftyContinuousMap X R) ≃ₐ[S] C(OnePoint X, R)

ZeroAtInftyContinuousMap.unitizationEquiv as an AlgEquiv.

Equations

• ZeroAtInftyContinuousMap.unitizationAlgEquiv X R S = { toEquiv := (ZeroAtInftyContinuousMap.unitizationRingEquiv X R).toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

@[simp]

theorem ZeroAtInftyContinuousMap.coe_unitizationAlgEquiv {X : Type u_1} {R : Type u_2} {S : Type u_3} [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [CommRing R] [IsTopologicalRing R] [CommSemiring S] [Algebra S R] : ⇑(unitizationAlgEquiv X R S) = ⇑(unitizationEquiv X R)

@[simp]

theorem ZeroAtInftyContinuousMap.coe_unitizationAlgEquiv_symm {X : Type u_1} {R : Type u_2} {S : Type u_3} [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [CommRing R] [IsTopologicalRing R] [CommSemiring S] [Algebra S R] : ⇑(unitizationAlgEquiv X R S).symm = ⇑(unitizationEquiv X R).symm

@[simp]

theorem ZeroAtInftyContinuousMap.toRingEquiv_unitizationAlgEquiv {X : Type u_1} {R : Type u_2} {S : Type u_3} [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [CommRing R] [IsTopologicalRing R] [CommSemiring S] [Algebra S R] : (unitizationAlgEquiv X R S).toRingEquiv = unitizationRingEquiv X R

@[simp]

theorem ZeroAtInftyContinuousMap.toLinearEquiv_unitizationAlgEquiv {X : Type u_1} {R : Type u_2} {S : Type u_3} [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [CommRing R] [IsTopologicalRing R] [CommSemiring S] [Algebra S R] : ↑(unitizationAlgEquiv X R S) = unitizationLinearEquiv X R S

def ZeroAtInftyContinuousMap.unitizationStarAlgEquiv (X : Type u_1) (R : Type u_2) (S : Type u_3) [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [CommRing R] [IsTopologicalRing R] [CommSemiring S] [Algebra S R] [StarRing R] [ContinuousStar R] : Unitization R (ZeroAtInftyContinuousMap X R) ≃⋆ₐ[S] C(OnePoint X, R)

ZeroAtInftyContinuousMap.unitizationEquiv as a StarAlgEquiv.

Equations

• ZeroAtInftyContinuousMap.unitizationStarAlgEquiv X R S = { toRingEquiv := ZeroAtInftyContinuousMap.unitizationRingEquiv X R, map_star' := ⋯, map_smul' := ⋯ }

@[simp]

theorem ZeroAtInftyContinuousMap.coe_unitizationStarAlgEquiv {X : Type u_1} {R : Type u_2} {S : Type u_3} [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [CommRing R] [IsTopologicalRing R] [CommSemiring S] [Algebra S R] [StarRing R] [ContinuousStar R] : ⇑(unitizationStarAlgEquiv X R S) = ⇑(unitizationEquiv X R)

@[simp]

theorem ZeroAtInftyContinuousMap.coe_unitizationStarAlgEquiv_symm {X : Type u_1} {R : Type u_2} {S : Type u_3} [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [CommRing R] [IsTopologicalRing R] [CommSemiring S] [Algebra S R] [StarRing R] [ContinuousStar R] : ⇑(unitizationStarAlgEquiv X R S).symm = ⇑(unitizationEquiv X R).symm

@[simp]

theorem ZeroAtInftyContinuousMap.toAlgEquiv_unitizationStarAlgEquiv {X : Type u_1} {R : Type u_2} {S : Type u_3} [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [CommRing R] [IsTopologicalRing R] [CommSemiring S] [Algebra S R] [StarRing R] [ContinuousStar R] : (unitizationStarAlgEquiv X R S).toAlgEquiv = unitizationAlgEquiv X R S

theorem ZeroAtInftyContinuousMap.coe_starLift_toOnePointNonUnitalStarAlgHom {X : Type u_1} {R : Type u_2} [TopologicalSpace X] [R1Space X] [TopologicalSpace R] [CommRing R] [IsTopologicalRing R] [StarRing R] [ContinuousStar R] : ⇑(Unitization.starLift (toOnePointNonUnitalStarAlgHom X R R)) = ⇑(unitizationEquiv X R)

ZeroAtInftyContinuousMap.unitizationStarAlgEquiv is the map obtained lifting ZeroAtInftyContinuousMap.toOnePoint to the unitization.