Documentation

Mathlib.Topology.ContinuousFunction.Algebra

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

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.instAdd {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Add β] [ContinuousAdd β] :

Equations

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

instance ContinuousMap.instMul {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Mul β] [ContinuousMul β] :

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(α, β)) :

ContinuousMap.comp (f₁ + f₂) g = ContinuousMap.comp f₁ g + ContinuousMap.comp f₂ 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(α, β)) :

ContinuousMap.comp (f₁ * f₂) g = ContinuousMap.comp f₁ g * ContinuousMap.comp f₂ g

`one` #

instance ContinuousMap.instZeroContinuousMap {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Zero β] :

Equations

ContinuousMap.instZeroContinuousMap = { zero := ContinuousMap.const α 0 }

instance ContinuousMap.instOneContinuousMap {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [One β] :

Equations

ContinuousMap.instOneContinuousMap = { 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.instNatCastContinuousMap {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [NatCast β] :

NatCast C(α, β)

Equations

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

@[simp]

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

⇑↑n = ↑n

@[simp]

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

↑n x = ↑n

`Int.cast` #

instance ContinuousMap.instIntCastContinuousMap {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [IntCast β] :

IntCast C(α, β)

Equations

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

@[simp]

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

⇑↑n = ↑n

@[simp]

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

↑n x = ↑n

`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 β] (f : C(α, β)) (n : ℕ) :

⇑(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(α, β)) :

ContinuousMap.comp (n • f) g = n • ContinuousMap.comp f 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(α, β)) :

ContinuousMap.comp (f ^ n) g = ContinuousMap.comp f g ^ n

`inv` and `neg` #

instance ContinuousMap.instNegContinuousMap {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Neg β] [ContinuousNeg β] :

Equations

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

theorem ContinuousMap.instNegContinuousMap.proof_1 {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Neg β] [ContinuousNeg β] (f : C(α, β)) :

Continuous fun (x : α) => -f x

instance ContinuousMap.instInvContinuousMap {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Inv β] [ContinuousInv β] :

Equations

ContinuousMap.instInvContinuousMap = { 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(α, β)) :

ContinuousMap.comp (-f) g = -ContinuousMap.comp f g

@[simp]

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

ContinuousMap.comp f⁻¹ g = (ContinuousMap.comp f g)⁻¹

`div` and `sub` #

theorem ContinuousMap.instSubContinuousMap.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.instSubContinuousMap {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Sub β] [ContinuousSub β] :

Equations

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

instance ContinuousMap.instDivContinuousMap {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Div β] [ContinuousDiv β] :

Equations

ContinuousMap.instDivContinuousMap = { 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(α, β)) :

ContinuousMap.comp (f - g) h = ContinuousMap.comp f h - ContinuousMap.comp g 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(α, β)) :

ContinuousMap.comp (f / g) h = ContinuousMap.comp f h / ContinuousMap.comp g 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 β] (f : C(α, β)) (z : ℤ) :

⇑(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(α, β)) :

ContinuousMap.comp (z • f) g = z • ContinuousMap.comp f 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(α, β)) :

ContinuousMap.comp (f ^ z) g = ContinuousMap.comp f g ^ z

Group structure #

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

theorem continuousAddSubmonoid.proof_2 (α : Type u_1) (β : Type u_2) [TopologicalSpace α] [TopologicalSpace β] [AddZeroClass β] :

Continuous fun (x : α) => 0

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

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

AddSubmonoid (α → β)

The AddSubmonoid of continuous maps α → β.

Equations

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

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

Submonoid (α → β)

The Submonoid of continuous maps α → β.

Equations

continuousSubmonoid α β = { toSubsemigroup := { 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 α β = let __src := continuousAddSubmonoid α β; { toAddSubmonoid := __src, 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 α β = let __src := continuousSubmonoid α β; { toSubmonoid := __src, inv_mem' := ⋯ }

instance ContinuousMap.instAddSemigroupContinuousMap {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [AddSemigroup β] [ContinuousAdd β] :

AddSemigroup C(α, β)

Equations

ContinuousMap.instAddSemigroupContinuousMap = Function.Injective.addSemigroup DFunLike.coe ⋯ ⋯

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

⇑(f + g) = ⇑f + ⇑g

instance ContinuousMap.instSemigroupContinuousMap {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Semigroup β] [ContinuousMul β] :

Semigroup C(α, β)

Equations

ContinuousMap.instSemigroupContinuousMap = Function.Injective.semigroup DFunLike.coe ⋯ ⋯

instance ContinuousMap.instAddCommSemigroupContinuousMap {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [AddCommSemigroup β] [ContinuousAdd β] :

AddCommSemigroup C(α, β)

Equations

ContinuousMap.instAddCommSemigroupContinuousMap = Function.Injective.addCommSemigroup DFunLike.coe ⋯ ⋯

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

⇑(f + g) = ⇑f + ⇑g

instance ContinuousMap.instCommSemigroupContinuousMap {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [CommSemigroup β] [ContinuousMul β] :

CommSemigroup C(α, β)

Equations

ContinuousMap.instCommSemigroupContinuousMap = Function.Injective.commSemigroup DFunLike.coe ⋯ ⋯

instance ContinuousMap.instAddZeroClassContinuousMap {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [AddZeroClass β] [ContinuousAdd β] :

AddZeroClass C(α, β)

Equations

ContinuousMap.instAddZeroClassContinuousMap = Function.Injective.addZeroClass DFunLike.coe ⋯ ⋯ ⋯

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

⇑(f + g) = ⇑f + ⇑g

theorem ContinuousMap.instAddZeroClassContinuousMap.proof_1 {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [AddZeroClass β] :

⇑0 = 0

instance ContinuousMap.instMulOneClassContinuousMap {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [MulOneClass β] [ContinuousMul β] :

MulOneClass C(α, β)

Equations

ContinuousMap.instMulOneClassContinuousMap = Function.Injective.mulOneClass DFunLike.coe ⋯ ⋯ ⋯

instance ContinuousMap.instMulZeroClassContinuousMap {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [MulZeroClass β] [ContinuousMul β] :

MulZeroClass C(α, β)

Equations

ContinuousMap.instMulZeroClassContinuousMap = Function.Injective.mulZeroClass DFunLike.coe ⋯ ⋯ ⋯

instance ContinuousMap.instSemigroupWithZeroContinuousMap {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [SemigroupWithZero β] [ContinuousMul β] :

SemigroupWithZero C(α, β)

Equations

ContinuousMap.instSemigroupWithZeroContinuousMap = Function.Injective.semigroupWithZero DFunLike.coe ⋯ ⋯ ⋯

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

⇑(f + g) = ⇑f + ⇑g

instance ContinuousMap.instAddMonoidContinuousMap {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [AddMonoid β] [ContinuousAdd β] :

AddMonoid C(α, β)

Equations

ContinuousMap.instAddMonoidContinuousMap = Function.Injective.addMonoid DFunLike.coe ⋯ ⋯ ⋯ ⋯

theorem ContinuousMap.instAddMonoidContinuousMap.proof_1 {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [AddMonoid β] :

⇑0 = 0

instance ContinuousMap.instMonoidContinuousMap {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Monoid β] [ContinuousMul β] :

Monoid C(α, β)

Equations

ContinuousMap.instMonoidContinuousMap = Function.Injective.monoid DFunLike.coe ⋯ ⋯ ⋯ ⋯

instance ContinuousMap.instMonoidWithZeroContinuousMap {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [MonoidWithZero β] [ContinuousMul β] :

MonoidWithZero C(α, β)

Equations

ContinuousMap.instMonoidWithZeroContinuousMap = Function.Injective.monoidWithZero DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯

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

⇑(f + g) = ⇑f + ⇑g

instance ContinuousMap.instAddCommMonoidContinuousMap {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [AddCommMonoid β] [ContinuousAdd β] :

AddCommMonoid C(α, β)

Equations

ContinuousMap.instAddCommMonoidContinuousMap = Function.Injective.addCommMonoid DFunLike.coe ⋯ ⋯ ⋯ ⋯

theorem ContinuousMap.instAddCommMonoidContinuousMap.proof_1 {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [AddCommMonoid β] :

⇑0 = 0

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

⇑(n • f) = n • ⇑f

instance ContinuousMap.instCommMonoidContinuousMap {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [CommMonoid β] [ContinuousMul β] :

CommMonoid C(α, β)

Equations

ContinuousMap.instCommMonoidContinuousMap = Function.Injective.commMonoid DFunLike.coe ⋯ ⋯ ⋯ ⋯

instance ContinuousMap.instCommMonoidWithZeroContinuousMap {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [CommMonoidWithZero β] [ContinuousMul β] :

CommMonoidWithZero C(α, β)

Equations

ContinuousMap.instCommMonoidWithZeroContinuousMap = Function.Injective.commMonoidWithZero DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯

instance ContinuousMap.instContinuousAddContinuousMapCompactOpenInstAdd {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [LocallyCompactSpace α] [Add β] [ContinuousAdd β] :

ContinuousAdd C(α, β)

Equations

⋯ = ⋯

instance ContinuousMap.instContinuousMulContinuousMapCompactOpenInstMul {α : 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_2} {β : Type u_1} [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 = { toZeroHom := { 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 = { toOneHom := { toFun := fun (f : C(α, β)) => ⇑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

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

theorem AddMonoidHom.compLeftContinuous.proof_2 (α : Type u_2) {β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] {γ : Type u_3} [AddMonoid β] [ContinuousAdd β] [TopologicalSpace γ] [AddMonoid γ] [ContinuousAdd γ] (g : β →+ γ) (hg : Continuous ⇑g) :

∀ (x x_1 : C(α, β)), { toFun := fun (f : C(α, β)) => ContinuousMap.comp { toFun := ⇑g, continuous_toFun := hg } f, map_zero' := ⋯ }.toFun (x + x_1) = { toFun := fun (f : C(α, β)) => ContinuousMap.comp { toFun := ⇑g, continuous_toFun := hg } f, map_zero' := ⋯ }.toFun x + { toFun := fun (f : C(α, β)) => ContinuousMap.comp { toFun := ⇑g, continuous_toFun := hg } f, map_zero' := ⋯ }.toFun x_1

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(α, β)) => ContinuousMap.comp { toFun := ⇑g, continuous_toFun := hg } f) 0 = 0

@[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 = ContinuousMap.comp { toFun := ⇑g, continuous_toFun := hg } 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 = ContinuousMap.comp { toFun := ⇑g, continuous_toFun := hg } 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 = { toOneHom := { toFun := fun (f : C(α, β)) => ContinuousMap.comp { toFun := ⇑g, continuous_toFun := hg } f, map_one' := ⋯ }, map_mul' := ⋯ }

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

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

ContinuousMap.comp (f₁ + f₂) g = ContinuousMap.comp f₁ g + ContinuousMap.comp f₂ g

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

ContinuousMap.compAddMonoidHom' g = { toZeroHom := { toFun := fun (f : C(β, γ)) => ContinuousMap.comp f g, map_zero' := ⋯ }, map_add' := ⋯ }

@[simp]

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

(ContinuousMap.compMonoidHom' g) f = ContinuousMap.comp f g

@[simp]

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

(ContinuousMap.compAddMonoidHom' g) f = ContinuousMap.comp f 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

ContinuousMap.compMonoidHom' g = { toOneHom := { toFun := fun (f : C(β, γ)) => ContinuousMap.comp f 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(α, β)) :

⇑(Finset.sum s fun (i : ι) => f i) = Finset.sum s fun (i : ι) => ⇑(f i)

@[simp]

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

⇑(Finset.prod s fun (i : ι) => f i) = Finset.prod s fun (i : ι) => ⇑(f i)

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

(Finset.sum s fun (i : ι) => f i) a = Finset.sum s fun (i : ι) => (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 : α) :

(Finset.prod s fun (i : ι) => f i) a = Finset.prod s fun (i : ι) => (f i) a

instance ContinuousMap.instAddGroupContinuousMap {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [AddGroup β] [TopologicalAddGroup β] :

AddGroup C(α, β)

Equations

ContinuousMap.instAddGroupContinuousMap = Function.Injective.addGroup DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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

⇑(f + g) = ⇑f + ⇑g

theorem ContinuousMap.instAddGroupContinuousMap.proof_1 {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [AddGroup β] :

⇑0 = 0

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

⇑(f - g) = ⇑f - ⇑g

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

⇑(-f) = -⇑f

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

⇑(n • f) = n • ⇑f

instance ContinuousMap.instGroupContinuousMap {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Group β] [TopologicalGroup β] :

Group C(α, β)

Equations

ContinuousMap.instGroupContinuousMap = Function.Injective.group DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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

⇑(f - g) = ⇑f - ⇑g

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

AddCommGroup C(α, β)

Equations

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

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

⇑(-f) = -⇑f

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

ContinuousAdd β

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

ContinuousSub β

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

⇑(f + g) = ⇑f + ⇑g

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

⇑(n • f) = n • ⇑f

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

ContinuousNeg β

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

⇑0 = 0

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

⇑(z • f) = z • ⇑f

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.instTopologicalAddGroupContinuousMapCompactOpenInstAddGroupContinuousMapToAddGroup {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [AddCommGroup β] [TopologicalAddGroup β] :

TopologicalAddGroup C(α, β)

Equations

⋯ = ⋯

instance ContinuousMap.instTopologicalGroupContinuousMapCompactOpenInstGroupContinuousMapToGroup {α : 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

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

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

Subring (α → R)

The subring of continuous maps α → β.

Equations

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

instance ContinuousMap.instNonUnitalNonAssocSemiringContinuousMap {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [NonUnitalNonAssocSemiring β] [TopologicalSemiring β] :

NonUnitalNonAssocSemiring C(α, β)

Equations

ContinuousMap.instNonUnitalNonAssocSemiringContinuousMap = Function.Injective.nonUnitalNonAssocSemiring DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯

instance ContinuousMap.instNonUnitalSemiringContinuousMap {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [NonUnitalSemiring β] [TopologicalSemiring β] :

NonUnitalSemiring C(α, β)

Equations

ContinuousMap.instNonUnitalSemiringContinuousMap = Function.Injective.nonUnitalSemiring DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯

instance ContinuousMap.instAddMonoidWithOneContinuousMap {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [AddMonoidWithOne β] [ContinuousAdd β] :

AddMonoidWithOne C(α, β)

Equations

ContinuousMap.instAddMonoidWithOneContinuousMap = Function.Injective.addMonoidWithOne DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance ContinuousMap.instNonAssocSemiringContinuousMap {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [NonAssocSemiring β] [TopologicalSemiring β] :

NonAssocSemiring C(α, β)

Equations

ContinuousMap.instNonAssocSemiringContinuousMap = Function.Injective.nonAssocSemiring DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance ContinuousMap.instSemiringContinuousMap {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Semiring β] [TopologicalSemiring β] :

Semiring C(α, β)

Equations

ContinuousMap.instSemiringContinuousMap = Function.Injective.semiring DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance ContinuousMap.instNonUnitalNonAssocRingContinuousMap {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [NonUnitalNonAssocRing β] [TopologicalRing β] :

NonUnitalNonAssocRing C(α, β)

Equations

ContinuousMap.instNonUnitalNonAssocRingContinuousMap = Function.Injective.nonUnitalNonAssocRing DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance ContinuousMap.instNonUnitalRingContinuousMap {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [NonUnitalRing β] [TopologicalRing β] :

NonUnitalRing C(α, β)

Equations

ContinuousMap.instNonUnitalRingContinuousMap = Function.Injective.nonUnitalRing DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance ContinuousMap.instNonAssocRingContinuousMap {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [NonAssocRing β] [TopologicalRing β] :

NonAssocRing C(α, β)

Equations

ContinuousMap.instNonAssocRingContinuousMap = Function.Injective.nonAssocRing DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance ContinuousMap.instRingContinuousMap {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Ring β] [TopologicalRing β] :

Equations

ContinuousMap.instRingContinuousMap = Function.Injective.ring DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance ContinuousMap.instNonUnitalCommSemiringContinuousMap {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [NonUnitalCommSemiring β] [TopologicalSemiring β] :

NonUnitalCommSemiring C(α, β)

Equations

ContinuousMap.instNonUnitalCommSemiringContinuousMap = Function.Injective.nonUnitalCommSemiring DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯

instance ContinuousMap.instCommSemiringContinuousMap {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [CommSemiring β] [TopologicalSemiring β] :

CommSemiring C(α, β)

Equations

ContinuousMap.instCommSemiringContinuousMap = Function.Injective.commSemiring DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance ContinuousMap.instNonUnitalCommRingContinuousMap {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [NonUnitalCommRing β] [TopologicalRing β] :

NonUnitalCommRing C(α, β)

Equations

ContinuousMap.instNonUnitalCommRingContinuousMap = Function.Injective.nonUnitalCommRing DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance ContinuousMap.instCommRingContinuousMap {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [CommRing β] [TopologicalRing β] :

CommRing C(α, β)

Equations

ContinuousMap.instCommRingContinuousMap = Function.Injective.commRing DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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

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

@[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 = let __src := ContinuousMap.coeFnMonoidHom; let __src_1 := ContinuousMap.coeFnAddMonoidHom; { toMonoidHom := __src, 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

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

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

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.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.instContinuousConstVAddContinuousMapCompactOpenInstVAdd {α : 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.instContinuousConstSMulContinuousMapCompactOpenInstSMul {α : 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.instContinuousVAddContinuousMapInstVAddContinuousConstVAddCompactOpen {α : 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.instContinuousSMulContinuousMapInstSMulContinuousConstSMulCompactOpen {α : 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(α, β)) :

ContinuousMap.comp (r +ᵥ f) g = r +ᵥ ContinuousMap.comp f 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(α, β)) :

ContinuousMap.comp (r • f) g = r • ContinuousMap.comp f g

instance ContinuousMap.instVAddCommClassContinuousMapInstVAddInstVAdd {α : 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.instSMulCommClassContinuousMapInstSMulInstSMul {α : 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.instIsScalarTowerContinuousMapInstSMulInstSMul {α : 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.instIsCentralScalarContinuousMapInstSMulMulOppositeOp {α : 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.instMulActionContinuousMap {α : 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.instMulActionContinuousMap = Function.Injective.mulAction DFunLike.coe ⋯ ⋯

instance ContinuousMap.instDistribMulActionContinuousMapInstAddMonoidContinuousMap {α : 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.instDistribMulActionContinuousMapInstAddMonoidContinuousMap = 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 α (LinearMap.toAddMonoidHom ↑g) ⋯).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

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

@[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 = let __src := ContinuousMap.coeFnAddMonoidHom; { toAddHom := { toFun := __src.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

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

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

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

@[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 = let __src := RingHom.compLeftContinuous α g.toRingHom hg; { toRingHom := __src, 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 = ContinuousMap.comp g 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

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

@[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 = let __src := ContinuousMap.coeFnRingHom; { toRingHom := __src, commutes' := ⋯ }

@[inline, reducible]

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

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

Equations

Subalgebra.SeparatesPoints s = Set.SeparatesPoints ((fun (f : C(α, A)) => ⇑f) '' ↑s)

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)) => Subalgebra.SeparatesPoints s

@[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(α, 𝕜)) :

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

Set.SeparatesPointsStrongly s = ∀ (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 : Subalgebra.SeparatesPoints s) :

Set.SeparatesPointsStrongly ↑s

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 (x x_1 : β) => x + x_1) fun (x x_1 : β) => x ≤ x_1] :

CovariantClass C(α, β) C(α, β) (fun (x x_1 : C(α, β)) => x + x_1) fun (x x_1 : C(α, β)) => x ≤ x_1

Equations

⋯ = ⋯

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

CovariantClass C(α, β) C(α, β) (fun (x x_1 : C(α, β)) => x * x_1) fun (x x_1 : C(α, β)) => x ≤ x_1

Equations

⋯ = ⋯

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

CovariantClass C(α, β) C(α, β) (Function.swap fun (x x_1 : C(α, β)) => x + x_1) fun (x x_1 : C(α, β)) => x ≤ x_1

Equations

⋯ = ⋯

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

CovariantClass C(α, β) C(α, β) (Function.swap fun (x x_1 : C(α, β)) => x * x_1) fun (x x_1 : C(α, β)) => x ≤ x_1

Equations

⋯ = ⋯

@[simp]

theorem ContinuousMap.coe_abs {α : Type u_1} [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.instStarContinuousMap {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [Star β] [ContinuousStar β] :

Equations

ContinuousMap.instStarContinuousMap = { star := fun (f : C(α, β)) => ContinuousMap.comp starContinuousMap 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.instInvolutiveStarContinuousMap {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [InvolutiveStar β] [ContinuousStar β] :

InvolutiveStar C(α, β)

Equations

ContinuousMap.instInvolutiveStarContinuousMap = 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.instStarRingContinuousMapInstNonUnitalNonAssocSemiringContinuousMap {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [NonUnitalNonAssocSemiring β] [TopologicalSemiring β] [StarRing β] [ContinuousStar β] :

StarRing C(α, β)

Equations

ContinuousMap.instStarRingContinuousMapInstNonUnitalNonAssocSemiringContinuousMap = let __src := ContinuousMap.starAddMonoid; let __src_1 := ContinuousMap.starMul; StarRing.mk ⋯

instance ContinuousMap.instStarModuleContinuousMapInstStarContinuousMapInstSMul {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 = ContinuousMap.comp g 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

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

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 (ContinuousMap.comp g f) = StarAlgHom.comp (ContinuousMap.compStarAlgHom' 𝕜 A f) (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 = ContinuousMap.comp { toFun := ⇑φ, continuous_toFun := hφ } 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 (StarAlgHom.comp ψ φ) ⋯ = StarAlgHom.comp (ContinuousMap.compStarAlgHom X ψ hψ) (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 : ℤ), ContinuousMap.comp f (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'_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)) :

(StarAlgEquiv.symm (Homeomorph.compStarAlgEquiv' 𝕜 A f)) a = (ContinuousMap.compStarAlgHom' 𝕜 A (Homeomorph.toContinuousMap (Homeomorph.symm f))) a

@[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 (Homeomorph.toContinuousMap f)) 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.