# Algebraic structures over continuous functions #

In this file we define instances of algebraic structures over the type ContinuousMap α β (denoted C(α, β)) of bundled continuous maps from α to β. For example, C(α, β) is a group when β is a group, a ring when β is a ring, etc.

For each type of algebraic structure, we also define an appropriate subobject of α → β with carrier { f : α → β | Continuous f }. For example, when β is a group, a subgroup continuousSubgroup α β of α → β is constructed with carrier { f : α → β | Continuous f }.

Note that, rather than using the derived algebraic structures on these subobjects (for example, when β is a group, the derived group structure on continuousSubgroup α β), one should use C(α, β) with the appropriate instance of the structure.

instance ContinuousFunctions.instCoeFunElemForallSetOfContinuous {α : Type u_1} {β : Type u_2} [] [] :
CoeFun {f : αβ | } fun (x : {f : αβ | }) => αβ
Equations
• ContinuousFunctions.instCoeFunElemForallSetOfContinuous = { coe := Subtype.val }

### mul and add#

theorem ContinuousMap.instAdd.proof_1 {α : Type u_1} {β : Type u_2} [] [] [Add β] [] (f : C(α, β)) (g : C(α, β)) :
Continuous ((fun (p : β × β) => p.1 + p.2) fun (x : α) => (f x, g x))
instance ContinuousMap.instAdd {α : Type u_1} {β : Type u_2} [] [] [Add β] [] :
Equations
• ContinuousMap.instAdd = { add := fun (f g : C(α, β)) => { toFun := f + g, continuous_toFun := } }
instance ContinuousMap.instMul {α : Type u_1} {β : Type u_2} [] [] [Mul β] [] :
Mul C(α, β)
Equations
• ContinuousMap.instMul = { mul := fun (f g : C(α, β)) => { toFun := f * g, continuous_toFun := } }
@[simp]
theorem ContinuousMap.coe_add {α : Type u_1} {β : Type u_2} [] [] [Add β] [] (f : C(α, β)) (g : C(α, β)) :
(f + g) = f + g
@[simp]
theorem ContinuousMap.coe_mul {α : Type u_1} {β : Type u_2} [] [] [Mul β] [] (f : C(α, β)) (g : C(α, β)) :
(f * g) = f * g
@[simp]
theorem ContinuousMap.add_apply {α : Type u_1} {β : Type u_2} [] [] [Add β] [] (f : C(α, β)) (g : C(α, β)) (x : α) :
(f + g) x = f x + g x
@[simp]
theorem ContinuousMap.mul_apply {α : Type u_1} {β : Type u_2} [] [] [Mul β] [] (f : C(α, β)) (g : C(α, β)) (x : α) :
(f * g) x = f x * g x
@[simp]
theorem ContinuousMap.add_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] [Add γ] [] (f₁ : C(β, γ)) (f₂ : C(β, γ)) (g : C(α, β)) :
(f₁ + f₂).comp g = f₁.comp g + f₂.comp g
@[simp]
theorem ContinuousMap.mul_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] [Mul γ] [] (f₁ : C(β, γ)) (f₂ : C(β, γ)) (g : C(α, β)) :
(f₁ * f₂).comp g = f₁.comp g * f₂.comp g

### one#

instance ContinuousMap.instZero {α : Type u_1} {β : Type u_2} [] [] [Zero β] :
Zero C(α, β)
Equations
• ContinuousMap.instZero = { zero := }
instance ContinuousMap.instOne {α : Type u_1} {β : Type u_2} [] [] [One β] :
One C(α, β)
Equations
• ContinuousMap.instOne = { one := }
@[simp]
theorem ContinuousMap.coe_zero {α : Type u_1} {β : Type u_2} [] [] [Zero β] :
0 = 0
@[simp]
theorem ContinuousMap.coe_one {α : Type u_1} {β : Type u_2} [] [] [One β] :
1 = 1
@[simp]
theorem ContinuousMap.zero_apply {α : Type u_1} {β : Type u_2} [] [] [Zero β] (x : α) :
0 x = 0
@[simp]
theorem ContinuousMap.one_apply {α : Type u_1} {β : Type u_2} [] [] [One β] (x : α) :
1 x = 1
@[simp]
theorem ContinuousMap.zero_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] [Zero γ] (g : C(α, β)) :
= 0
@[simp]
theorem ContinuousMap.one_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] [One γ] (g : C(α, β)) :
= 1

### Nat.cast#

instance ContinuousMap.instNatCast {α : Type u_1} {β : Type u_2} [] [] [] :
Equations
• ContinuousMap.instNatCast = { natCast := fun (n : ) => }
@[simp]
theorem ContinuousMap.coe_natCast {α : Type u_1} {β : Type u_2} [] [] [] (n : ) :
n = n
@[simp]
theorem ContinuousMap.natCast_apply {α : Type u_1} {β : Type u_2} [] [] [] (n : ) (x : α) :
n x = n

### Int.cast#

instance ContinuousMap.instIntCast {α : Type u_1} {β : Type u_2} [] [] [] :
Equations
• ContinuousMap.instIntCast = { intCast := fun (n : ) => }
@[simp]
theorem ContinuousMap.coe_intCast {α : Type u_1} {β : Type u_2} [] [] [] (n : ) :
n = n
@[simp]
theorem ContinuousMap.intCast_apply {α : Type u_1} {β : Type u_2} [] [] [] (n : ) (x : α) :
n x = n

### nsmul and pow#

instance ContinuousMap.instNSMul {α : Type u_1} {β : Type u_2} [] [] [] [] :
Equations
• ContinuousMap.instNSMul = { smul := fun (n : ) (f : C(α, β)) => { toFun := n f, continuous_toFun := } }
instance ContinuousMap.instPow {α : Type u_1} {β : Type u_2} [] [] [] [] :
Pow C(α, β)
Equations
• ContinuousMap.instPow = { pow := fun (f : C(α, β)) (n : ) => { toFun := f ^ n, continuous_toFun := } }
theorem ContinuousMap.coe_nsmul {α : Type u_1} {β : Type u_2} [] [] [] [] (n : ) (f : C(α, β)) :
(n f) = n f
@[simp]
theorem ContinuousMap.coe_pow {α : Type u_1} {β : Type u_2} [] [] [] [] (f : C(α, β)) (n : ) :
(f ^ n) = f ^ n
theorem ContinuousMap.nsmul_apply {α : Type u_1} {β : Type u_2} [] [] [] [] (f : C(α, β)) (n : ) (x : α) :
(n f) x = n f x
@[simp]
theorem ContinuousMap.pow_apply {α : Type u_1} {β : Type u_2} [] [] [] [] (f : C(α, β)) (n : ) (x : α) :
(f ^ n) x = f x ^ n
theorem ContinuousMap.nsmul_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] [] [] (f : C(β, γ)) (n : ) (g : C(α, β)) :
(n f).comp g = n f.comp g
@[simp]
theorem ContinuousMap.pow_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] [] [] (f : C(β, γ)) (n : ) (g : C(α, β)) :
(f ^ n).comp g = f.comp g ^ n

### inv and neg#

instance ContinuousMap.instNegOfContinuousNeg {α : Type u_1} {β : Type u_2} [] [] [Neg β] [] :
Neg C(α, β)
Equations
• ContinuousMap.instNegOfContinuousNeg = { neg := fun (f : C(α, β)) => { toFun := -f, continuous_toFun := } }
theorem ContinuousMap.instNegOfContinuousNeg.proof_1 {α : Type u_1} {β : Type u_2} [] [] [Neg β] [] (f : C(α, β)) :
Continuous fun (x : α) => -f x
instance ContinuousMap.instInvOfContinuousInv {α : Type u_1} {β : Type u_2} [] [] [Inv β] [] :
Inv C(α, β)
Equations
• ContinuousMap.instInvOfContinuousInv = { inv := fun (f : C(α, β)) => { toFun := (f)⁻¹, continuous_toFun := } }
@[simp]
theorem ContinuousMap.coe_neg {α : Type u_1} {β : Type u_2} [] [] [Neg β] [] (f : C(α, β)) :
(-f) = -f
@[simp]
theorem ContinuousMap.coe_inv {α : Type u_1} {β : Type u_2} [] [] [Inv β] [] (f : C(α, β)) :
f⁻¹ = (f)⁻¹
@[simp]
theorem ContinuousMap.neg_apply {α : Type u_1} {β : Type u_2} [] [] [Neg β] [] (f : C(α, β)) (x : α) :
(-f) x = -f x
@[simp]
theorem ContinuousMap.inv_apply {α : Type u_1} {β : Type u_2} [] [] [Inv β] [] (f : C(α, β)) (x : α) :
f⁻¹ x = (f x)⁻¹
@[simp]
theorem ContinuousMap.neg_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] [Neg γ] [] (f : C(β, γ)) (g : C(α, β)) :
(-f).comp g = -f.comp g
@[simp]
theorem ContinuousMap.inv_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] [Inv γ] [] (f : C(β, γ)) (g : C(α, β)) :
f⁻¹.comp g = (f.comp g)⁻¹

### div and sub#

theorem ContinuousMap.instSubOfContinuousSub.proof_1 {α : Type u_1} {β : Type u_2} [] [] [Sub β] [] (f : C(α, β)) (g : C(α, β)) :
Continuous fun (x : α) => f x - g x
instance ContinuousMap.instSubOfContinuousSub {α : Type u_1} {β : Type u_2} [] [] [Sub β] [] :
Sub C(α, β)
Equations
• ContinuousMap.instSubOfContinuousSub = { sub := fun (f g : C(α, β)) => { toFun := f - g, continuous_toFun := } }
instance ContinuousMap.instDivOfContinuousDiv {α : Type u_1} {β : Type u_2} [] [] [Div β] [] :
Div C(α, β)
Equations
• ContinuousMap.instDivOfContinuousDiv = { div := fun (f g : C(α, β)) => { toFun := f / g, continuous_toFun := } }
@[simp]
theorem ContinuousMap.coe_sub {α : Type u_1} {β : Type u_2} [] [] [Sub β] [] (f : C(α, β)) (g : C(α, β)) :
(f - g) = f - g
@[simp]
theorem ContinuousMap.coe_div {α : Type u_1} {β : Type u_2} [] [] [Div β] [] (f : C(α, β)) (g : C(α, β)) :
(f / g) = f / g
@[simp]
theorem ContinuousMap.sub_apply {α : Type u_1} {β : Type u_2} [] [] [Sub β] [] (f : C(α, β)) (g : C(α, β)) (x : α) :
(f - g) x = f x - g x
@[simp]
theorem ContinuousMap.div_apply {α : Type u_1} {β : Type u_2} [] [] [Div β] [] (f : C(α, β)) (g : C(α, β)) (x : α) :
(f / g) x = f x / g x
@[simp]
theorem ContinuousMap.sub_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] [Sub γ] [] (f : C(β, γ)) (g : C(β, γ)) (h : C(α, β)) :
(f - g).comp h = f.comp h - g.comp h
@[simp]
theorem ContinuousMap.div_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] [Div γ] [] (f : C(β, γ)) (g : C(β, γ)) (h : C(α, β)) :
(f / g).comp h = f.comp h / g.comp h

### zpow and zsmul#

instance ContinuousMap.instZSMul {α : Type u_1} {β : Type u_2} [] [] [] :
Equations
• ContinuousMap.instZSMul = { smul := fun (z : ) (f : C(α, β)) => { toFun := z f, continuous_toFun := } }
instance ContinuousMap.instZPow {α : Type u_1} {β : Type u_2} [] [] [] [] :
Pow C(α, β)
Equations
• ContinuousMap.instZPow = { pow := fun (f : C(α, β)) (z : ) => { toFun := f ^ z, continuous_toFun := } }
theorem ContinuousMap.coe_zsmul {α : Type u_1} {β : Type u_2} [] [] [] (z : ) (f : C(α, β)) :
(z f) = z f
@[simp]
theorem ContinuousMap.coe_zpow {α : Type u_1} {β : Type u_2} [] [] [] [] (f : C(α, β)) (z : ) :
(f ^ z) = f ^ z
theorem ContinuousMap.zsmul_apply {α : Type u_1} {β : Type u_2} [] [] [] (f : C(α, β)) (z : ) (x : α) :
(z f) x = z f x
@[simp]
theorem ContinuousMap.zpow_apply {α : Type u_1} {β : Type u_2} [] [] [] [] (f : C(α, β)) (z : ) (x : α) :
(f ^ z) x = f x ^ z
theorem ContinuousMap.zsmul_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] [] (f : C(β, γ)) (z : ) (g : C(α, β)) :
(z f).comp g = z f.comp g
@[simp]
theorem ContinuousMap.zpow_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] [] [] (f : C(β, γ)) (z : ) (g : C(α, β)) :
(f ^ z).comp g = f.comp g ^ z

### Group structure #

In this section we show that continuous functions valued in a topological group inherit the structure of a group.

theorem continuousAddSubmonoid.proof_2 (α : Type u_1) (β : Type u_2) [] [] [] :
Continuous fun (x : α) => 0
theorem continuousAddSubmonoid.proof_1 (α : Type u_1) (β : Type u_2) [] [] [] [] :
∀ {a b : αβ}, a {f : αβ | }b {f : αβ | }Continuous fun (x : α) => a x + b x
def continuousAddSubmonoid (α : Type u_1) (β : Type u_2) [] [] [] [] :

The AddSubmonoid of continuous maps α → β.

Equations
• = { carrier := {f : αβ | }, add_mem' := , zero_mem' := }
Instances For
def continuousSubmonoid (α : Type u_1) (β : Type u_2) [] [] [] [] :
Submonoid (αβ)

The Submonoid of continuous maps α → β.

Equations
• = { carrier := {f : αβ | }, mul_mem' := , one_mem' := }
Instances For
theorem continuousAddSubgroup.proof_1 (α : Type u_1) (β : Type u_2) [] [] [] :
∀ {x : αβ}, x ().carrierContinuous fun (x_1 : α) => -x x_1
def continuousAddSubgroup (α : Type u_1) (β : Type u_2) [] [] [] :

The AddSubgroup of continuous maps α → β.

Equations
• = let __src := ; { toAddSubmonoid := __src, neg_mem' := }
Instances For
def continuousSubgroup (α : Type u_1) (β : Type u_2) [] [] [] [] :
Subgroup (αβ)

The subgroup of continuous maps α → β.

Equations
• = let __src := ; { toSubmonoid := __src, inv_mem' := }
Instances For
theorem ContinuousMap.instAddSemigroupOfContinuousAdd.proof_1 {α : Type u_2} {β : Type u_1} [] [] [] [] (f : C(α, β)) (g : C(α, β)) :
(f + g) = f + g
instance ContinuousMap.instAddSemigroupOfContinuousAdd {α : Type u_1} {β : Type u_2} [] [] [] [] :
Equations
instance ContinuousMap.instSemigroupOfContinuousMul {α : Type u_1} {β : Type u_2} [] [] [] [] :
Equations
theorem ContinuousMap.instAddCommSemigroupOfContinuousAdd.proof_1 {α : Type u_2} {β : Type u_1} [] [] [] [] (f : C(α, β)) (g : C(α, β)) :
(f + g) = f + g
instance ContinuousMap.instAddCommSemigroupOfContinuousAdd {α : Type u_1} {β : Type u_2} [] [] [] [] :
Equations
instance ContinuousMap.instCommSemigroupOfContinuousMul {α : Type u_1} {β : Type u_2} [] [] [] [] :
Equations
theorem ContinuousMap.instAddZeroClassOfContinuousAdd.proof_1 {α : Type u_1} {β : Type u_2} [] [] [] :
0 = 0
instance ContinuousMap.instAddZeroClassOfContinuousAdd {α : Type u_1} {β : Type u_2} [] [] [] [] :
Equations
theorem ContinuousMap.instAddZeroClassOfContinuousAdd.proof_2 {α : Type u_2} {β : Type u_1} [] [] [] [] (f : C(α, β)) (g : C(α, β)) :
(f + g) = f + g
instance ContinuousMap.instMulOneClassOfContinuousMul {α : Type u_1} {β : Type u_2} [] [] [] [] :
Equations
instance ContinuousMap.instMulZeroClassOfContinuousMul {α : Type u_1} {β : Type u_2} [] [] [] [] :
Equations
instance ContinuousMap.instSemigroupWithZeroOfContinuousMul {α : Type u_1} {β : Type u_2} [] [] [] :
Equations
theorem ContinuousMap.instAddMonoidOfContinuousAdd.proof_1 {α : Type u_1} {β : Type u_2} [] [] [] :
0 = 0
theorem ContinuousMap.instAddMonoidOfContinuousAdd.proof_2 {α : Type u_2} {β : Type u_1} [] [] [] [] (f : C(α, β)) (g : C(α, β)) :
(f + g) = f + g
instance ContinuousMap.instAddMonoidOfContinuousAdd {α : Type u_1} {β : Type u_2} [] [] [] [] :
Equations
instance ContinuousMap.instMonoidOfContinuousMul {α : Type u_1} {β : Type u_2} [] [] [] [] :
Equations
instance ContinuousMap.instMonoidWithZeroOfContinuousMul {α : Type u_1} {β : Type u_2} [] [] [] [] :
Equations
instance ContinuousMap.instAddCommMonoidOfContinuousAdd {α : Type u_1} {β : Type u_2} [] [] [] [] :
Equations
theorem ContinuousMap.instAddCommMonoidOfContinuousAdd.proof_3 {α : Type u_2} {β : Type u_1} [] [] [] [] (f : C(α, β)) (n : ) :
(n f) = n f
theorem ContinuousMap.instAddCommMonoidOfContinuousAdd.proof_1 {α : Type u_1} {β : Type u_2} [] [] [] :
0 = 0
theorem ContinuousMap.instAddCommMonoidOfContinuousAdd.proof_2 {α : Type u_2} {β : Type u_1} [] [] [] [] (f : C(α, β)) (g : C(α, β)) :
(f + g) = f + g
instance ContinuousMap.instCommMonoidOfContinuousMul {α : Type u_1} {β : Type u_2} [] [] [] [] :
Equations
instance ContinuousMap.instCommMonoidWithZeroOfContinuousMul {α : Type u_1} {β : Type u_2} [] [] [] :
Equations
instance ContinuousMap.instContinuousAddOfLocallyCompactSpace {α : Type u_1} {β : Type u_2} [] [] [Add β] [] :
Equations
• =
instance ContinuousMap.instContinuousMulOfLocallyCompactSpace {α : Type u_1} {β : Type u_2} [] [] [Mul β] [] :
Equations
• =
theorem ContinuousMap.coeFnAddMonoidHom.proof_2 {α : Type u_2} {β : Type u_1} [] [] [] [] (f : C(α, β)) (g : C(α, β)) :
(f + g) = f + g
theorem ContinuousMap.coeFnAddMonoidHom.proof_1 {α : Type u_1} {β : Type u_2} [] [] [] :
0 = 0
def ContinuousMap.coeFnAddMonoidHom {α : Type u_1} {β : Type u_2} [] [] [] [] :
C(α, β) →+ αβ

Coercion to a function as an AddMonoidHom. Similar to AddMonoidHom.coeFn.

Equations
• ContinuousMap.coeFnAddMonoidHom = { toFun := fun (f : C(α, β)) => f, map_zero' := , map_add' := }
Instances For
@[simp]
theorem ContinuousMap.coeFnMonoidHom_apply {α : Type u_1} {β : Type u_2} [] [] [] [] (f : C(α, β)) (a : α) :
ContinuousMap.coeFnMonoidHom f a = f a
@[simp]
theorem ContinuousMap.coeFnAddMonoidHom_apply {α : Type u_1} {β : Type u_2} [] [] [] [] (f : C(α, β)) (a : α) :
ContinuousMap.coeFnAddMonoidHom f a = f a
def ContinuousMap.coeFnMonoidHom {α : Type u_1} {β : Type u_2} [] [] [] [] :
C(α, β) →* αβ

Coercion to a function as a MonoidHom. Similar to MonoidHom.coeFn.

Equations
• ContinuousMap.coeFnMonoidHom = { toFun := fun (f : C(α, β)) => f, map_one' := , map_mul' := }
Instances For
theorem AddMonoidHom.compLeftContinuous.proof_1 (α : Type u_1) {β : Type u_3} [] [] {γ : Type u_2} [] [] [] [] [] (g : β →+ γ) (hg : ) :
(fun (f : C(α, β)) => { toFun := g, continuous_toFun := hg }.comp f) 0 = 0
theorem AddMonoidHom.compLeftContinuous.proof_2 (α : Type u_2) {β : Type u_1} [] [] {γ : Type u_3} [] [] [] [] [] (g : β →+ γ) (hg : ) :
∀ (x x_1 : C(α, β)), { toFun := fun (f : C(α, β)) => { toFun := g, continuous_toFun := hg }.comp f, map_zero' := }.toFun (x + x_1) = { toFun := fun (f : C(α, β)) => { toFun := g, continuous_toFun := hg }.comp f, map_zero' := }.toFun x + { toFun := fun (f : C(α, β)) => { toFun := g, continuous_toFun := hg }.comp f, map_zero' := }.toFun x_1
def AddMonoidHom.compLeftContinuous (α : Type u_1) {β : Type u_2} [] [] {γ : Type u_3} [] [] [] [] [] (g : β →+ γ) (hg : ) :
C(α, β) →+ C(α, γ)

Composition on the left by a (continuous) homomorphism of topological AddMonoids, as an AddMonoidHom. Similar to AddMonoidHom.comp_left.

Equations
• = { toFun := fun (f : C(α, β)) => { toFun := g, continuous_toFun := hg }.comp f, map_zero' := , map_add' := }
Instances For
@[simp]
theorem AddMonoidHom.compLeftContinuous_apply (α : Type u_1) {β : Type u_2} [] [] {γ : Type u_3} [] [] [] [] [] (g : β →+ γ) (hg : ) (f : C(α, β)) :
() f = { toFun := g, continuous_toFun := hg }.comp f
@[simp]
theorem MonoidHom.compLeftContinuous_apply (α : Type u_1) {β : Type u_2} [] [] {γ : Type u_3} [] [] [] [] [] (g : β →* γ) (hg : ) (f : C(α, β)) :
() f = { toFun := g, continuous_toFun := hg }.comp f
def MonoidHom.compLeftContinuous (α : Type u_1) {β : Type u_2} [] [] {γ : Type u_3} [] [] [] [] [] (g : β →* γ) (hg : ) :
C(α, β) →* C(α, γ)

Composition on the left by a (continuous) homomorphism of topological monoids, as a MonoidHom. Similar to MonoidHom.compLeft.

Equations
• = { toFun := fun (f : C(α, β)) => { toFun := g, continuous_toFun := hg }.comp f, map_one' := , map_mul' := }
Instances For
theorem ContinuousMap.compAddMonoidHom'.proof_2 {α : Type u_3} {β : Type u_2} [] [] {γ : Type u_1} [] [] [] (g : C(α, β)) (f₁ : C(β, γ)) (f₂ : C(β, γ)) :
(f₁ + f₂).comp g = f₁.comp g + f₂.comp g
theorem ContinuousMap.compAddMonoidHom'.proof_1 {α : Type u_1} {β : Type u_3} [] [] {γ : Type u_2} [] [] (g : C(α, β)) :
= 0
def ContinuousMap.compAddMonoidHom' {α : Type u_1} {β : Type u_2} [] [] {γ : Type u_3} [] [] [] (g : C(α, β)) :
C(β, γ) →+ C(α, γ)

Composition on the right as an AddMonoidHom. Similar to AddMonoidHom.compHom'.

Equations
• g.compAddMonoidHom' = { toFun := fun (f : C(β, γ)) => f.comp g, map_zero' := , map_add' := }
Instances For
@[simp]
theorem ContinuousMap.compAddMonoidHom'_apply {α : Type u_1} {β : Type u_2} [] [] {γ : Type u_3} [] [] [] (g : C(α, β)) (f : C(β, γ)) :
@[simp]
theorem ContinuousMap.compMonoidHom'_apply {α : Type u_1} {β : Type u_2} [] [] {γ : Type u_3} [] [] [] (g : C(α, β)) (f : C(β, γ)) :
g.compMonoidHom' f = f.comp g
def ContinuousMap.compMonoidHom' {α : Type u_1} {β : Type u_2} [] [] {γ : Type u_3} [] [] [] (g : C(α, β)) :
C(β, γ) →* C(α, γ)

Composition on the right as a MonoidHom. Similar to MonoidHom.compHom'.

Equations
• g.compMonoidHom' = { toFun := fun (f : C(β, γ)) => f.comp g, map_one' := , map_mul' := }
Instances For
@[simp]
theorem ContinuousMap.coe_sum {α : Type u_1} {β : Type u_2} [] [] [] [] {ι : Type u_3} (s : ) (f : ιC(α, β)) :
(s.sum fun (i : ι) => f i) = s.sum fun (i : ι) => (f i)
@[simp]
theorem ContinuousMap.coe_prod {α : Type u_1} {β : Type u_2} [] [] [] [] {ι : Type u_3} (s : ) (f : ιC(α, β)) :
(s.prod fun (i : ι) => f i) = s.prod fun (i : ι) => (f i)
theorem ContinuousMap.sum_apply {α : Type u_1} {β : Type u_2} [] [] [] [] {ι : Type u_3} (s : ) (f : ιC(α, β)) (a : α) :
(s.sum fun (i : ι) => f i) a = s.sum fun (i : ι) => (f i) a
theorem ContinuousMap.prod_apply {α : Type u_1} {β : Type u_2} [] [] [] [] {ι : Type u_3} (s : ) (f : ιC(α, β)) (a : α) :
(s.prod fun (i : ι) => f i) a = s.prod fun (i : ι) => (f i) a
theorem ContinuousMap.instAddGroupOfTopologicalAddGroup.proof_4 {α : Type u_2} {β : Type u_1} [] [] [] (f : C(α, β)) (g : C(α, β)) :
(f - g) = f - g
theorem ContinuousMap.instAddGroupOfTopologicalAddGroup.proof_2 {α : Type u_2} {β : Type u_1} [] [] [] (f : C(α, β)) (g : C(α, β)) :
(f + g) = f + g
theorem ContinuousMap.instAddGroupOfTopologicalAddGroup.proof_1 {α : Type u_1} {β : Type u_2} [] [] [] :
0 = 0
theorem ContinuousMap.instAddGroupOfTopologicalAddGroup.proof_5 {α : Type u_2} {β : Type u_1} [] [] [] (f : C(α, β)) (n : ) :
(n f) = n f
instance ContinuousMap.instAddGroupOfTopologicalAddGroup {α : Type u_1} {β : Type u_2} [] [] [] :
Equations
theorem ContinuousMap.instAddGroupOfTopologicalAddGroup.proof_3 {α : Type u_2} {β : Type u_1} [] [] [] (f : C(α, β)) :
(-f) = -f
instance ContinuousMap.instGroupOfTopologicalGroup {α : Type u_1} {β : Type u_2} [] [] [] [] :
Group C(α, β)
Equations
theorem ContinuousMap.instAddCommGroupContinuousMap.proof_6 {α : Type u_2} {β : Type u_1} [] [] [] (f : C(α, β)) :
(-f) = -f
theorem ContinuousMap.instAddCommGroupContinuousMap.proof_7 {α : Type u_2} {β : Type u_1} [] [] [] (f : C(α, β)) (g : C(α, β)) :
(f - g) = f - g
theorem ContinuousMap.instAddCommGroupContinuousMap.proof_9 {α : Type u_2} {β : Type u_1} [] [] [] (f : C(α, β)) (z : ) :
(z f) = z f
instance ContinuousMap.instAddCommGroupContinuousMap {α : Type u_1} {β : Type u_2} [] [] [] :
Equations
theorem ContinuousMap.instAddCommGroupContinuousMap.proof_8 {α : Type u_2} {β : Type u_1} [] [] [] (f : C(α, β)) (n : ) :
(n f) = n f
theorem ContinuousMap.instAddCommGroupContinuousMap.proof_5 {α : Type u_2} {β : Type u_1} [] [] [] (f : C(α, β)) (g : C(α, β)) :
(f + g) = f + g
theorem ContinuousMap.instAddCommGroupContinuousMap.proof_4 {α : Type u_1} {β : Type u_2} [] [] [] :
0 = 0
instance ContinuousMap.instCommGroupContinuousMap {α : Type u_1} {β : Type u_2} [] [] [] [] :
Equations
instance ContinuousMap.instTopologicalAddGroup {α : Type u_1} {β : Type u_2} [] [] [] :
Equations
• =
instance ContinuousMap.instTopologicalGroup {α : Type u_1} {β : Type u_2} [] [] [] [] :
Equations
• =
theorem ContinuousMap.hasSum_apply {α : Type u_1} {β : Type u_2} [] [] {γ : Type u_3} [] [] {f : γC(α, β)} {g : C(α, β)} (hf : HasSum f g) (x : α) :
HasSum (fun (i : γ) => (f i) x) (g x)

If α is locally compact, and an infinite sum of functions in C(α, β) converges to g (for the compact-open topology), then the pointwise sum converges to g x for all x ∈ α.

theorem ContinuousMap.summable_apply {α : Type u_1} {β : Type u_2} [] [] [] [] {γ : Type u_3} {f : γC(α, β)} (hf : ) (x : α) :
Summable fun (i : γ) => (f i) x
theorem ContinuousMap.tsum_apply {α : Type u_1} {β : Type u_2} [] [] [] [] [] {γ : Type u_3} {f : γC(α, β)} (hf : ) (x : α) :
∑' (i : γ), (f i) x = (∑' (i : γ), f i) x

### Ring structure #

In this section we show that continuous functions valued in a topological semiring R inherit the structure of a ring.

def continuousSubsemiring (α : Type u_1) (R : Type u_2) [] [] [] :
Subsemiring (αR)

The subsemiring of continuous maps α → β.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def continuousSubring (α : Type u_1) (R : Type u_2) [] [] [Ring R] [] :
Subring (αR)

The subring of continuous maps α → β.

Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
Equations
instance ContinuousMap.instAddMonoidWithOneOfContinuousAdd {α : Type u_1} {β : Type u_2} [] [] [] [] :
Equations
instance ContinuousMap.instNonAssocSemiringOfTopologicalSemiring {α : Type u_1} {β : Type u_2} [] [] [] :
Equations
instance ContinuousMap.instSemiringOfTopologicalSemiring {α : Type u_1} {β : Type u_2} [] [] [] :
Equations
instance ContinuousMap.instNonUnitalNonAssocRingOfTopologicalRing {α : Type u_1} {β : Type u_2} [] [] [] :
Equations
instance ContinuousMap.instNonUnitalRingOfTopologicalRing {α : Type u_1} {β : Type u_2} [] [] [] [] :
Equations
instance ContinuousMap.instNonAssocRingOfTopologicalRing {α : Type u_1} {β : Type u_2} [] [] [] [] :
Equations
instance ContinuousMap.instRingContinuousMap {α : Type u_1} {β : Type u_2} [] [] [Ring β] [] :
Ring C(α, β)
Equations
• ContinuousMap.instRingContinuousMap = Function.Injective.ring DFunLike.coe
Equations
instance ContinuousMap.instCommSemiringOfTopologicalSemiring {α : Type u_1} {β : Type u_2} [] [] [] :
Equations
instance ContinuousMap.instNonUnitalCommRingOfTopologicalRing {α : Type u_1} {β : Type u_2} [] [] [] :
Equations
instance ContinuousMap.instCommRingOfTopologicalRing {α : Type u_1} {β : Type u_2} [] [] [] [] :
Equations
@[simp]
theorem RingHom.compLeftContinuous_apply_apply (α : Type u_1) {β : Type u_2} {γ : Type u_3} [] [] [] [] [] (g : β →+* γ) (hg : ) (f : C(α, β)) :
∀ (a : α), (() f) a = g (f a)
def RingHom.compLeftContinuous (α : Type u_1) {β : Type u_2} {γ : Type u_3} [] [] [] [] [] (g : β →+* γ) (hg : ) :
C(α, β) →+* C(α, γ)

Composition on the left by a (continuous) homomorphism of topological semirings, as a RingHom. Similar to RingHom.compLeft.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem ContinuousMap.coeFnRingHom_apply {α : Type u_1} {β : Type u_2} [] [] [] (f : C(α, β)) (a : α) :
ContinuousMap.coeFnRingHom f a = f a
def ContinuousMap.coeFnRingHom {α : Type u_1} {β : Type u_2} [] [] [] :
C(α, β) →+* αβ

Coercion to a function as a RingHom.

Equations
• ContinuousMap.coeFnRingHom = let __src := ContinuousMap.coeFnMonoidHom; let __src_1 := ContinuousMap.coeFnAddMonoidHom; { toMonoidHom := __src, map_zero' := , map_add' := }
Instances For

### Module structure #

In this section we show that continuous functions valued in a topological module M over a topological semiring R inherit the structure of a module.

def continuousSubmodule (α : Type u_1) [] (R : Type u_2) [] (M : Type u_3) [] [] [Module R M] [] :
Submodule R (αM)

The R-submodule of continuous maps α → M.

Equations
• = let __src := ; { carrier := {f : αM | }, add_mem' := , zero_mem' := , smul_mem' := }
Instances For
theorem ContinuousMap.instVAdd.proof_1 {α : Type u_1} [] {R : Type u_3} {M : Type u_2} [] [VAdd R M] [] (r : R) (f : C(α, M)) :
Continuous fun (x : α) => r +ᵥ f x
instance ContinuousMap.instVAdd {α : Type u_1} [] {R : Type u_3} {M : Type u_5} [] [VAdd R M] [] :
Equations
• ContinuousMap.instVAdd = { vadd := fun (r : R) (f : C(α, M)) => { toFun := r +ᵥ f, continuous_toFun := } }
instance ContinuousMap.instSMul {α : Type u_1} [] {R : Type u_3} {M : Type u_5} [] [SMul R M] [] :
SMul R C(α, M)
Equations
• ContinuousMap.instSMul = { smul := fun (r : R) (f : C(α, M)) => { toFun := r f, continuous_toFun := } }
instance ContinuousMap.instContinuousConstVAddOfLocallyCompactSpace {α : Type u_1} [] {R : Type u_3} {M : Type u_5} [] [VAdd R M] [] :
Equations
• =
instance ContinuousMap.instContinuousConstSMulOfLocallyCompactSpace {α : Type u_1} [] {R : Type u_3} {M : Type u_5} [] [SMul R M] [] :
Equations
• =
instance ContinuousMap.instContinuousVAddOfLocallyCompactSpace {α : Type u_1} [] {R : Type u_3} {M : Type u_5} [] [] [VAdd R M] [] :
Equations
• =
instance ContinuousMap.instContinuousSMulOfLocallyCompactSpace {α : Type u_1} [] {R : Type u_3} {M : Type u_5} [] [] [SMul R M] [] :
Equations
• =
@[simp]
theorem ContinuousMap.coe_vadd {α : Type u_1} [] {R : Type u_3} {M : Type u_5} [] [VAdd R M] [] (c : R) (f : C(α, M)) :
(c +ᵥ f) = c +ᵥ f
@[simp]
theorem ContinuousMap.coe_smul {α : Type u_1} [] {R : Type u_3} {M : Type u_5} [] [SMul R M] [] (c : R) (f : C(α, M)) :
(c f) = c f
theorem ContinuousMap.vadd_apply {α : Type u_1} [] {R : Type u_3} {M : Type u_5} [] [VAdd R M] [] (c : R) (f : C(α, M)) (a : α) :
(c +ᵥ f) a = c +ᵥ f a
theorem ContinuousMap.smul_apply {α : Type u_1} [] {R : Type u_3} {M : Type u_5} [] [SMul R M] [] (c : R) (f : C(α, M)) (a : α) :
(c f) a = c f a
@[simp]
theorem ContinuousMap.vadd_comp {α : Type u_1} {β : Type u_2} [] [] {R : Type u_3} {M : Type u_5} [] [VAdd R M] [] (r : R) (f : C(β, M)) (g : C(α, β)) :
(r +ᵥ f).comp g = r +ᵥ f.comp g
@[simp]
theorem ContinuousMap.smul_comp {α : Type u_1} {β : Type u_2} [] [] {R : Type u_3} {M : Type u_5} [] [SMul R M] [] (r : R) (f : C(β, M)) (g : C(α, β)) :
(r f).comp g = r f.comp g
instance ContinuousMap.instVAddCommClass {α : Type u_1} [] {R : Type u_3} {R₁ : Type u_4} {M : Type u_5} [] [VAdd R M] [] [VAdd R₁ M] [] [VAddCommClass R R₁ M] :
Equations
• =
instance ContinuousMap.instSMulCommClass {α : Type u_1} [] {R : Type u_3} {R₁ : Type u_4} {M : Type u_5} [] [SMul R M] [] [SMul R₁ M] [] [SMulCommClass R R₁ M] :
SMulCommClass R R₁ C(α, M)
Equations
• =
instance ContinuousMap.instIsScalarTower {α : Type u_1} [] {R : Type u_3} {R₁ : Type u_4} {M : Type u_5} [] [SMul R M] [] [SMul R₁ M] [] [SMul R R₁] [IsScalarTower R R₁ M] :
IsScalarTower R R₁ C(α, M)
Equations
• =
instance ContinuousMap.instIsCentralScalar {α : Type u_1} [] {R : Type u_3} {M : Type u_5} [] [SMul R M] [SMul Rᵐᵒᵖ M] [] [] :
Equations
• =
instance ContinuousMap.instMulActionOfContinuousConstSMul {α : Type u_1} [] {R : Type u_3} {M : Type u_5} [] [] [] [] :
Equations
instance ContinuousMap.instDistribMulActionOfContinuousConstSMul {α : Type u_1} [] {R : Type u_3} {M : Type u_5} [] [] [] [] [] [] :
Equations
instance ContinuousMap.module {α : Type u_1} [] {R : Type u_3} {M : Type u_5} [] [] [] [] [Module R M] [] :
Module R C(α, M)
Equations
@[simp]
theorem ContinuousLinearMap.compLeftContinuous_apply (R : Type u_3) {M : Type u_5} [] {M₂ : Type u_6} [] [] [] [] [] [Module R M] [] [] [Module R M₂] [] (α : Type u_7) [] (g : M →L[R] M₂) :
def ContinuousLinearMap.compLeftContinuous (R : Type u_3) {M : Type u_5} [] {M₂ : Type u_6} [] [] [] [] [] [Module R M] [] [] [Module R M₂] [] (α : Type u_7) [] (g : M →L[R] M₂) :
C(α, M) →ₗ[R] C(α, M₂)

Composition on the left by a continuous linear map, as a LinearMap. Similar to LinearMap.compLeft.

Equations
Instances For
@[simp]
theorem ContinuousMap.coeFnLinearMap_apply {α : Type u_1} [] (R : Type u_3) {M : Type u_5} [] [] [] [] [Module R M] [] :
∀ (a : C(α, M)) (a_1 : α), a a_1 = (ContinuousMap.coeFnAddMonoidHom).toFun a a_1
def ContinuousMap.coeFnLinearMap {α : Type u_1} [] (R : Type u_3) {M : Type u_5} [] [] [] [] [Module R M] [] :
C(α, M) →ₗ[R] αM

Coercion to a function as a LinearMap.

Equations
• = let __src := ContinuousMap.coeFnAddMonoidHom; { toFun := (__src).toFun, map_add' := , map_smul' := }
Instances For

### Algebra structure #

In this section we show that continuous functions valued in a topological algebra A over a ring R inherit the structure of an algebra. Note that the hypothesis that A is a topological algebra is obtained by requiring that A be both a ContinuousSMul and a TopologicalSemiring.

def continuousSubalgebra {α : Type u_1} [] {R : Type u_2} [] {A : Type u_3} [] [] [Algebra R A] :
Subalgebra R (αA)

The R-subalgebra of continuous maps α → A.

Equations
• continuousSubalgebra = let __src := ; { carrier := {f : αA | }, mul_mem' := , one_mem' := , add_mem' := , zero_mem' := , algebraMap_mem' := }
Instances For
def ContinuousMap.C {α : Type u_1} [] {R : Type u_2} [] {A : Type u_3} [] [] [Algebra R A] :
R →+* C(α, A)

Continuous constant functions as a RingHom.

Equations
• ContinuousMap.C = { toFun := fun (c : R) => { toFun := fun (x : α) => () c, continuous_toFun := }, map_one' := , map_mul' := , map_zero' := , map_add' := }
Instances For
@[simp]
theorem ContinuousMap.C_apply {α : Type u_1} [] {R : Type u_2} [] {A : Type u_3} [] [] [Algebra R A] (r : R) (a : α) :
(ContinuousMap.C r) a = () r
instance ContinuousMap.algebra {α : Type u_1} [] {R : Type u_2} [] {A : Type u_3} [] [] [Algebra R A] :
Equations
• ContinuousMap.algebra = Algebra.mk ContinuousMap.C
@[simp]
theorem AlgHom.compLeftContinuous_apply_apply (R : Type u_2) [] {A : Type u_3} [] [] [Algebra R A] {A₂ : Type u_4} [] [Semiring A₂] [Algebra R A₂] [] {α : Type u_5} [] (g : A →ₐ[R] A₂) (hg : ) (f : C(α, A)) :
∀ (a : α), (() f) a = g (f a)
def AlgHom.compLeftContinuous (R : Type u_2) [] {A : Type u_3} [] [] [Algebra R A] {A₂ : Type u_4} [] [Semiring A₂] [Algebra R A₂] [] {α : Type u_5} [] (g : A →ₐ[R] A₂) (hg : ) :
C(α, A) →ₐ[R] C(α, A₂)

Composition on the left by a (continuous) homomorphism of topological R-algebras, as an AlgHom. Similar to AlgHom.compLeft.

Equations
Instances For
@[simp]
theorem ContinuousMap.compRightAlgHom_apply (R : Type u_2) [] (A : Type u_3) [] [] [Algebra R A] {α : Type u_5} {β : Type u_6} [] [] (f : C(α, β)) (g : C(β, A)) :
() g = g.comp f
def ContinuousMap.compRightAlgHom (R : Type u_2) [] (A : Type u_3) [] [] [Algebra R A] {α : Type u_5} {β : Type u_6} [] [] (f : C(α, β)) :
C(β, A) →ₐ[R] C(α, A)

Precomposition of functions into a topological semiring by a continuous map is an algebra homomorphism.

Equations
• = { toFun := fun (g : C(β, A)) => g.comp f, map_one' := , map_mul' := , map_zero' := , map_add' := , commutes' := }
Instances For
@[simp]
theorem ContinuousMap.coeFnAlgHom_apply {α : Type u_1} [] (R : Type u_2) [] {A : Type u_3} [] [] [Algebra R A] (f : C(α, A)) (a : α) :
= f a
def ContinuousMap.coeFnAlgHom {α : Type u_1} [] (R : Type u_2) [] {A : Type u_3} [] [] [Algebra R A] :
C(α, A) →ₐ[R] αA

Coercion to a function as an AlgHom.

Equations
• = let __src := ContinuousMap.coeFnRingHom; { toRingHom := __src, commutes' := }
Instances For
@[reducible, inline]
abbrev Subalgebra.SeparatesPoints {α : Type u_1} [] {R : Type u_2} [] {A : Type u_3} [] [] [Algebra R A] (s : Subalgebra R C(α, A)) :

A version of Set.SeparatesPoints for subalgebras of the continuous functions, used for stating the Stone-Weierstrass theorem.

Equations
• s.SeparatesPoints = ((fun (f : C(α, A)) => f) '' s).SeparatesPoints
Instances For
theorem Subalgebra.separatesPoints_monotone {α : Type u_1} [] {R : Type u_2} [] {A : Type u_3} [] [] [Algebra R A] :
Monotone fun (s : Subalgebra R C(α, A)) => s.SeparatesPoints
@[simp]
theorem algebraMap_apply {α : Type u_1} [] {R : Type u_2} [] {A : Type u_3} [] [] [Algebra R A] (k : R) (a : α) :
((algebraMap R C(α, A)) k) a = k 1
def Set.SeparatesPointsStrongly {α : Type u_1} [] {𝕜 : Type u_5} [] (s : Set C(α, 𝕜)) :

A set of continuous maps "separates points strongly" if for each pair of distinct points there is a function with specified values on them.

We give a slightly unusual formulation, where the specified values are given by some function v, and we ask f x = v x ∧ f y = v y. This avoids needing a hypothesis x ≠ y.

In fact, this definition would work perfectly well for a set of non-continuous functions, but as the only current use case is in the Stone-Weierstrass theorem, writing it this way avoids having to deal with casts inside the set. (This may need to change if we do Stone-Weierstrass on non-compact spaces, where the functions would be continuous functions vanishing at infinity.)

Equations
• s.SeparatesPointsStrongly = ∀ (v : α𝕜) (x y : α), fs, f x = v x f y = v y
Instances For
theorem Subalgebra.SeparatesPoints.strongly {α : Type u_1} [] {𝕜 : Type u_5} [] [] [] {s : Subalgebra 𝕜 C(α, 𝕜)} (h : s.SeparatesPoints) :
(s).SeparatesPointsStrongly

Working in continuous functions into a topological field, a subalgebra of functions that separates points also separates points strongly.

By the hypothesis, we can find a function f so f x ≠ f y. By an affine transformation in the field we can arrange so that f x = a and f x = b.

instance ContinuousMap.subsingleton_subalgebra (α : Type u_1) [] (R : Type u_2) [] [] [] :
Equations
• =

### Structure as module over scalar functions #

If M is a module over R, then we show that the space of continuous functions from α to M is naturally a module over the ring of continuous functions from α to R.

instance ContinuousMap.instSMul' {α : Type u_1} [] {R : Type u_2} [] [] {M : Type u_3} [] [] [Module R M] [] :
SMul C(α, R) C(α, M)
Equations
• ContinuousMap.instSMul' = { smul := fun (f : C(α, R)) (g : C(α, M)) => { toFun := fun (x : α) => f x g x, continuous_toFun := } }
instance ContinuousMap.module' {α : Type u_1} [] (R : Type u_2) [] [] (M : Type u_3) [] [] [] [Module R M] [] :
Module C(α, R) C(α, M)
Equations

We now provide formulas for f ⊓ g and f ⊔ g, where f g : C(α, β), in terms of ContinuousMap.abs.

C(α, β)is a lattice ordered group

instance ContinuousMap.instCovariantClass_add_le_left {α : Type u_1} [] {β : Type u_2} [] [] [Add β] [] [CovariantClass β β (fun (x x_1 : β) => x + x_1) fun (x x_1 : β) => x x_1] :
CovariantClass C(α, β) C(α, β) (fun (x x_1 : C(α, β)) => x + x_1) fun (x x_1 : C(α, β)) => x x_1
Equations
• =
instance ContinuousMap.instCovariantClass_mul_le_left {α : Type u_1} [] {β : Type u_2} [] [] [Mul β] [] [CovariantClass β β (fun (x x_1 : β) => x * x_1) fun (x x_1 : β) => x x_1] :
CovariantClass C(α, β) C(α, β) (fun (x x_1 : C(α, β)) => x * x_1) fun (x x_1 : C(α, β)) => x x_1
Equations
• =
instance ContinuousMap.instCovariantClass_add_le_right {α : Type u_1} [] {β : Type u_2} [] [] [Add β] [] [CovariantClass β β (Function.swap fun (x x_1 : β) => x + x_1) fun (x x_1 : β) => x x_1] :
CovariantClass C(α, β) C(α, β) (Function.swap fun (x x_1 : C(α, β)) => x + x_1) fun (x x_1 : C(α, β)) => x x_1
Equations
• =
instance ContinuousMap.instCovariantClass_mul_le_right {α : Type u_1} [] {β : Type u_2} [] [] [Mul β] [] [CovariantClass β β (Function.swap fun (x x_1 : β) => x * x_1) fun (x x_1 : β) => x x_1] :
CovariantClass C(α, β) C(α, β) (Function.swap fun (x x_1 : C(α, β)) => x * x_1) fun (x x_1 : C(α, β)) => x x_1
Equations
• =
@[simp]
theorem ContinuousMap.coe_abs {α : Type u_1} [] {β : Type u_2} [] [] [] (f : C(α, β)) :
|f| = |f|
@[simp]
theorem ContinuousMap.coe_mabs {α : Type u_1} [] {β : Type u_2} [] [] [] [] (f : C(α, β)) :
(mabs f) = mabs f
@[simp]
theorem ContinuousMap.abs_apply {α : Type u_1} [] {β : Type u_2} [] [] [] (f : C(α, β)) (x : α) :
|f| x = |f x|
@[simp]
theorem ContinuousMap.mabs_apply {α : Type u_1} [] {β : Type u_2} [] [] [] [] (f : C(α, β)) (x : α) :
(mabs f) x = mabs (f x)

### Star structure #

If β has a continuous star operation, we put a star structure on C(α, β) by using the star operation pointwise.

If β is a ⋆-ring, then C(α, β) inherits a ⋆-ring structure.

If β is a ⋆-ring and a ⋆-module over R, then the space of continuous functions from α to β is a ⋆-module over R.

instance ContinuousMap.instStar {α : Type u_2} {β : Type u_3} [] [] [Star β] [] :
Star C(α, β)
Equations
• ContinuousMap.instStar = { star := fun (f : C(α, β)) => starContinuousMap.comp f }
@[simp]
theorem ContinuousMap.coe_star {α : Type u_2} {β : Type u_3} [] [] [Star β] [] (f : C(α, β)) :
(star f) = star f
@[simp]
theorem ContinuousMap.star_apply {α : Type u_2} {β : Type u_3} [] [] [Star β] [] (f : C(α, β)) (x : α) :
(star f) x = star (f x)
instance ContinuousMap.instTrivialStar {α : Type u_2} {β : Type u_3} [] [] [Star β] [] [] :
Equations
• =
instance ContinuousMap.instInvolutiveStarOfContinuousStar {α : Type u_2} {β : Type u_3} [] [] [] [] :
Equations
• ContinuousMap.instInvolutiveStarOfContinuousStar =
instance ContinuousMap.starAddMonoid {α : Type u_2} {β : Type u_3} [] [] [] [] [] [] :
Equations
instance ContinuousMap.starMul {α : Type u_2} {β : Type u_3} [] [] [Mul β] [] [] [] :
Equations
• ContinuousMap.starMul =
instance ContinuousMap.instStarRingOfContinuousStar {α : Type u_2} {β : Type u_3} [] [] [] [] :
Equations
• ContinuousMap.instStarRingOfContinuousStar = let __src := ContinuousMap.starAddMonoid; let __src_1 := ContinuousMap.starMul;
instance ContinuousMap.instStarModule {R : Type u_1} {α : Type u_2} {β : Type u_3} [] [] [Star R] [Star β] [SMul R β] [] [] [] :
Equations
• =
@[simp]
theorem ContinuousMap.compStarAlgHom'_apply {X : Type u_1} {Y : Type u_2} [] [] (𝕜 : Type u_4) [] (A : Type u_5) [] [] [Star A] [] [Algebra 𝕜 A] (f : C(X, Y)) (g : C(Y, A)) :
() g = g.comp f
def ContinuousMap.compStarAlgHom' {X : Type u_1} {Y : Type u_2} [] [] (𝕜 : Type u_4) [] (A : Type u_5) [] [] [Star A] [] [Algebra 𝕜 A] (f : C(X, Y)) :

The functorial map taking f : C(X, Y) to C(Y, A) →⋆ₐ[𝕜] C(X, A) given by pre-composition with the continuous function f. See ContinuousMap.compMonoidHom' and ContinuousMap.compAddMonoidHom', ContinuousMap.compRightAlgHom for bundlings of pre-composition into a MonoidHom, an AddMonoidHom and an AlgHom, respectively, under suitable assumptions on A.

Equations
• = { toFun := fun (g : C(Y, A)) => g.comp f, map_one' := , map_mul' := , map_zero' := , map_add' := , commutes' := , map_star' := }
Instances For
theorem ContinuousMap.compStarAlgHom'_id {X : Type u_1} [] (𝕜 : Type u_4) [] (A : Type u_5) [] [] [Star A] [] [Algebra 𝕜 A] :

ContinuousMap.compStarAlgHom' sends the identity continuous map to the identity StarAlgHom

theorem ContinuousMap.compStarAlgHom'_comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [] [] [] (𝕜 : Type u_4) [] (A : Type u_5) [] [] [Star A] [] [Algebra 𝕜 A] (g : C(Y, Z)) (f : C(X, Y)) :
ContinuousMap.compStarAlgHom' 𝕜 A (g.comp f) = ().comp ()

ContinuousMap.compStarAlgHom' is functorial.

@[simp]
theorem ContinuousMap.compStarAlgHom_apply (X : Type u_1) {𝕜 : Type u_2} {A : Type u_3} {B : Type u_4} [] [] [] [] [Star A] [] [Algebra 𝕜 A] [] [] [Star B] [] [Algebra 𝕜 B] (φ : A →⋆ₐ[𝕜] B) (hφ : ) (f : C(X, A)) :
() f = { toFun := φ, continuous_toFun := }.comp f
def ContinuousMap.compStarAlgHom (X : Type u_1) {𝕜 : Type u_2} {A : Type u_3} {B : Type u_4} [] [] [] [] [Star A] [] [Algebra 𝕜 A] [] [] [Star B] [] [Algebra 𝕜 B] (φ : A →⋆ₐ[𝕜] B) (hφ : ) :

Post-composition with a continuous star algebra homomorphism is a star algebra homomorphism between spaces of continuous maps.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem ContinuousMap.compStarAlgHom_id (X : Type u_1) {𝕜 : Type u_2} {A : Type u_3} [] [] [] [] [Star A] [] [Algebra 𝕜 A] :
=

ContinuousMap.compStarAlgHom sends the identity StarAlgHom on A to the identity StarAlgHom on C(X, A).

theorem ContinuousMap.compStarAlgHom_comp (X : Type u_1) {𝕜 : Type u_2} {A : Type u_3} {B : Type u_4} {C : Type u_5} [] [] [] [] [Star A] [] [Algebra 𝕜 A] [] [] [Star B] [] [Algebra 𝕜 B] [] [] [Star C] [] [Algebra 𝕜 C] (φ : A →⋆ₐ[𝕜] B) (ψ : B →⋆ₐ[𝕜] C) (hφ : ) (hψ : ) :
ContinuousMap.compStarAlgHom X (ψ.comp φ) = ().comp ()

ContinuousMap.compStarAlgHom is functorial.

### Summing translates of a function #

theorem ContinuousMap.periodic_tsum_comp_add_zsmul {X : Type u_1} {Y : Type u_2} [] [] [] [] [] [] (f : C(X, Y)) (p : X) :
Function.Periodic ((∑' (n : ), f.comp (ContinuousMap.addRight (n p)))) p

Summing the translates of f by ℤ • p gives a map which is periodic with period p. (This is true without any convergence conditions, since if the sum doesn't converge it is taken to be the zero map, which is periodic.)

@[simp]
theorem Homeomorph.compStarAlgEquiv'_apply {X : Type u_1} {Y : Type u_2} [] [] (𝕜 : Type u_3) [] (A : Type u_4) [] [] [] [] [Algebra 𝕜 A] (f : X ≃ₜ Y) (a : C(Y, A)) :
() a = (ContinuousMap.compStarAlgHom' 𝕜 A f.toContinuousMap) a
@[simp]
theorem Homeomorph.compStarAlgEquiv'_symm_apply {X : Type u_1} {Y : Type u_2} [] [] (𝕜 : Type u_3) [] (A : Type u_4) [] [] [] [] [Algebra 𝕜 A] (f : X ≃ₜ Y) (a : C(X, A)) :
().symm a = (ContinuousMap.compStarAlgHom' 𝕜 A f.symm.toContinuousMap) a
def Homeomorph.compStarAlgEquiv' {X : Type u_1} {Y : Type u_2} [] [] (𝕜 : Type u_3) [] (A : Type u_4) [] [] [] [] [Algebra 𝕜 A] (f : X ≃ₜ Y) :

ContinuousMap.compStarAlgHom' as a StarAlgEquiv when the continuous map f is actually a homeomorphism.

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