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 => α → β

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem ContinuousMap.instNegContinuousMap.proof_1 {α : Type u_2} {β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] [AddGroup β] [TopologicalAddGroup β] (f : C(α, β)) : Continuous fun x => -↑f x

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

@[simp]

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

@[simp]

theorem ContinuousMap.coe_inv {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Group β] [TopologicalGroup β] (f : C(α, β)) : ↑f⁻¹ = (↑f)⁻¹

@[simp]

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

@[simp]

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

@[simp]

theorem ContinuousMap.neg_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [AddGroup γ] [TopologicalAddGroup γ] (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 γ] [Group γ] [TopologicalGroup γ] (f : C(β, γ)) (g : C(α, β)) : ContinuousMap.comp f⁻¹ g = (ContinuousMap.comp f g)⁻¹

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

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

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

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

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

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

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_2) (β : Type u_1) [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 α → β.

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

The Submonoid of continuous maps α → β.

theorem continuousAddSubgroup.proof_1 (α : Type u_1) (β : Type u_2) [TopologicalSpace α] [TopologicalSpace β] [AddGroup β] [TopologicalAddGroup β] : 0 ∈ (continuousAddSubmonoid α β).toAddSubsemigroup.carrier

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

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

The AddSubgroup of continuous maps α → β.

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

The subgroup of continuous maps α → β.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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.

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

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.

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(α, β)), ZeroHom.toFun { toFun := fun f => ContinuousMap.comp (ContinuousMap.mk ↑g) f, map_zero' := (_ : (fun f => ContinuousMap.comp (ContinuousMap.mk ↑g) f) 0 = 0) } (x + x_1) = ZeroHom.toFun { toFun := fun f => ContinuousMap.comp (ContinuousMap.mk ↑g) f, map_zero' := (_ : (fun f => ContinuousMap.comp (ContinuousMap.mk ↑g) f) 0 = 0) } x + ZeroHom.toFun { toFun := fun f => ContinuousMap.comp (ContinuousMap.mk ↑g) f, map_zero' := (_ : (fun f => ContinuousMap.comp (ContinuousMap.mk ↑g) f) 0 = 0) } 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 => ContinuousMap.comp (ContinuousMap.mk ↑g) f) 0 = 0

@[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 (ContinuousMap.mk ↑g) f

@[simp]

theorem AddMonoidHom.compLeftContinuous_apply (α : Type u_1) {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {γ : Type u_3} [AddMonoid β] [ContinuousAdd β] [TopologicalSpace γ] [AddMonoid γ] [ContinuousAdd γ] (g : β →+ γ) (hg : Continuous ↑g) (f : C(α, β)) : ↑(AddMonoidHom.compLeftContinuous α g hg) f = ContinuousMap.comp (ContinuousMap.mk ↑g) 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.

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

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

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

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

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

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_4 {α : Type u_2} {β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] [AddGroup β] [TopologicalAddGroup β] (f : C(α, β)) (n : ℕ) : ↑(n • f) = n • ↑f

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

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

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

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

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

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

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

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

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

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

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

theorem ContinuousMap.instAddCommGroupContinuousMap.proof_4 {α : 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(α, β)) (z : ℤ) : ↑(z • f) = z • ↑f

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

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

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

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

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 α → β.

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

The subring of continuous maps α → β.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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)

theorem ContinuousMap.instContinuousConstVAddContinuousMapCompactOpenInstVAdd.proof_1 {α : Type u_1} [TopologicalSpace α] {R : Type u_2} {M : Type u_3} [TopologicalSpace M] [LocallyCompactSpace α] [VAdd R M] [ContinuousConstVAdd R M] : ContinuousConstVAdd R C(α, M)

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)

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)

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)

theorem ContinuousMap.instContinuousVAddContinuousMapInstVAddContinuousConstVAddCompactOpen.proof_1 {α : Type u_1} [TopologicalSpace α] {R : Type u_2} {M : Type u_3} [TopologicalSpace M] [LocallyCompactSpace α] [TopologicalSpace R] [VAdd R M] [ContinuousVAdd R M] : ContinuousVAdd R C(α, M)

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)

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

@[simp]

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

theorem ContinuousMap.instVAddCommClassContinuousMapInstVAddInstVAdd.proof_1 {α : Type u_1} [TopologicalSpace α] {R : Type u_2} {R₁ : Type u_3} {M : Type u_4} [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.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)

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)

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)

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)

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)

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)

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)

@[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 = ZeroHom.toFun (↑(AddMonoidHom.compLeftContinuous α (LinearMap.toAddMonoidHom ↑g) (_ : Continuous ↑g))) 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.

@[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 = ZeroHom.toFun C(α, M) (α → M) AddZeroClass.toZero AddZeroClass.toZero (↑ContinuousMap.coeFnAddMonoidHom) 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.

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.

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.

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

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

@[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 normed ring by a continuous map is an algebra homomorphism.

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

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

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

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

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

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)

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)

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 => x + x_1) fun x x_1 => x ≤ x_1

theorem ContinuousMap.instCovariantClass_add_le_left.proof_1 {α : 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 => x + x_1) fun x x_1 => x ≤ x_1

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 => x * x_1) fun x x_1 => x ≤ x_1

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 => x + x_1) fun x x_1 => x ≤ x_1

theorem ContinuousMap.instCovariantClass_add_le_right.proof_1 {α : 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 => x + x_1) fun x x_1 => x ≤ x_1

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 => x * x_1) fun x x_1 => x ≤ x_1

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

@[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.instInvolutiveStarContinuousMap {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [InvolutiveStar β] [ContinuousStar β] : InvolutiveStar C(α, β)

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

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

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

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

@[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] [StarRing 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] [StarRing 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.

theorem ContinuousMap.compStarAlgHom'_id {X : Type u_1} [TopologicalSpace X] (𝕜 : Type u_4) [CommSemiring 𝕜] (A : Type u_5) [TopologicalSpace A] [Semiring A] [TopologicalSemiring A] [StarRing 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] [StarRing 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.

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.