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} [TopologicalSpace α] [TopologicalSpace β] : CoeFun ↑{f : α → β | Continuous f} fun (x : ↑{f : α → β | Continuous f}) => α → β

Equations

• ContinuousFunctions.instCoeFunElemForallSetOfContinuous = { coe := Subtype.val }

mul and add

instance ContinuousMap.instAdd {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Add β] [ContinuousAdd β] : Add C(α, β)

Equations

• ContinuousMap.instAdd = { add := fun (f g : C(α, β)) => { toFun := ⇑f + ⇑g, continuous_toFun := ⋯ } }

theorem ContinuousMap.instAdd.proof_1 {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Add β] [ContinuousAdd β] (f : C(α, β)) (g : C(α, β)) : Continuous ((fun (p : β × β) => p.1 + p.2) ∘ fun (x : α) => (f x, g x))

instance ContinuousMap.instMul {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Mul β] [ContinuousMul β] : 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} [TopologicalSpace α] [TopologicalSpace β] [Add β] [ContinuousAdd β] (f : C(α, β)) (g : C(α, β)) : ⇑(f + g) = ⇑f + ⇑g

@[simp]

theorem ContinuousMap.coe_mul {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Mul β] [ContinuousMul β] (f : C(α, β)) (g : C(α, β)) : ⇑(f * g) = ⇑f * ⇑g

@[simp]

theorem ContinuousMap.add_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Add β] [ContinuousAdd β] (f : C(α, β)) (g : C(α, β)) (x : α) : (f + g) x = f x + g x

@[simp]

theorem ContinuousMap.mul_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Mul β] [ContinuousMul β] (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} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [Add γ] [ContinuousAdd γ] (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} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [Mul γ] [ContinuousMul γ] (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} [TopologicalSpace α] [TopologicalSpace β] [Zero β] : Zero C(α, β)

Equations

• ContinuousMap.instZero = { zero := ContinuousMap.const α 0 }

instance ContinuousMap.instOne {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [One β] : One C(α, β)

Equations

• ContinuousMap.instOne = { one := ContinuousMap.const α 1 }

@[simp]

theorem ContinuousMap.coe_zero {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Zero β] : ⇑0 = 0

@[simp]

theorem ContinuousMap.coe_one {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [One β] : ⇑1 = 1

@[simp]

theorem ContinuousMap.zero_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Zero β] (x : α) : 0 x = 0

@[simp]

theorem ContinuousMap.one_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [One β] (x : α) : 1 x = 1

@[simp]

theorem ContinuousMap.zero_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [Zero γ] (g : C(α, β)) : ContinuousMap.comp 0 g = 0

@[simp]

theorem ContinuousMap.one_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [One γ] (g : C(α, β)) : ContinuousMap.comp 1 g = 1

Nat.cast

instance ContinuousMap.instNatCast {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [NatCast β] : NatCast C(α, β)

Equations

• ContinuousMap.instNatCast = { natCast := fun (n : ℕ) => ContinuousMap.const α ↑n }

@[simp]

theorem ContinuousMap.coe_natCast {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [NatCast β] (n : ℕ) : ⇑↑n = ↑n

@[deprecated ContinuousMap.coe_natCast]

theorem ContinuousMap.coe_nat_cast {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [NatCast β] (n : ℕ) : ⇑↑n = ↑n

Alias of ContinuousMap.coe_natCast.

@[simp]

theorem ContinuousMap.natCast_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [NatCast β] (n : ℕ) (x : α) : ↑n x = ↑n

@[deprecated ContinuousMap.natCast_apply]

theorem ContinuousMap.nat_cast_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [NatCast β] (n : ℕ) (x : α) : ↑n x = ↑n

Alias of ContinuousMap.natCast_apply.

Int.cast

instance ContinuousMap.instIntCast {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [IntCast β] : IntCast C(α, β)

Equations

• ContinuousMap.instIntCast = { intCast := fun (n : ℤ) => ContinuousMap.const α ↑n }

@[simp]

theorem ContinuousMap.coe_intCast {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [IntCast β] (n : ℤ) : ⇑↑n = ↑n

@[deprecated ContinuousMap.coe_intCast]

theorem ContinuousMap.coe_int_cast {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [IntCast β] (n : ℤ) : ⇑↑n = ↑n

Alias of ContinuousMap.coe_intCast.

@[simp]

theorem ContinuousMap.intCast_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [IntCast β] (n : ℤ) (x : α) : ↑n x = ↑n

@[deprecated ContinuousMap.intCast_apply]

theorem ContinuousMap.int_cast_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [IntCast β] (n : ℤ) (x : α) : ↑n x = ↑n

Alias of ContinuousMap.intCast_apply.

nsmul and pow

instance ContinuousMap.instNSMul {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [AddMonoid β] [ContinuousAdd β] : SMul ℕ C(α, β)

Equations

• ContinuousMap.instNSMul = { smul := fun (n : ℕ) (f : C(α, β)) => { toFun := n • ⇑f, continuous_toFun := ⋯ } }

instance ContinuousMap.instPow {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Monoid β] [ContinuousMul β] : 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} [TopologicalSpace α] [TopologicalSpace β] [AddMonoid β] [ContinuousAdd β] (n : ℕ) (f : C(α, β)) : ⇑(n • f) = n • ⇑f

@[simp]

theorem ContinuousMap.coe_pow {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Monoid β] [ContinuousMul β] (f : C(α, β)) (n : ℕ) : ⇑(f ^ n) = ⇑f ^ n

theorem ContinuousMap.nsmul_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [AddMonoid β] [ContinuousAdd β] (f : C(α, β)) (n : ℕ) (x : α) : (n • f) x = n • f x

@[simp]

theorem ContinuousMap.pow_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Monoid β] [ContinuousMul β] (f : C(α, β)) (n : ℕ) (x : α) : (f ^ n) x = f x ^ n

theorem ContinuousMap.nsmul_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [AddMonoid γ] [ContinuousAdd γ] (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} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [Monoid γ] [ContinuousMul γ] (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} [TopologicalSpace α] [TopologicalSpace β] [Neg β] [ContinuousNeg β] : Neg C(α, β)

Equations

• ContinuousMap.instNegOfContinuousNeg = { neg := fun (f : C(α, β)) => { toFun := -⇑f, continuous_toFun := ⋯ } }

theorem ContinuousMap.instNegOfContinuousNeg.proof_1 {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Neg β] [ContinuousNeg β] (f : C(α, β)) : Continuous fun (x : α) => -f x

instance ContinuousMap.instInvOfContinuousInv {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Inv β] [ContinuousInv β] : Inv C(α, β)

Equations

• ContinuousMap.instInvOfContinuousInv = { inv := fun (f : C(α, β)) => { toFun := (⇑f)⁻¹, continuous_toFun := ⋯ } }

@[simp]

theorem ContinuousMap.coe_neg {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Neg β] [ContinuousNeg β] (f : C(α, β)) : ⇑(-f) = -⇑f

@[simp]

theorem ContinuousMap.coe_inv {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Inv β] [ContinuousInv β] (f : C(α, β)) : ⇑f⁻¹ = (⇑f)⁻¹

@[simp]

theorem ContinuousMap.neg_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Neg β] [ContinuousNeg β] (f : C(α, β)) (x : α) : (-f) x = -f x

@[simp]

theorem ContinuousMap.inv_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Inv β] [ContinuousInv β] (f : C(α, β)) (x : α) : f⁻¹ x = (f x)⁻¹

@[simp]

theorem ContinuousMap.neg_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [Neg γ] [ContinuousNeg γ] (f : C(β, γ)) (g : C(α, β)) : (-f).comp g = -f.comp g

@[simp]

theorem ContinuousMap.inv_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [Inv γ] [ContinuousInv γ] (f : C(β, γ)) (g : C(α, β)) : f⁻¹.comp g = (f.comp g)⁻¹

div and sub

theorem ContinuousMap.instSubOfContinuousSub.proof_1 {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Sub β] [ContinuousSub β] (f : C(α, β)) (g : C(α, β)) : Continuous fun (x : α) => f x - g x

instance ContinuousMap.instSubOfContinuousSub {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Sub β] [ContinuousSub β] : Sub C(α, β)

Equations

• ContinuousMap.instSubOfContinuousSub = { sub := fun (f g : C(α, β)) => { toFun := ⇑f - ⇑g, continuous_toFun := ⋯ } }

instance ContinuousMap.instDivOfContinuousDiv {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Div β] [ContinuousDiv β] : 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} [TopologicalSpace α] [TopologicalSpace β] [Sub β] [ContinuousSub β] (f : C(α, β)) (g : C(α, β)) : ⇑(f - g) = ⇑f - ⇑g

@[simp]

theorem ContinuousMap.coe_div {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Div β] [ContinuousDiv β] (f : C(α, β)) (g : C(α, β)) : ⇑(f / g) = ⇑f / ⇑g

@[simp]

theorem ContinuousMap.sub_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Sub β] [ContinuousSub β] (f : C(α, β)) (g : C(α, β)) (x : α) : (f - g) x = f x - g x

@[simp]

theorem ContinuousMap.div_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Div β] [ContinuousDiv β] (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} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [Sub γ] [ContinuousSub γ] (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} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [Div γ] [ContinuousDiv γ] (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} [TopologicalSpace α] [TopologicalSpace β] [AddGroup β] [TopologicalAddGroup β] : SMul ℤ C(α, β)

Equations

• ContinuousMap.instZSMul = { smul := fun (z : ℤ) (f : C(α, β)) => { toFun := z • ⇑f, continuous_toFun := ⋯ } }

instance ContinuousMap.instZPow {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Group β] [TopologicalGroup β] : 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} [TopologicalSpace α] [TopologicalSpace β] [AddGroup β] [TopologicalAddGroup β] (z : ℤ) (f : C(α, β)) : ⇑(z • f) = z • ⇑f

@[simp]

theorem ContinuousMap.coe_zpow {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Group β] [TopologicalGroup β] (f : C(α, β)) (z : ℤ) : ⇑(f ^ z) = ⇑f ^ z

theorem ContinuousMap.zsmul_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [AddGroup β] [TopologicalAddGroup β] (f : C(α, β)) (z : ℤ) (x : α) : (z • f) x = z • f x

@[simp]

theorem ContinuousMap.zpow_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Group β] [TopologicalGroup β] (f : C(α, β)) (z : ℤ) (x : α) : (f ^ z) x = f x ^ z

theorem ContinuousMap.zsmul_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [AddGroup γ] [TopologicalAddGroup γ] (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} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [Group γ] [TopologicalGroup γ] (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.

def continuousAddSubmonoid (α : Type u_1) (β : Type u_2) [TopologicalSpace α] [TopologicalSpace β] [AddZeroClass β] [ContinuousAdd β] : AddSubmonoid (α → β)

The AddSubmonoid of continuous maps α → β.

Equations

• continuousAddSubmonoid α β = { carrier := {f : α → β | Continuous f}, add_mem' := ⋯, zero_mem' := ⋯ }

theorem continuousAddSubmonoid.proof_1 (α : Type u_1) (β : Type u_2) [TopologicalSpace α] [TopologicalSpace β] [AddZeroClass β] [ContinuousAdd β] : ∀ {a b : α → β}, a ∈ {f : α → β | Continuous f} → b ∈ {f : α → β | Continuous f} → Continuous fun (x : α) => a x + b x

theorem continuousAddSubmonoid.proof_2 (α : Type u_1) (β : Type u_2) [TopologicalSpace α] [TopologicalSpace β] [AddZeroClass β] : Continuous fun (x : α) => 0

def continuousSubmonoid (α : Type u_1) (β : Type u_2) [TopologicalSpace α] [TopologicalSpace β] [MulOneClass β] [ContinuousMul β] : Submonoid (α → β)

The Submonoid of continuous maps α → β.

Equations

• continuousSubmonoid α β = { carrier := {f : α → β | Continuous f}, mul_mem' := ⋯, one_mem' := ⋯ }

def continuousAddSubgroup (α : Type u_1) (β : Type u_2) [TopologicalSpace α] [TopologicalSpace β] [AddGroup β] [TopologicalAddGroup β] : AddSubgroup (α → β)

The AddSubgroup of continuous maps α → β.

Equations

• continuousAddSubgroup α β = { toAddSubmonoid := continuousAddSubmonoid α β, neg_mem' := ⋯ }

theorem continuousAddSubgroup.proof_1 (α : Type u_1) (β : Type u_2) [TopologicalSpace α] [TopologicalSpace β] [AddGroup β] [TopologicalAddGroup β] : ∀ {x : α → β}, x ∈ (continuousAddSubmonoid α β).carrier → Continuous fun (x_1 : α) => -x x_1

def continuousSubgroup (α : Type u_1) (β : Type u_2) [TopologicalSpace α] [TopologicalSpace β] [Group β] [TopologicalGroup β] : Subgroup (α → β)

The subgroup of continuous maps α → β.

Equations

• continuousSubgroup α β = { toSubmonoid := continuousSubmonoid α β, inv_mem' := ⋯ }

theorem ContinuousMap.instAddSemigroupOfContinuousAdd.proof_1 {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [AddSemigroup β] [ContinuousAdd β] (f : C(α, β)) (g : C(α, β)) : ⇑(f + g) = ⇑f + ⇑g

instance ContinuousMap.instAddSemigroupOfContinuousAdd {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [AddSemigroup β] [ContinuousAdd β] : AddSemigroup C(α, β)

Equations

• ContinuousMap.instAddSemigroupOfContinuousAdd = Function.Injective.addSemigroup DFunLike.coe ⋯ ⋯

instance ContinuousMap.instSemigroupOfContinuousMul {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Semigroup β] [ContinuousMul β] : Semigroup C(α, β)

Equations

• ContinuousMap.instSemigroupOfContinuousMul = Function.Injective.semigroup DFunLike.coe ⋯ ⋯

instance ContinuousMap.instAddCommSemigroupOfContinuousAdd {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [AddCommSemigroup β] [ContinuousAdd β] : AddCommSemigroup C(α, β)

Equations

• ContinuousMap.instAddCommSemigroupOfContinuousAdd = Function.Injective.addCommSemigroup DFunLike.coe ⋯ ⋯

theorem ContinuousMap.instAddCommSemigroupOfContinuousAdd.proof_1 {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [AddCommSemigroup β] [ContinuousAdd β] (f : C(α, β)) (g : C(α, β)) : ⇑(f + g) = ⇑f + ⇑g

instance ContinuousMap.instCommSemigroupOfContinuousMul {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [CommSemigroup β] [ContinuousMul β] : CommSemigroup C(α, β)

Equations

• ContinuousMap.instCommSemigroupOfContinuousMul = Function.Injective.commSemigroup DFunLike.coe ⋯ ⋯

theorem ContinuousMap.instAddZeroClassOfContinuousAdd.proof_1 {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [AddZeroClass β] : ⇑0 = 0

instance ContinuousMap.instAddZeroClassOfContinuousAdd {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [AddZeroClass β] [ContinuousAdd β] : AddZeroClass C(α, β)

Equations

• ContinuousMap.instAddZeroClassOfContinuousAdd = Function.Injective.addZeroClass DFunLike.coe ⋯ ⋯ ⋯

theorem ContinuousMap.instAddZeroClassOfContinuousAdd.proof_2 {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [AddZeroClass β] [ContinuousAdd β] (f : C(α, β)) (g : C(α, β)) : ⇑(f + g) = ⇑f + ⇑g

instance ContinuousMap.instMulOneClassOfContinuousMul {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [MulOneClass β] [ContinuousMul β] : MulOneClass C(α, β)

Equations

• ContinuousMap.instMulOneClassOfContinuousMul = Function.Injective.mulOneClass DFunLike.coe ⋯ ⋯ ⋯

instance ContinuousMap.instMulZeroClassOfContinuousMul {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [MulZeroClass β] [ContinuousMul β] : MulZeroClass C(α, β)

Equations

• ContinuousMap.instMulZeroClassOfContinuousMul = Function.Injective.mulZeroClass DFunLike.coe ⋯ ⋯ ⋯

instance ContinuousMap.instSemigroupWithZeroOfContinuousMul {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [SemigroupWithZero β] [ContinuousMul β] : SemigroupWithZero C(α, β)

Equations

• ContinuousMap.instSemigroupWithZeroOfContinuousMul = Function.Injective.semigroupWithZero DFunLike.coe ⋯ ⋯ ⋯

theorem ContinuousMap.instAddMonoidOfContinuousAdd.proof_2 {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [AddMonoid β] [ContinuousAdd β] (f : C(α, β)) (g : C(α, β)) : ⇑(f + g) = ⇑f + ⇑g

instance ContinuousMap.instAddMonoidOfContinuousAdd {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [AddMonoid β] [ContinuousAdd β] : AddMonoid C(α, β)

Equations

• ContinuousMap.instAddMonoidOfContinuousAdd = Function.Injective.addMonoid DFunLike.coe ⋯ ⋯ ⋯ ⋯

theorem ContinuousMap.instAddMonoidOfContinuousAdd.proof_1 {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [AddMonoid β] : ⇑0 = 0

instance ContinuousMap.instMonoidOfContinuousMul {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Monoid β] [ContinuousMul β] : Monoid C(α, β)

Equations

• ContinuousMap.instMonoidOfContinuousMul = Function.Injective.monoid DFunLike.coe ⋯ ⋯ ⋯ ⋯

instance ContinuousMap.instMonoidWithZeroOfContinuousMul {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [MonoidWithZero β] [ContinuousMul β] : MonoidWithZero C(α, β)

Equations

• ContinuousMap.instMonoidWithZeroOfContinuousMul = Function.Injective.monoidWithZero DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯

theorem ContinuousMap.instAddCommMonoidOfContinuousAdd.proof_2 {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [AddCommMonoid β] [ContinuousAdd β] (f : C(α, β)) (g : C(α, β)) : ⇑(f + g) = ⇑f + ⇑g

instance ContinuousMap.instAddCommMonoidOfContinuousAdd {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [AddCommMonoid β] [ContinuousAdd β] : AddCommMonoid C(α, β)

Equations

• ContinuousMap.instAddCommMonoidOfContinuousAdd = Function.Injective.addCommMonoid DFunLike.coe ⋯ ⋯ ⋯ ⋯

theorem ContinuousMap.instAddCommMonoidOfContinuousAdd.proof_3 {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [AddCommMonoid β] [ContinuousAdd β] (f : C(α, β)) (n : ℕ) : ⇑(n • f) = n • ⇑f

theorem ContinuousMap.instAddCommMonoidOfContinuousAdd.proof_1 {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [AddCommMonoid β] : ⇑0 = 0

instance ContinuousMap.instCommMonoidOfContinuousMul {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [CommMonoid β] [ContinuousMul β] : CommMonoid C(α, β)

Equations

• ContinuousMap.instCommMonoidOfContinuousMul = Function.Injective.commMonoid DFunLike.coe ⋯ ⋯ ⋯ ⋯

instance ContinuousMap.instCommMonoidWithZeroOfContinuousMul {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [CommMonoidWithZero β] [ContinuousMul β] : CommMonoidWithZero C(α, β)

Equations

• ContinuousMap.instCommMonoidWithZeroOfContinuousMul = Function.Injective.commMonoidWithZero DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯

instance ContinuousMap.instContinuousAddOfLocallyCompactSpace {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [LocallyCompactSpace α] [Add β] [ContinuousAdd β] : ContinuousAdd C(α, β)

Equations

• ⋯ = ⋯

instance ContinuousMap.instContinuousMulOfLocallyCompactSpace {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [LocallyCompactSpace α] [Mul β] [ContinuousMul β] : ContinuousMul C(α, β)

Equations

• ⋯ = ⋯

theorem ContinuousMap.coeFnAddMonoidHom.proof_1 {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [AddMonoid β] : ⇑0 = 0

theorem ContinuousMap.coeFnAddMonoidHom.proof_2 {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [AddMonoid β] [ContinuousAdd β] (f : C(α, β)) (g : C(α, β)) : ⇑(f + g) = ⇑f + ⇑g

def ContinuousMap.coeFnAddMonoidHom {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [AddMonoid β] [ContinuousAdd β] : C(α, β) →+ α → β

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

Equations

• ContinuousMap.coeFnAddMonoidHom = { toFun := fun (f : C(α, β)) => ⇑f, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem ContinuousMap.coeFnMonoidHom_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Monoid β] [ContinuousMul β] (f : C(α, β)) (a : α) : ContinuousMap.coeFnMonoidHom f a = f a

@[simp]

theorem ContinuousMap.coeFnAddMonoidHom_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [AddMonoid β] [ContinuousAdd β] (f : C(α, β)) (a : α) : ContinuousMap.coeFnAddMonoidHom f a = f a

def ContinuousMap.coeFnMonoidHom {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Monoid β] [ContinuousMul β] : C(α, β) →* α → β

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

Equations

• ContinuousMap.coeFnMonoidHom = { toFun := fun (f : C(α, β)) => ⇑f, map_one' := ⋯, map_mul' := ⋯ }

theorem AddMonoidHom.compLeftContinuous.proof_1 (α : Type u_1) {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] {γ : Type u_2} [AddMonoid β] [ContinuousAdd β] [TopologicalSpace γ] [AddMonoid γ] [ContinuousAdd γ] (g : β →+ γ) (hg : Continuous ⇑g) : (fun (f : C(α, β)) => { toFun := ⇑g, continuous_toFun := hg }.comp f) 0 = 0

theorem AddMonoidHom.compLeftContinuous.proof_2 (α : Type u_1) {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {γ : Type u_3} [AddMonoid β] [ContinuousAdd β] [TopologicalSpace γ] [AddMonoid γ] [ContinuousAdd γ] (g : β →+ γ) (hg : Continuous ⇑g) : ∀ (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} [TopologicalSpace α] [TopologicalSpace β] {γ : Type u_3} [AddMonoid β] [ContinuousAdd β] [TopologicalSpace γ] [AddMonoid γ] [ContinuousAdd γ] (g : β →+ γ) (hg : Continuous ⇑g) : C(α, β) →+ C(α, γ)

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

Equations

• AddMonoidHom.compLeftContinuous α g hg = { toFun := fun (f : C(α, β)) => { toFun := ⇑g, continuous_toFun := hg }.comp f, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem MonoidHom.compLeftContinuous_apply (α : Type u_1) {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {γ : Type u_3} [Monoid β] [ContinuousMul β] [TopologicalSpace γ] [Monoid γ] [ContinuousMul γ] (g : β →* γ) (hg : Continuous ⇑g) (f : C(α, β)) : (MonoidHom.compLeftContinuous α g hg) f = { toFun := ⇑g, continuous_toFun := hg }.comp f

@[simp]

theorem AddMonoidHom.compLeftContinuous_apply (α : Type u_1) {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {γ : Type u_3} [AddMonoid β] [ContinuousAdd β] [TopologicalSpace γ] [AddMonoid γ] [ContinuousAdd γ] (g : β →+ γ) (hg : Continuous ⇑g) (f : C(α, β)) : (AddMonoidHom.compLeftContinuous α g hg) f = { toFun := ⇑g, continuous_toFun := hg }.comp f

def MonoidHom.compLeftContinuous (α : Type u_1) {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {γ : Type u_3} [Monoid β] [ContinuousMul β] [TopologicalSpace γ] [Monoid γ] [ContinuousMul γ] (g : β →* γ) (hg : Continuous ⇑g) : C(α, β) →* C(α, γ)

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

Equations

• MonoidHom.compLeftContinuous α g hg = { toFun := fun (f : C(α, β)) => { toFun := ⇑g, continuous_toFun := hg }.comp f, map_one' := ⋯, map_mul' := ⋯ }

def ContinuousMap.compAddMonoidHom' {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {γ : Type u_3} [TopologicalSpace γ] [AddZeroClass γ] [ContinuousAdd γ] (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' := ⋯ }

theorem ContinuousMap.compAddMonoidHom'.proof_2 {α : Type u_3} {β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] {γ : Type u_2} [TopologicalSpace γ] [AddZeroClass γ] [ContinuousAdd γ] (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} [TopologicalSpace α] [TopologicalSpace β] {γ : Type u_2} [TopologicalSpace γ] [AddZeroClass γ] (g : C(α, β)) : ContinuousMap.comp 0 g = 0

@[simp]

theorem ContinuousMap.compMonoidHom'_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {γ : Type u_3} [TopologicalSpace γ] [MulOneClass γ] [ContinuousMul γ] (g : C(α, β)) (f : C(β, γ)) : g.compMonoidHom' f = f.comp g

@[simp]

theorem ContinuousMap.compAddMonoidHom'_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {γ : Type u_3} [TopologicalSpace γ] [AddZeroClass γ] [ContinuousAdd γ] (g : C(α, β)) (f : C(β, γ)) : g.compAddMonoidHom' f = f.comp g

def ContinuousMap.compMonoidHom' {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {γ : Type u_3} [TopologicalSpace γ] [MulOneClass γ] [ContinuousMul γ] (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' := ⋯ }

@[simp]

theorem ContinuousMap.coe_sum {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [AddCommMonoid β] [ContinuousAdd β] {ι : Type u_3} (s : Finset ι) (f : ι → C(α, β)) : ⇑(∑ i ∈ s, f i) = ∑ i ∈ s, ⇑(f i)

@[simp]

theorem ContinuousMap.coe_prod {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [CommMonoid β] [ContinuousMul β] {ι : Type u_3} (s : Finset ι) (f : ι → C(α, β)) : ⇑(∏ i ∈ s, f i) = ∏ i ∈ s, ⇑(f i)

theorem ContinuousMap.sum_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [AddCommMonoid β] [ContinuousAdd β] {ι : Type u_3} (s : Finset ι) (f : ι → C(α, β)) (a : α) : (∑ i ∈ s, f i) a = ∑ i ∈ s, (f i) a

theorem ContinuousMap.prod_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [CommMonoid β] [ContinuousMul β] {ι : Type u_3} (s : Finset ι) (f : ι → C(α, β)) (a : α) : (∏ i ∈ s, f i) a = ∏ i ∈ s, (f i) a

theorem ContinuousMap.instAddGroupOfTopologicalAddGroup.proof_5 {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [AddGroup β] [TopologicalAddGroup β] (f : C(α, β)) (n : ℕ) : ⇑(n • f) = n • ⇑f

instance ContinuousMap.instAddGroupOfTopologicalAddGroup {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [AddGroup β] [TopologicalAddGroup β] : AddGroup C(α, β)

Equations

• ContinuousMap.instAddGroupOfTopologicalAddGroup = Function.Injective.addGroup DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

theorem ContinuousMap.instAddGroupOfTopologicalAddGroup.proof_1 {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [AddGroup β] : ⇑0 = 0

theorem ContinuousMap.instAddGroupOfTopologicalAddGroup.proof_3 {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [AddGroup β] [TopologicalAddGroup β] (f : C(α, β)) : ⇑(-f) = -⇑f

theorem ContinuousMap.instAddGroupOfTopologicalAddGroup.proof_4 {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [AddGroup β] [TopologicalAddGroup β] (f : C(α, β)) (g : C(α, β)) : ⇑(f - g) = ⇑f - ⇑g

theorem ContinuousMap.instAddGroupOfTopologicalAddGroup.proof_2 {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [AddGroup β] [TopologicalAddGroup β] (f : C(α, β)) (g : C(α, β)) : ⇑(f + g) = ⇑f + ⇑g

instance ContinuousMap.instGroupOfTopologicalGroup {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Group β] [TopologicalGroup β] : Group C(α, β)

Equations

• ContinuousMap.instGroupOfTopologicalGroup = Function.Injective.group DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

theorem ContinuousMap.instAddCommGroupContinuousMap.proof_7 {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [AddCommGroup β] [TopologicalAddGroup β] (f : C(α, β)) (g : C(α, β)) : ⇑(f - g) = ⇑f - ⇑g

theorem ContinuousMap.instAddCommGroupContinuousMap.proof_5 {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [AddCommGroup β] [TopologicalAddGroup β] (f : C(α, β)) (g : C(α, β)) : ⇑(f + g) = ⇑f + ⇑g

theorem ContinuousMap.instAddCommGroupContinuousMap.proof_1 {β : Type u_1} [TopologicalSpace β] [AddCommGroup β] [TopologicalAddGroup β] : ContinuousAdd β

theorem ContinuousMap.instAddCommGroupContinuousMap.proof_4 {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [AddCommGroup β] : ⇑0 = 0

theorem ContinuousMap.instAddCommGroupContinuousMap.proof_6 {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [AddCommGroup β] [TopologicalAddGroup β] (f : C(α, β)) : ⇑(-f) = -⇑f

theorem ContinuousMap.instAddCommGroupContinuousMap.proof_2 {β : Type u_1} [TopologicalSpace β] [AddCommGroup β] [TopologicalAddGroup β] : ContinuousNeg β

theorem ContinuousMap.instAddCommGroupContinuousMap.proof_8 {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [AddCommGroup β] [TopologicalAddGroup β] (f : C(α, β)) (n : ℕ) : ⇑(n • f) = n • ⇑f

theorem ContinuousMap.instAddCommGroupContinuousMap.proof_3 {β : Type u_1} [TopologicalSpace β] [AddCommGroup β] [TopologicalAddGroup β] : ContinuousSub β

theorem ContinuousMap.instAddCommGroupContinuousMap.proof_9 {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [AddCommGroup β] [TopologicalAddGroup β] (f : C(α, β)) (z : ℤ) : ⇑(z • f) = z • ⇑f

instance ContinuousMap.instAddCommGroupContinuousMap {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [AddCommGroup β] [TopologicalAddGroup β] : AddCommGroup C(α, β)

Equations

• ContinuousMap.instAddCommGroupContinuousMap = Function.Injective.addCommGroup DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance ContinuousMap.instCommGroupContinuousMap {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [CommGroup β] [TopologicalGroup β] : CommGroup C(α, β)

Equations

• ContinuousMap.instCommGroupContinuousMap = Function.Injective.commGroup DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance ContinuousMap.instTopologicalAddGroup {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [AddCommGroup β] [TopologicalAddGroup β] : TopologicalAddGroup C(α, β)

Equations

• ⋯ = ⋯

instance ContinuousMap.instTopologicalGroup {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [CommGroup β] [TopologicalGroup β] : TopologicalGroup C(α, β)

Equations

• ⋯ = ⋯

theorem ContinuousMap.hasSum_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {γ : Type u_3} [AddCommMonoid β] [ContinuousAdd β] {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} [TopologicalSpace α] [TopologicalSpace β] [AddCommMonoid β] [ContinuousAdd β] {γ : Type u_3} {f : γ → C(α, β)} (hf : Summable f) (x : α) : Summable fun (i : γ) => (f i) x

theorem ContinuousMap.tsum_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [T2Space β] [AddCommMonoid β] [ContinuousAdd β] {γ : Type u_3} {f : γ → C(α, β)} (hf : Summable f) (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) [TopologicalSpace α] [TopologicalSpace R] [NonAssocSemiring R] [TopologicalSemiring R] : Subsemiring (α → R)

The subsemiring of continuous maps α → β.

Equations

• continuousSubsemiring α R = { carrier := (continuousAddSubmonoid α R).carrier, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯ }

def continuousSubring (α : Type u_1) (R : Type u_2) [TopologicalSpace α] [TopologicalSpace R] [Ring R] [TopologicalRing R] : Subring (α → R)

The subring of continuous maps α → β.

Equations

• continuousSubring α R = { carrier := (continuousAddSubgroup α R).carrier, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }

instance ContinuousMap.instNonUnitalNonAssocSemiringOfTopologicalSemiring {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [NonUnitalNonAssocSemiring β] [TopologicalSemiring β] : NonUnitalNonAssocSemiring C(α, β)

Equations

• ContinuousMap.instNonUnitalNonAssocSemiringOfTopologicalSemiring = Function.Injective.nonUnitalNonAssocSemiring DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯

instance ContinuousMap.instNonUnitalSemiringOfTopologicalSemiring {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [NonUnitalSemiring β] [TopologicalSemiring β] : NonUnitalSemiring C(α, β)

Equations

• ContinuousMap.instNonUnitalSemiringOfTopologicalSemiring = Function.Injective.nonUnitalSemiring DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯

instance ContinuousMap.instAddMonoidWithOneOfContinuousAdd {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [AddMonoidWithOne β] [ContinuousAdd β] : AddMonoidWithOne C(α, β)

Equations

• ContinuousMap.instAddMonoidWithOneOfContinuousAdd = Function.Injective.addMonoidWithOne DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance ContinuousMap.instNonAssocSemiringOfTopologicalSemiring {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [NonAssocSemiring β] [TopologicalSemiring β] : NonAssocSemiring C(α, β)

Equations

• ContinuousMap.instNonAssocSemiringOfTopologicalSemiring = Function.Injective.nonAssocSemiring DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance ContinuousMap.instSemiringOfTopologicalSemiring {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Semiring β] [TopologicalSemiring β] : Semiring C(α, β)

Equations

• ContinuousMap.instSemiringOfTopologicalSemiring = Function.Injective.semiring DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance ContinuousMap.instNonUnitalNonAssocRingOfTopologicalRing {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [NonUnitalNonAssocRing β] [TopologicalRing β] : NonUnitalNonAssocRing C(α, β)

Equations

• ContinuousMap.instNonUnitalNonAssocRingOfTopologicalRing = Function.Injective.nonUnitalNonAssocRing DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance ContinuousMap.instNonUnitalRingOfTopologicalRing {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [NonUnitalRing β] [TopologicalRing β] : NonUnitalRing C(α, β)

Equations

• ContinuousMap.instNonUnitalRingOfTopologicalRing = Function.Injective.nonUnitalRing DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance ContinuousMap.instNonAssocRingOfTopologicalRing {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [NonAssocRing β] [TopologicalRing β] : NonAssocRing C(α, β)

Equations

• ContinuousMap.instNonAssocRingOfTopologicalRing = Function.Injective.nonAssocRing DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance ContinuousMap.instRing {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Ring β] [TopologicalRing β] : Ring C(α, β)

Equations

• ContinuousMap.instRing = Function.Injective.ring DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance ContinuousMap.instNonUnitalCommSemiringOfTopologicalSemiring {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [NonUnitalCommSemiring β] [TopologicalSemiring β] : NonUnitalCommSemiring C(α, β)

Equations

• ContinuousMap.instNonUnitalCommSemiringOfTopologicalSemiring = Function.Injective.nonUnitalCommSemiring DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯

instance ContinuousMap.instCommSemiringOfTopologicalSemiring {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [CommSemiring β] [TopologicalSemiring β] : CommSemiring C(α, β)

Equations

• ContinuousMap.instCommSemiringOfTopologicalSemiring = Function.Injective.commSemiring DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance ContinuousMap.instNonUnitalCommRingOfTopologicalRing {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [NonUnitalCommRing β] [TopologicalRing β] : NonUnitalCommRing C(α, β)

Equations

• ContinuousMap.instNonUnitalCommRingOfTopologicalRing = Function.Injective.nonUnitalCommRing DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance ContinuousMap.instCommRingOfTopologicalRing {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [CommRing β] [TopologicalRing β] : CommRing C(α, β)

Equations

• ContinuousMap.instCommRingOfTopologicalRing = Function.Injective.commRing DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance ContinuousMap.instTopologicalSemiringOfLocallyCompactSpace {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [LocallyCompactSpace α] [NonUnitalSemiring β] [TopologicalSemiring β] : TopologicalSemiring C(α, β)

Equations

• ⋯ = ⋯

instance ContinuousMap.instTopologicalRingOfLocallyCompactSpace {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [LocallyCompactSpace α] [NonUnitalRing β] [TopologicalRing β] : TopologicalRing C(α, β)

Equations

• ⋯ = ⋯

@[simp]

theorem RingHom.compLeftContinuous_apply_apply (α : Type u_1) {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [Semiring β] [TopologicalSemiring β] [TopologicalSpace γ] [Semiring γ] [TopologicalSemiring γ] (g : β →+* γ) (hg : Continuous ⇑g) (f : C(α, β)) : ∀ (a : α), ((RingHom.compLeftContinuous α g hg) f) a = g (f a)

def RingHom.compLeftContinuous (α : Type u_1) {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [Semiring β] [TopologicalSemiring β] [TopologicalSpace γ] [Semiring γ] [TopologicalSemiring γ] (g : β →+* γ) (hg : Continuous ⇑g) : C(α, β) →+* C(α, γ)

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

Equations

• RingHom.compLeftContinuous α g hg = { toMonoidHom := MonoidHom.compLeftContinuous α (↑g) hg, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem ContinuousMap.coeFnRingHom_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Semiring β] [TopologicalSemiring β] (f : C(α, β)) (a : α) : ContinuousMap.coeFnRingHom f a = f a

def ContinuousMap.coeFnRingHom {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Semiring β] [TopologicalSemiring β] : C(α, β) →+* α → β

Coercion to a function as a RingHom.

Equations

• ContinuousMap.coeFnRingHom = { toMonoidHom := ContinuousMap.coeFnMonoidHom, map_zero' := ⋯, map_add' := ⋯ }

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) [TopologicalSpace α] (R : Type u_2) [Semiring R] (M : Type u_3) [TopologicalSpace M] [AddCommGroup M] [Module R M] [ContinuousConstSMul R M] [TopologicalAddGroup M] : Submodule R (α → M)

The R-submodule of continuous maps α → M.

Equations

• continuousSubmodule α R M = { carrier := {f : α → M | Continuous f}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

theorem ContinuousMap.instVAdd.proof_1 {α : Type u_1} [TopologicalSpace α] {R : Type u_3} {M : Type u_2} [TopologicalSpace M] [VAdd R M] [ContinuousConstVAdd R M] (r : R) (f : C(α, M)) : Continuous fun (x : α) => r +ᵥ f x

instance ContinuousMap.instVAdd {α : Type u_1} [TopologicalSpace α] {R : Type u_3} {M : Type u_5} [TopologicalSpace M] [VAdd R M] [ContinuousConstVAdd R M] : VAdd R C(α, M)

Equations

• ContinuousMap.instVAdd = { vadd := fun (r : R) (f : C(α, M)) => { toFun := r +ᵥ ⇑f, continuous_toFun := ⋯ } }

instance ContinuousMap.instSMul {α : Type u_1} [TopologicalSpace α] {R : Type u_3} {M : Type u_5} [TopologicalSpace M] [SMul R M] [ContinuousConstSMul 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} [TopologicalSpace α] {R : Type u_3} {M : Type u_5} [TopologicalSpace M] [LocallyCompactSpace α] [VAdd R M] [ContinuousConstVAdd R M] : ContinuousConstVAdd R C(α, M)

Equations

• ⋯ = ⋯

instance ContinuousMap.instContinuousConstSMulOfLocallyCompactSpace {α : Type u_1} [TopologicalSpace α] {R : Type u_3} {M : Type u_5} [TopologicalSpace M] [LocallyCompactSpace α] [SMul R M] [ContinuousConstSMul R M] : ContinuousConstSMul R C(α, M)

Equations

• ⋯ = ⋯

instance ContinuousMap.instContinuousVAddOfLocallyCompactSpace {α : Type u_1} [TopologicalSpace α] {R : Type u_3} {M : Type u_5} [TopologicalSpace M] [LocallyCompactSpace α] [TopologicalSpace R] [VAdd R M] [ContinuousVAdd R M] : ContinuousVAdd R C(α, M)

Equations

• ⋯ = ⋯

instance ContinuousMap.instContinuousSMulOfLocallyCompactSpace {α : Type u_1} [TopologicalSpace α] {R : Type u_3} {M : Type u_5} [TopologicalSpace M] [LocallyCompactSpace α] [TopologicalSpace R] [SMul R M] [ContinuousSMul R M] : ContinuousSMul R C(α, M)

Equations

• ⋯ = ⋯

@[simp]

theorem ContinuousMap.coe_vadd {α : Type u_1} [TopologicalSpace α] {R : Type u_3} {M : Type u_5} [TopologicalSpace M] [VAdd R M] [ContinuousConstVAdd R M] (c : R) (f : C(α, M)) : ⇑(c +ᵥ f) = c +ᵥ ⇑f

@[simp]

theorem ContinuousMap.coe_smul {α : Type u_1} [TopologicalSpace α] {R : Type u_3} {M : Type u_5} [TopologicalSpace M] [SMul R M] [ContinuousConstSMul R M] (c : R) (f : C(α, M)) : ⇑(c • f) = c • ⇑f

theorem ContinuousMap.vadd_apply {α : Type u_1} [TopologicalSpace α] {R : Type u_3} {M : Type u_5} [TopologicalSpace M] [VAdd R M] [ContinuousConstVAdd R M] (c : R) (f : C(α, M)) (a : α) : (c +ᵥ f) a = c +ᵥ f a

theorem ContinuousMap.smul_apply {α : Type u_1} [TopologicalSpace α] {R : Type u_3} {M : Type u_5} [TopologicalSpace M] [SMul R M] [ContinuousConstSMul 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} [TopologicalSpace α] [TopologicalSpace β] {R : Type u_3} {M : Type u_5} [TopologicalSpace M] [VAdd R M] [ContinuousConstVAdd 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} [TopologicalSpace α] [TopologicalSpace β] {R : Type u_3} {M : Type u_5} [TopologicalSpace M] [SMul R M] [ContinuousConstSMul R M] (r : R) (f : C(β, M)) (g : C(α, β)) : (r • f).comp g = r • f.comp g

instance ContinuousMap.instVAddCommClass {α : Type u_1} [TopologicalSpace α] {R : Type u_3} {R₁ : Type u_4} {M : Type u_5} [TopologicalSpace M] [VAdd R M] [ContinuousConstVAdd R M] [VAdd R₁ M] [ContinuousConstVAdd R₁ M] [VAddCommClass R R₁ M] : VAddCommClass R R₁ C(α, M)

Equations

• ⋯ = ⋯

instance ContinuousMap.instSMulCommClass {α : Type u_1} [TopologicalSpace α] {R : Type u_3} {R₁ : Type u_4} {M : Type u_5} [TopologicalSpace M] [SMul R M] [ContinuousConstSMul R M] [SMul R₁ M] [ContinuousConstSMul R₁ M] [SMulCommClass R R₁ M] : SMulCommClass R R₁ C(α, M)

Equations

• ⋯ = ⋯

instance ContinuousMap.instIsScalarTower {α : Type u_1} [TopologicalSpace α] {R : Type u_3} {R₁ : Type u_4} {M : Type u_5} [TopologicalSpace M] [SMul R M] [ContinuousConstSMul R M] [SMul R₁ M] [ContinuousConstSMul R₁ M] [SMul R R₁] [IsScalarTower R R₁ M] : IsScalarTower R R₁ C(α, M)

Equations

• ⋯ = ⋯

instance ContinuousMap.instIsCentralScalar {α : Type u_1} [TopologicalSpace α] {R : Type u_3} {M : Type u_5} [TopologicalSpace M] [SMul R M] [SMul Rᵐᵒᵖ M] [ContinuousConstSMul R M] [IsCentralScalar R M] : IsCentralScalar R C(α, M)

Equations

• ⋯ = ⋯

instance ContinuousMap.instMulActionOfContinuousConstSMul {α : Type u_1} [TopologicalSpace α] {R : Type u_3} {M : Type u_5} [TopologicalSpace M] [Monoid R] [MulAction R M] [ContinuousConstSMul R M] : MulAction R C(α, M)

Equations

• ContinuousMap.instMulActionOfContinuousConstSMul = Function.Injective.mulAction DFunLike.coe ⋯ ⋯

instance ContinuousMap.instDistribMulActionOfContinuousConstSMul {α : Type u_1} [TopologicalSpace α] {R : Type u_3} {M : Type u_5} [TopologicalSpace M] [Monoid R] [AddMonoid M] [DistribMulAction R M] [ContinuousAdd M] [ContinuousConstSMul R M] : DistribMulAction R C(α, M)

Equations

• ContinuousMap.instDistribMulActionOfContinuousConstSMul = Function.Injective.distribMulAction ContinuousMap.coeFnAddMonoidHom ⋯ ⋯

instance ContinuousMap.module {α : Type u_1} [TopologicalSpace α] {R : Type u_3} {M : Type u_5} [TopologicalSpace M] [Semiring R] [AddCommMonoid M] [ContinuousAdd M] [Module R M] [ContinuousConstSMul R M] : Module R C(α, M)

Equations

• ContinuousMap.module = Function.Injective.module R ContinuousMap.coeFnAddMonoidHom ⋯ ⋯

@[simp]

theorem ContinuousLinearMap.compLeftContinuous_apply (R : Type u_3) {M : Type u_5} [TopologicalSpace M] {M₂ : Type u_6} [TopologicalSpace M₂] [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [ContinuousAdd M] [Module R M] [ContinuousConstSMul R M] [ContinuousAdd M₂] [Module R M₂] [ContinuousConstSMul R M₂] (α : Type u_7) [TopologicalSpace α] (g : M →L[R] M₂) : ∀ (a : C(α, M)), (ContinuousLinearMap.compLeftContinuous R α g) a = (↑(AddMonoidHom.compLeftContinuous α (↑g).toAddMonoidHom ⋯)).toFun a

def ContinuousLinearMap.compLeftContinuous (R : Type u_3) {M : Type u_5} [TopologicalSpace M] {M₂ : Type u_6} [TopologicalSpace M₂] [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [ContinuousAdd M] [Module R M] [ContinuousConstSMul R M] [ContinuousAdd M₂] [Module R M₂] [ContinuousConstSMul R M₂] (α : Type u_7) [TopologicalSpace α] (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

• ContinuousLinearMap.compLeftContinuous R α g = { toFun := (↑(AddMonoidHom.compLeftContinuous α (↑g).toAddMonoidHom ⋯)).toFun, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem ContinuousMap.coeFnLinearMap_apply {α : Type u_1} [TopologicalSpace α] (R : Type u_3) {M : Type u_5} [TopologicalSpace M] [Semiring R] [AddCommMonoid M] [ContinuousAdd M] [Module R M] [ContinuousConstSMul R M] : ∀ (a : C(α, M)) (a_1 : α), (ContinuousMap.coeFnLinearMap R) a a_1 = (↑ContinuousMap.coeFnAddMonoidHom).toFun a a_1

def ContinuousMap.coeFnLinearMap {α : Type u_1} [TopologicalSpace α] (R : Type u_3) {M : Type u_5} [TopologicalSpace M] [Semiring R] [AddCommMonoid M] [ContinuousAdd M] [Module R M] [ContinuousConstSMul R M] : C(α, M) →ₗ[R] α → M

Coercion to a function as a LinearMap.

Equations

• ContinuousMap.coeFnLinearMap R = { toFun := (↑ContinuousMap.coeFnAddMonoidHom).toFun, map_add' := ⋯, map_smul' := ⋯ }

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} [TopologicalSpace α] {R : Type u_2} [CommSemiring R] {A : Type u_3} [TopologicalSpace A] [Semiring A] [Algebra R A] [TopologicalSemiring A] : Subalgebra R (α → A)

The R-subalgebra of continuous maps α → A.

Equations

• continuousSubalgebra = { carrier := {f : α → A | Continuous f}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, algebraMap_mem' := ⋯ }

def ContinuousMap.C {α : Type u_1} [TopologicalSpace α] {R : Type u_2} [CommSemiring R] {A : Type u_3} [TopologicalSpace A] [Semiring A] [Algebra R A] [TopologicalSemiring A] : R →+* C(α, A)

Continuous constant functions as a RingHom.

Equations

• ContinuousMap.C = { toFun := fun (c : R) => { toFun := fun (x : α) => (algebraMap R A) c, continuous_toFun := ⋯ }, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem ContinuousMap.C_apply {α : Type u_1} [TopologicalSpace α] {R : Type u_2} [CommSemiring R] {A : Type u_3} [TopologicalSpace A] [Semiring A] [Algebra R A] [TopologicalSemiring A] (r : R) (a : α) : (ContinuousMap.C r) a = (algebraMap R A) r

instance ContinuousMap.algebra {α : Type u_1} [TopologicalSpace α] {R : Type u_2} [CommSemiring R] {A : Type u_3} [TopologicalSpace A] [Semiring A] [Algebra R A] [TopologicalSemiring A] : Algebra R C(α, A)

Equations

• ContinuousMap.algebra = Algebra.mk ContinuousMap.C ⋯ ⋯

@[simp]

theorem AlgHom.compLeftContinuous_apply_apply (R : Type u_2) [CommSemiring R] {A : Type u_3} [TopologicalSpace A] [Semiring A] [Algebra R A] [TopologicalSemiring A] {A₂ : Type u_4} [TopologicalSpace A₂] [Semiring A₂] [Algebra R A₂] [TopologicalSemiring A₂] {α : Type u_5} [TopologicalSpace α] (g : A →ₐ[R] A₂) (hg : Continuous ⇑g) (f : C(α, A)) : ∀ (a : α), ((AlgHom.compLeftContinuous R g hg) f) a = g (f a)

def AlgHom.compLeftContinuous (R : Type u_2) [CommSemiring R] {A : Type u_3} [TopologicalSpace A] [Semiring A] [Algebra R A] [TopologicalSemiring A] {A₂ : Type u_4} [TopologicalSpace A₂] [Semiring A₂] [Algebra R A₂] [TopologicalSemiring A₂] {α : Type u_5} [TopologicalSpace α] (g : A →ₐ[R] A₂) (hg : Continuous ⇑g) : 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

• AlgHom.compLeftContinuous R g hg = { toRingHom := RingHom.compLeftContinuous α g.toRingHom hg, commutes' := ⋯ }

@[simp]

theorem ContinuousMap.compRightAlgHom_apply (R : Type u_2) [CommSemiring R] (A : Type u_3) [TopologicalSpace A] [Semiring A] [Algebra R A] [TopologicalSemiring A] {α : Type u_5} {β : Type u_6} [TopologicalSpace α] [TopologicalSpace β] (f : C(α, β)) (g : C(β, A)) : (ContinuousMap.compRightAlgHom R A f) g = g.comp f

def ContinuousMap.compRightAlgHom (R : Type u_2) [CommSemiring R] (A : Type u_3) [TopologicalSpace A] [Semiring A] [Algebra R A] [TopologicalSemiring A] {α : Type u_5} {β : Type u_6} [TopologicalSpace α] [TopologicalSpace β] (f : C(α, β)) : C(β, A) →ₐ[R] C(α, A)

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

Equations

• ContinuousMap.compRightAlgHom R A f = { toFun := fun (g : C(β, A)) => g.comp f, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }

@[simp]

theorem ContinuousMap.coeFnAlgHom_apply {α : Type u_1} [TopologicalSpace α] (R : Type u_2) [CommSemiring R] {A : Type u_3} [TopologicalSpace A] [Semiring A] [Algebra R A] [TopologicalSemiring A] (f : C(α, A)) (a : α) : (ContinuousMap.coeFnAlgHom R) f a = f a

def ContinuousMap.coeFnAlgHom {α : Type u_1} [TopologicalSpace α] (R : Type u_2) [CommSemiring R] {A : Type u_3} [TopologicalSpace A] [Semiring A] [Algebra R A] [TopologicalSemiring A] : C(α, A) →ₐ[R] α → A

Coercion to a function as an AlgHom.

Equations

• ContinuousMap.coeFnAlgHom R = { toRingHom := ContinuousMap.coeFnRingHom, commutes' := ⋯ }

@[reducible, inline]

abbrev Subalgebra.SeparatesPoints {α : Type u_1} [TopologicalSpace α] {R : Type u_2} [CommSemiring R] {A : Type u_3} [TopologicalSpace A] [Semiring A] [Algebra R A] [TopologicalSemiring A] (s : Subalgebra R C(α, A)) : Prop

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

theorem Subalgebra.separatesPoints_monotone {α : Type u_1} [TopologicalSpace α] {R : Type u_2} [CommSemiring R] {A : Type u_3} [TopologicalSpace A] [Semiring A] [Algebra R A] [TopologicalSemiring A] : Monotone fun (s : Subalgebra R C(α, A)) => s.SeparatesPoints

@[simp]

theorem algebraMap_apply {α : Type u_1} [TopologicalSpace α] {R : Type u_2} [CommSemiring R] {A : Type u_3} [TopologicalSpace A] [Semiring A] [Algebra R A] [TopologicalSemiring A] (k : R) (a : α) : ((algebraMap R C(α, A)) k) a = k • 1

def Set.SeparatesPointsStrongly {α : Type u_1} [TopologicalSpace α] {𝕜 : Type u_5} [TopologicalSpace 𝕜] (s : Set C(α, 𝕜)) : Prop

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 : α), ∃ f ∈ s, f x = v x ∧ f y = v y

theorem Subalgebra.SeparatesPoints.strongly {α : Type u_1} [TopologicalSpace α] {𝕜 : Type u_5} [TopologicalSpace 𝕜] [Field 𝕜] [TopologicalRing 𝕜] {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) [TopologicalSpace α] (R : Type u_2) [CommSemiring R] [TopologicalSpace R] [TopologicalSemiring R] [Subsingleton α] : Subsingleton (Subalgebra R C(α, R))

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} [TopologicalSpace α] {R : Type u_2} [Semiring R] [TopologicalSpace R] {M : Type u_3} [TopologicalSpace M] [AddCommMonoid M] [Module R M] [ContinuousSMul 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} [TopologicalSpace α] (R : Type u_2) [Semiring R] [TopologicalSpace R] [TopologicalSemiring R] (M : Type u_3) [TopologicalSpace M] [AddCommMonoid M] [ContinuousAdd M] [Module R M] [ContinuousSMul R M] : Module C(α, R) C(α, M)

Equations

• ContinuousMap.module' R M = Module.mk ⋯ ⋯

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} [TopologicalSpace α] {β : Type u_2} [TopologicalSpace β] [PartialOrder β] [Add β] [ContinuousAdd β] [CovariantClass β β (fun (x1 x2 : β) => x1 + x2) fun (x1 x2 : β) => x1 ≤ x2] : CovariantClass C(α, β) C(α, β) (fun (x1 x2 : C(α, β)) => x1 + x2) fun (x1 x2 : C(α, β)) => x1 ≤ x2

Equations

• ⋯ = ⋯

instance ContinuousMap.instCovariantClass_mul_le_left {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [TopologicalSpace β] [PartialOrder β] [Mul β] [ContinuousMul β] [CovariantClass β β (fun (x1 x2 : β) => x1 * x2) fun (x1 x2 : β) => x1 ≤ x2] : CovariantClass C(α, β) C(α, β) (fun (x1 x2 : C(α, β)) => x1 * x2) fun (x1 x2 : C(α, β)) => x1 ≤ x2

Equations

• ⋯ = ⋯

instance ContinuousMap.instCovariantClass_add_le_right {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [TopologicalSpace β] [PartialOrder β] [Add β] [ContinuousAdd β] [CovariantClass β β (Function.swap fun (x1 x2 : β) => x1 + x2) fun (x1 x2 : β) => x1 ≤ x2] : CovariantClass C(α, β) C(α, β) (Function.swap fun (x1 x2 : C(α, β)) => x1 + x2) fun (x1 x2 : C(α, β)) => x1 ≤ x2

Equations

• ⋯ = ⋯

instance ContinuousMap.instCovariantClass_mul_le_right {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [TopologicalSpace β] [PartialOrder β] [Mul β] [ContinuousMul β] [CovariantClass β β (Function.swap fun (x1 x2 : β) => x1 * x2) fun (x1 x2 : β) => x1 ≤ x2] : CovariantClass C(α, β) C(α, β) (Function.swap fun (x1 x2 : C(α, β)) => x1 * x2) fun (x1 x2 : C(α, β)) => x1 ≤ x2

Equations

• ⋯ = ⋯

@[simp]

theorem ContinuousMap.coe_abs {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [TopologicalSpace β] [AddGroup β] [TopologicalAddGroup β] [Lattice β] [TopologicalLattice β] (f : C(α, β)) : ⇑|f| = |⇑f|

@[simp]

theorem ContinuousMap.coe_mabs {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [TopologicalSpace β] [Group β] [TopologicalGroup β] [Lattice β] [TopologicalLattice β] (f : C(α, β)) : ⇑(mabs f) = mabs ⇑f

@[simp]

theorem ContinuousMap.abs_apply {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [TopologicalSpace β] [AddGroup β] [TopologicalAddGroup β] [Lattice β] [TopologicalLattice β] (f : C(α, β)) (x : α) : |f| x = |f x|

@[simp]

theorem ContinuousMap.mabs_apply {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [TopologicalSpace β] [Group β] [TopologicalGroup β] [Lattice β] [TopologicalLattice β] (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} [TopologicalSpace α] [TopologicalSpace β] [Star β] [ContinuousStar β] : Star C(α, β)

Equations

• ContinuousMap.instStar = { star := fun (f : C(α, β)) => starContinuousMap.comp f }

@[simp]

theorem ContinuousMap.coe_star {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [Star β] [ContinuousStar β] (f : C(α, β)) : ⇑(star f) = star ⇑f

@[simp]

theorem ContinuousMap.star_apply {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [Star β] [ContinuousStar β] (f : C(α, β)) (x : α) : (star f) x = star (f x)

instance ContinuousMap.instTrivialStar {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [Star β] [ContinuousStar β] [TrivialStar β] : TrivialStar C(α, β)

Equations

• ⋯ = ⋯

instance ContinuousMap.instInvolutiveStarOfContinuousStar {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [InvolutiveStar β] [ContinuousStar β] : InvolutiveStar C(α, β)

Equations

• ContinuousMap.instInvolutiveStarOfContinuousStar = InvolutiveStar.mk ⋯

instance ContinuousMap.starAddMonoid {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [AddMonoid β] [ContinuousAdd β] [StarAddMonoid β] [ContinuousStar β] : StarAddMonoid C(α, β)

Equations

• ContinuousMap.starAddMonoid = StarAddMonoid.mk ⋯

instance ContinuousMap.starMul {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [Mul β] [ContinuousMul β] [StarMul β] [ContinuousStar β] : StarMul C(α, β)

Equations

• ContinuousMap.starMul = StarMul.mk ⋯

instance ContinuousMap.instStarRingOfContinuousStar {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [NonUnitalNonAssocSemiring β] [TopologicalSemiring β] [StarRing β] [ContinuousStar β] : StarRing C(α, β)

Equations

• ContinuousMap.instStarRingOfContinuousStar = StarRing.mk ⋯

instance ContinuousMap.instStarModule {R : Type u_1} {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [Star R] [Star β] [SMul R β] [StarModule R β] [ContinuousStar β] [ContinuousConstSMul R β] : StarModule R C(α, β)

Equations

• ⋯ = ⋯

@[simp]

theorem ContinuousMap.compStarAlgHom'_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (𝕜 : Type u_4) [CommSemiring 𝕜] (A : Type u_5) [TopologicalSpace A] [Semiring A] [TopologicalSemiring A] [Star A] [ContinuousStar A] [Algebra 𝕜 A] (f : C(X, Y)) (g : C(Y, A)) : (ContinuousMap.compStarAlgHom' 𝕜 A f) g = g.comp f

def ContinuousMap.compStarAlgHom' {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (𝕜 : Type u_4) [CommSemiring 𝕜] (A : Type u_5) [TopologicalSpace A] [Semiring A] [TopologicalSemiring A] [Star A] [ContinuousStar A] [Algebra 𝕜 A] (f : C(X, Y)) : C(Y, A) →⋆ₐ[𝕜] C(X, A)

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

• ContinuousMap.compStarAlgHom' 𝕜 A f = { toFun := fun (g : C(Y, A)) => g.comp f, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯, map_star' := ⋯ }

theorem ContinuousMap.compStarAlgHom'_id {X : Type u_1} [TopologicalSpace X] (𝕜 : Type u_4) [CommSemiring 𝕜] (A : Type u_5) [TopologicalSpace A] [Semiring A] [TopologicalSemiring A] [Star A] [ContinuousStar A] [Algebra 𝕜 A] : ContinuousMap.compStarAlgHom' 𝕜 A (ContinuousMap.id X) = StarAlgHom.id 𝕜 C(X, 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} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (𝕜 : Type u_4) [CommSemiring 𝕜] (A : Type u_5) [TopologicalSpace A] [Semiring A] [TopologicalSemiring A] [Star A] [ContinuousStar A] [Algebra 𝕜 A] (g : C(Y, Z)) (f : C(X, Y)) : ContinuousMap.compStarAlgHom' 𝕜 A (g.comp f) = (ContinuousMap.compStarAlgHom' 𝕜 A f).comp (ContinuousMap.compStarAlgHom' 𝕜 A g)

ContinuousMap.compStarAlgHom' is functorial.

@[simp]

theorem ContinuousMap.compStarAlgHom_apply (X : Type u_1) {𝕜 : Type u_2} {A : Type u_3} {B : Type u_4} [TopologicalSpace X] [CommSemiring 𝕜] [TopologicalSpace A] [Semiring A] [TopologicalSemiring A] [Star A] [ContinuousStar A] [Algebra 𝕜 A] [TopologicalSpace B] [Semiring B] [TopologicalSemiring B] [Star B] [ContinuousStar B] [Algebra 𝕜 B] (φ : A →⋆ₐ[𝕜] B) (hφ : Continuous ⇑φ) (f : C(X, A)) : (ContinuousMap.compStarAlgHom X φ hφ) f = { toFun := ⇑φ, continuous_toFun := hφ }.comp f

def ContinuousMap.compStarAlgHom (X : Type u_1) {𝕜 : Type u_2} {A : Type u_3} {B : Type u_4} [TopologicalSpace X] [CommSemiring 𝕜] [TopologicalSpace A] [Semiring A] [TopologicalSemiring A] [Star A] [ContinuousStar A] [Algebra 𝕜 A] [TopologicalSpace B] [Semiring B] [TopologicalSemiring B] [Star B] [ContinuousStar B] [Algebra 𝕜 B] (φ : A →⋆ₐ[𝕜] B) (hφ : Continuous ⇑φ) : C(X, A) →⋆ₐ[𝕜] C(X, B)

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.

theorem ContinuousMap.compStarAlgHom_id (X : Type u_1) {𝕜 : Type u_2} {A : Type u_3} [TopologicalSpace X] [CommSemiring 𝕜] [TopologicalSpace A] [Semiring A] [TopologicalSemiring A] [Star A] [ContinuousStar A] [Algebra 𝕜 A] : ContinuousMap.compStarAlgHom X (StarAlgHom.id 𝕜 A) ⋯ = StarAlgHom.id 𝕜 C(X, 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} [TopologicalSpace X] [CommSemiring 𝕜] [TopologicalSpace A] [Semiring A] [TopologicalSemiring A] [Star A] [ContinuousStar A] [Algebra 𝕜 A] [TopologicalSpace B] [Semiring B] [TopologicalSemiring B] [Star B] [ContinuousStar B] [Algebra 𝕜 B] [TopologicalSpace C] [Semiring C] [TopologicalSemiring C] [Star C] [ContinuousStar C] [Algebra 𝕜 C] (φ : A →⋆ₐ[𝕜] B) (ψ : B →⋆ₐ[𝕜] C) (hφ : Continuous ⇑φ) (hψ : Continuous ⇑ψ) : ContinuousMap.compStarAlgHom X (ψ.comp φ) ⋯ = (ContinuousMap.compStarAlgHom X ψ hψ).comp (ContinuousMap.compStarAlgHom X φ hφ)

ContinuousMap.compStarAlgHom is functorial.

Summing translates of a function

theorem ContinuousMap.periodic_tsum_comp_add_zsmul {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [AddCommGroup X] [TopologicalAddGroup X] [AddCommMonoid Y] [ContinuousAdd Y] [T2Space Y] (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} [TopologicalSpace X] [TopologicalSpace Y] (𝕜 : Type u_3) [CommSemiring 𝕜] (A : Type u_4) [TopologicalSpace A] [Semiring A] [TopologicalSemiring A] [StarRing A] [ContinuousStar A] [Algebra 𝕜 A] (f : X ≃ₜ Y) (a : C(Y, A)) : (Homeomorph.compStarAlgEquiv' 𝕜 A f) a = (ContinuousMap.compStarAlgHom' 𝕜 A f.toContinuousMap) a

@[simp]

theorem Homeomorph.compStarAlgEquiv'_symm_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (𝕜 : Type u_3) [CommSemiring 𝕜] (A : Type u_4) [TopologicalSpace A] [Semiring A] [TopologicalSemiring A] [StarRing A] [ContinuousStar A] [Algebra 𝕜 A] (f : X ≃ₜ Y) (a : C(X, A)) : (Homeomorph.compStarAlgEquiv' 𝕜 A f).symm a = (ContinuousMap.compStarAlgHom' 𝕜 A f.symm.toContinuousMap) a

def Homeomorph.compStarAlgEquiv' {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (𝕜 : Type u_3) [CommSemiring 𝕜] (A : Type u_4) [TopologicalSpace A] [Semiring A] [TopologicalSemiring A] [StarRing A] [ContinuousStar A] [Algebra 𝕜 A] (f : X ≃ₜ Y) : C(Y, A) ≃⋆ₐ[𝕜] C(X, A)

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.

Evaluation as a bundled map

@[simp]

theorem ContinuousMap.evalAlgHom_apply {X : Type u_1} (S : Type u_2) (R : Type u_3) [TopologicalSpace X] [CommSemiring S] [CommSemiring R] [Algebra S R] [TopologicalSpace R] [TopologicalSemiring R] (x : X) (f : C(X, R)) : (ContinuousMap.evalAlgHom S R x) f = f x

def ContinuousMap.evalAlgHom {X : Type u_1} (S : Type u_2) (R : Type u_3) [TopologicalSpace X] [CommSemiring S] [CommSemiring R] [Algebra S R] [TopologicalSpace R] [TopologicalSemiring R] (x : X) : C(X, R) →ₐ[S] R

Evaluation of continuous maps at a point, bundled as an algebra homomorphism.

Equations

• ContinuousMap.evalAlgHom S R x = { toFun := fun (f : C(X, R)) => f x, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }

@[simp]

theorem ContinuousMap.evalStarAlgHom_apply {X : Type u_1} (S : Type u_2) (R : Type u_3) [TopologicalSpace X] [CommSemiring S] [CommSemiring R] [Algebra S R] [TopologicalSpace R] [TopologicalSemiring R] [StarRing R] [ContinuousStar R] (x : X) (f : C(X, R)) : (ContinuousMap.evalStarAlgHom S R x) f = f x

def ContinuousMap.evalStarAlgHom {X : Type u_1} (S : Type u_2) (R : Type u_3) [TopologicalSpace X] [CommSemiring S] [CommSemiring R] [Algebra S R] [TopologicalSpace R] [TopologicalSemiring R] [StarRing R] [ContinuousStar R] (x : X) : C(X, R) →⋆ₐ[S] R

Evaluation of continuous maps at a point, bundled as a star algebra homomorphism.

Equations

• ContinuousMap.evalStarAlgHom S R x = { toAlgHom := ContinuousMap.evalAlgHom S R x, map_star' := ⋯ }