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.

@[implicit_reducible]

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

@[implicit_reducible]

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 := ⋯ } }

@[implicit_reducible]

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 := ⋯ } }

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem ContinuousMap.mul_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [Mul γ] [ContinuousMul γ] (f₁ f₂ : C(β, γ)) (g : C(α, β)) : (f₁ * f₂).comp g = f₁.comp g * f₂.comp g

@[simp]

theorem ContinuousMap.add_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [Add γ] [ContinuousAdd γ] (f₁ f₂ : C(β, γ)) (g : C(α, β)) : (f₁ + f₂).comp g = f₁.comp g + f₂.comp g

one

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

Nat.cast

@[implicit_reducible]

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

@[simp]

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

Int.cast

@[implicit_reducible]

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

@[simp]

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

nsmul and pow

@[implicit_reducible]

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 := ⋯ } }

@[implicit_reducible]

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

Equations

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

@[simp]

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

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

@[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_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_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

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

inv and neg

@[implicit_reducible]

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 := ⋯ } }

@[implicit_reducible]

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 := ⋯ } }

@[simp]

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

@[simp]

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

@[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_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Neg β] [ContinuousNeg β] (f : C(α, β)) (x : α) : (-f) x = -f x

@[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)⁻¹

@[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

div and sub

@[implicit_reducible]

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 := ⋯ } }

@[implicit_reducible]

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 := ⋯ } }

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem ContinuousMap.div_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [Div γ] [ContinuousDiv γ] (f g : C(β, γ)) (h : C(α, β)) : (f / g).comp h = f.comp h / g.comp h

@[simp]

theorem ContinuousMap.sub_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [Sub γ] [ContinuousSub γ] (f g : C(β, γ)) (h : C(α, β)) : (f - g).comp h = f.comp h - g.comp h

zpow and zsmul

@[implicit_reducible]

instance ContinuousMap.instZPow {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Group β] [IsTopologicalGroup β] : Pow C(α, β) ℤ

Equations

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

@[implicit_reducible]

instance ContinuousMap.instZSMul {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [AddGroup β] [IsTopologicalAddGroup β] : SMul ℤ C(α, β)

Equations

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

@[simp]

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

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

@[simp]

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

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

@[simp]

theorem ContinuousMap.zpow_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [Group γ] [IsTopologicalGroup γ] (f : C(β, γ)) (z : ℤ) (g : C(α, β)) : (f ^ z).comp g = f.comp g ^ z

theorem ContinuousMap.zsmul_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [AddGroup γ] [IsTopologicalAddGroup γ] (f : C(β, γ)) (z : ℤ) (g : C(α, β)) : (z • f).comp g = z • f.comp g

Group structure

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

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 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' := ⋯ }

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

The subgroup of continuous maps α → β.

Equations

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

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

The AddSubgroup of continuous maps α → β.

Equations

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

@[implicit_reducible]

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

Equations

• ContinuousMap.instSemigroupOfContinuousMul = { toMul := ContinuousMap.instMul, mul_assoc := ⋯ }

@[implicit_reducible]

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

Equations

• ContinuousMap.instAddSemigroupOfContinuousAdd = { toAdd := ContinuousMap.instAdd, add_assoc := ⋯ }

@[implicit_reducible]

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

Equations

• ContinuousMap.instCommSemigroupOfContinuousMul = { toSemigroup := ContinuousMap.instSemigroupOfContinuousMul, mul_comm := ⋯ }

@[implicit_reducible]

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

Equations

• ContinuousMap.instAddCommSemigroupOfContinuousAdd = { toAddSemigroup := ContinuousMap.instAddSemigroupOfContinuousAdd, add_comm := ⋯ }

@[implicit_reducible]

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

Equations

• ContinuousMap.instMulOneClassOfContinuousMul = { toOne := ContinuousMap.instOne, toMul := ContinuousMap.instMul, one_mul := ⋯, mul_one := ⋯ }

@[implicit_reducible]

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

Equations

• ContinuousMap.instAddZeroClassOfContinuousAdd = { toZero := ContinuousMap.instZero, toAdd := ContinuousMap.instAdd, zero_add := ⋯, add_zero := ⋯ }

@[implicit_reducible]

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

Equations

• ContinuousMap.instMulZeroClassOfContinuousMul = { toMul := ContinuousMap.instMul, toZero := ContinuousMap.instZero, zero_mul := ⋯, mul_zero := ⋯ }

@[implicit_reducible]

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

Equations

• ContinuousMap.instSemigroupWithZeroOfContinuousMul = { toSemigroup := ContinuousMap.instSemigroupOfContinuousMul, toZero := ContinuousMap.instZero, zero_mul := ⋯, mul_zero := ⋯ }

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

• ContinuousMap.instMonoidWithZeroOfContinuousMul = { toMonoid := ContinuousMap.instMonoidOfContinuousMul, toZero := ContinuousMap.instZero, zero_mul := ⋯, mul_zero := ⋯ }

@[implicit_reducible]

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

Equations

• ContinuousMap.instCommMonoidOfContinuousMul = { toMonoid := ContinuousMap.instMonoidOfContinuousMul, mul_comm := ⋯ }

@[implicit_reducible]

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

Equations

• ContinuousMap.instAddCommMonoidOfContinuousAdd = { toAddMonoid := ContinuousMap.instAddMonoidOfContinuousAdd, add_comm := ⋯ }

@[implicit_reducible]

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

Equations

• ContinuousMap.instCommMonoidWithZeroOfContinuousMul = { toCommMonoid := ContinuousMap.instCommMonoidOfContinuousMul, toZero := ContinuousMap.instZero, zero_mul := ⋯, mul_zero := ⋯ }

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

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

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' := ⋯ }

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 : α) : coeFnMonoidHom f a = f a

@[simp]

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

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

@[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

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' := ⋯ }

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' := ⋯ }

@[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

@[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.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)

@[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)

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.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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

• ContinuousMap.instCommGroupContinuousMap = { toGroup := ContinuousMap.instGroupOfIsTopologicalGroup, mul_comm := ⋯ }

@[implicit_reducible]

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

Equations

• ContinuousMap.instAddCommGroupContinuousMap = { toAddGroup := ContinuousMap.instAddGroupOfIsTopologicalAddGroup, add_comm := ⋯ }

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

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

theorem ContinuousMap.hasProd_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {γ : Type u_3} [CommMonoid β] [ContinuousMul β] {f : γ → C(α, β)} {g : C(α, β)} {L : SummationFilter γ} (hf : HasProd f g L) (x : α) : HasProd (fun (i : γ) => (f i) x) (g x) L

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

theorem ContinuousMap.hasSum_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {γ : Type u_3} [AddCommMonoid β] [ContinuousAdd β] {f : γ → C(α, β)} {g : C(α, β)} {L : SummationFilter γ} (hf : HasSum f g L) (x : α) : HasSum (fun (i : γ) => (f i) x) (g x) L

If 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.multipliable_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [CommMonoid β] [ContinuousMul β] {γ : Type u_3} {f : γ → C(α, β)} {L : SummationFilter γ} (hf : Multipliable f L) (x : α) : Multipliable (fun (i : γ) => (f i) x) L

theorem ContinuousMap.summable_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [AddCommMonoid β] [ContinuousAdd β] {γ : Type u_3} {f : γ → C(α, β)} {L : SummationFilter γ} (hf : Summable f L) (x : α) : Summable (fun (i : γ) => (f i) x) L

theorem ContinuousMap.tprod_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [T2Space β] [CommMonoid β] [ContinuousMul β] {γ : Type u_3} {f : γ → C(α, β)} {L : SummationFilter γ} (hf : Multipliable f L) [L.NeBot] (x : α) : ∏'[L] (i : γ), (f i) x = (∏'[L] (i : γ), f i) x

theorem ContinuousMap.tsum_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [T2Space β] [AddCommMonoid β] [ContinuousAdd β] {γ : Type u_3} {f : γ → C(α, β)} {L : SummationFilter γ} (hf : Summable f L) [L.NeBot] (x : α) : ∑'[L] (i : γ), (f i) x = (∑'[L] (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] [IsTopologicalSemiring 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] [IsTopologicalRing 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' := ⋯ }

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

• ContinuousMap.instNonUnitalSemiringOfIsTopologicalSemiring = { toNonUnitalNonAssocSemiring := ContinuousMap.instNonUnitalNonAssocSemiringOfIsTopologicalSemiring, mul_assoc := ⋯ }

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

• ContinuousMap.instNonUnitalRingOfIsTopologicalRing = { toNonUnitalNonAssocRing := ContinuousMap.instNonUnitalNonAssocRingOfIsTopologicalRing, mul_assoc := ⋯ }

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

• ContinuousMap.instNonUnitalCommSemiringOfIsTopologicalSemiring = { toNonUnitalSemiring := ContinuousMap.instNonUnitalSemiringOfIsTopologicalSemiring, mul_comm := ⋯ }

@[implicit_reducible]

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

Equations

• ContinuousMap.instCommSemiringOfIsTopologicalSemiring = { toSemiring := ContinuousMap.instSemiringOfIsTopologicalSemiring, mul_comm := ⋯ }

@[implicit_reducible]

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

Equations

• ContinuousMap.instNonUnitalCommRingOfIsTopologicalRing = { toNonUnitalRing := ContinuousMap.instNonUnitalRingOfIsTopologicalRing, mul_comm := ⋯ }

@[implicit_reducible]

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

Equations

• ContinuousMap.instCommRingOfIsTopologicalRing = { toRing := ContinuousMap.instRing, mul_comm := ⋯ }

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

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

def RingHom.compLeftContinuous (α : Type u_1) {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [Semiring β] [IsTopologicalSemiring β] [TopologicalSpace γ] [Semiring γ] [IsTopologicalSemiring γ] (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 RingHom.compLeftContinuous_apply_apply (α : Type u_1) {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [Semiring β] [IsTopologicalSemiring β] [TopologicalSpace γ] [Semiring γ] [IsTopologicalSemiring γ] (g : β →+* γ) (hg : Continuous ⇑g) (f : C(α, β)) (a✝ : α) : ((RingHom.compLeftContinuous α g hg) f) a✝ = g (f a✝)

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

Coercion to a function as a RingHom.

Equations

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

@[simp]

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

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] [IsTopologicalAddGroup 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' := ⋯ }

@[implicit_reducible]

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 := ⋯ } }

@[implicit_reducible]

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

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

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

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

@[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

@[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

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

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

@[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

@[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

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)

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)

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)

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)

instance ContinuousMap.instIsScalarTower_1 {α : Type u_1} [TopologicalSpace α] {R : Type u_3} {M : Type u_5} [TopologicalSpace M] [SMul R M] [ContinuousConstSMul R M] [Mul M] [ContinuousMul M] [IsScalarTower R M M] : IsScalarTower R C(α, M) C(α, M)

instance ContinuousMap.instSMulCommClass_1 {α : Type u_1} [TopologicalSpace α] {R : Type u_3} {M : Type u_5} [TopologicalSpace M] [SMul R M] [ContinuousConstSMul R M] [Mul M] [ContinuousMul M] [SMulCommClass R M M] : SMulCommClass R C(α, M) C(α, M)

instance ContinuousMap.instSMulCommClass_2 {α : Type u_1} [TopologicalSpace α] {R : Type u_3} {M : Type u_5} [TopologicalSpace M] [SMul R M] [ContinuousConstSMul R M] [Mul M] [ContinuousMul M] [SMulCommClass M R M] : SMulCommClass C(α, M) R C(α, M)

@[implicit_reducible]

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 = { toSMul := ContinuousMap.instSMul, mul_smul := ⋯, one_smul := ⋯ }

@[implicit_reducible]

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 = { toMulAction := ContinuousMap.instMulActionOfContinuousConstSMul, smul_zero := ⋯, smul_add := ⋯ }

@[implicit_reducible]

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 = { toDistribMulAction := ContinuousMap.instDistribMulActionOfContinuousConstSMul, add_smul := ⋯, zero_smul := ⋯ }

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) →L[R] C(α, M₂)

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

Equations

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

@[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.const (R : Type u_3) {M : Type u_5} [TopologicalSpace M] [Semiring R] [AddCommMonoid M] [ContinuousAdd M] [Module R M] [ContinuousConstSMul R M] (α : Type u_7) [TopologicalSpace α] : M →L[R] C(α, M)

The constant map x ↦ y ↦ x as a ContinuousLinearMap.

Equations

• ContinuousLinearMap.const R α = { toFun := fun (m : M) => ContinuousMap.const α m, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }

@[simp]

theorem ContinuousLinearMap.const_apply_apply (R : Type u_3) {M : Type u_5} [TopologicalSpace M] [Semiring R] [AddCommMonoid M] [ContinuousAdd M] [Module R M] [ContinuousConstSMul R M] (α : Type u_7) [TopologicalSpace α] (m : M) (x✝ : α) : ((const R α) m) x✝ = m

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' := ⋯ }

@[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✝¹ : α) : (coeFnLinearMap R) a✝ a✝¹ = (↑coeFnAddMonoidHom).toFun a✝ a✝¹

def ContinuousMap.evalCLM {α : 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] (x : α) : C(α, M) →L[R] M

Evaluation at a point, as a continuous linear map.

Equations

• ContinuousMap.evalCLM R x = { toFun := fun (f : C(α, M)) => f x, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }

@[simp]

theorem ContinuousMap.evalCLM_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] (x : α) (f : C(α, M)) : (evalCLM R x) f = f x

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 IsTopologicalSemiring.

def continuousSubalgebra {α : Type u_1} [TopologicalSpace α] {R : Type u_2} [CommSemiring R] {A : Type u_3} [TopologicalSpace A] [Semiring A] [Algebra R A] [IsTopologicalSemiring 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] [IsTopologicalSemiring 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] [IsTopologicalSemiring A] (r : R) (a : α) : (C r) a = (algebraMap R A) r

@[implicit_reducible]

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

Equations

• ContinuousMap.algebra = { toSMul := ContinuousMap.instSMul, algebraMap := ContinuousMap.C, commutes' := ⋯, smul_def' := ⋯ }

def AlgHom.compLeftContinuous (R : Type u_2) [CommSemiring R] {A : Type u_3} [TopologicalSpace A] [Semiring A] [Algebra R A] [IsTopologicalSemiring A] {A₂ : Type u_4} [TopologicalSpace A₂] [Semiring A₂] [Algebra R A₂] [IsTopologicalSemiring 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 AlgHom.compLeftContinuous_apply_apply (R : Type u_2) [CommSemiring R] {A : Type u_3} [TopologicalSpace A] [Semiring A] [Algebra R A] [IsTopologicalSemiring A] {A₂ : Type u_4} [TopologicalSpace A₂] [Semiring A₂] [Algebra R A₂] [IsTopologicalSemiring 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 ContinuousMap.compRightAlgHom (R : Type u_2) [CommSemiring R] (A : Type u_3) [TopologicalSpace A] [Semiring A] [Algebra R A] [IsTopologicalSemiring 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.compRightAlgHom_apply (R : Type u_2) [CommSemiring R] (A : Type u_3) [TopologicalSpace A] [Semiring A] [Algebra R A] [IsTopologicalSemiring A] {α : Type u_5} {β : Type u_6} [TopologicalSpace α] [TopologicalSpace β] (f : C(α, β)) (g : C(β, A)) : (compRightAlgHom R A f) g = g.comp f

theorem ContinuousMap.compRightAlgHom_continuous (R : Type u_2) [CommSemiring R] (A : Type u_3) [TopologicalSpace A] [Semiring A] [Algebra R A] [IsTopologicalSemiring A] {α : Type u_5} {β : Type u_6} [TopologicalSpace α] [TopologicalSpace β] (f : C(α, β)) : Continuous ⇑(compRightAlgHom R A f)

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

Coercion to a function as an AlgHom.

Equations

• ContinuousMap.coeFnAlgHom R = { toRingHom := ContinuousMap.coeFnRingHom, 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] [IsTopologicalSemiring A] (f : C(α, A)) (a : α) : (coeFnAlgHom R) f a = f a

@[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] [IsTopologicalSemiring 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] [IsTopologicalSemiring 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] [IsTopologicalSemiring 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 𝕜] [IsTopologicalRing 𝕜] {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] [IsTopologicalSemiring R] [Subsingleton α] : Subsingleton (Subalgebra R C(α, R))

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.

@[implicit_reducible]

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 := ⋯ } }

@[simp]

theorem ContinuousMap.coe_smul' {α : 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] (f : C(α, R)) (g : C(α, M)) : ⇑(f • g) = ⇑f • ⇑g

Coercion to a function for a scalar-valued continuous map multiplying a vector-valued one (as opposed to ContinuousMap.coe_smul which is multiplication by a constant scalar).

theorem ContinuousMap.smul_apply' {α : 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] (f : C(α, R)) (g : C(α, M)) (x : α) : (f • g) x = f x • g x

Evaluation of a scalar-valued continuous map multiplying a vector-valued one (as opposed to ContinuousMap.smul_apply which is multiplication by a constant scalar).

@[implicit_reducible]

instance ContinuousMap.module' {α : 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] [IsTopologicalSemiring R] [ContinuousAdd M] : Module C(α, R) C(α, M)

Equations

• ContinuousMap.module' = { toSMul := ContinuousMap.instSMul', mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

Evaluation as a bundled map

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] [IsTopologicalSemiring 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.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] [IsTopologicalSemiring R] (x : X) (f : C(X, R)) : (evalAlgHom S R x) f = f x