Documentation

Mathlib.Topology.ContinuousMap.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.

@[implicit_reducible]

instance ContinuousFunctions.instCoeFunElemForallSetOfContinuous {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] :

CoeFun ↑{f : α → β | Continuous f} fun (x : ↑{f : α → β | Continuous f}) => α → β

`mul` and `add` #

@[implicit_reducible]

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

Mul C(α, β)

@[implicit_reducible]

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

Add C(α, β)

@[simp]

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

⇑(f * g) = ⇑f * ⇑g

@[simp]

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

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

@[simp]

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

(f * g) x = f x * g x

@[simp]

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

(f + g) x = f x + g x

@[simp]

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

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

@[simp]

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

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

`one` #

@[implicit_reducible]

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

One C(α, β)

@[implicit_reducible]

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

Zero C(α, β)

@[simp]

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

⇑1 = 1

@[simp]

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

⇑0 = 0

@[simp]

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

1 x = 1

@[simp]

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

0 x = 0

@[simp]

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

comp 1 g = 1

@[simp]

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

comp 0 g = 0

@[simp]

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

g.comp 1 = const α (g 1)

@[simp]

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

g.comp 0 = const α (g 0)

@[simp]

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

const α 1 = 1

@[simp]

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

const α 0 = 0

`Nat.cast` #

@[implicit_reducible]

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

NatCast C(α, β)

@[simp]

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

⇑↑n = ↑n

@[simp]

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

↑n x = ↑n

`Int.cast` #

@[implicit_reducible]

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

IntCast C(α, β)

@[simp]

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

⇑↑n = ↑n

@[simp]

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

↑n x = ↑n

`nsmul` and `pow` #

@[implicit_reducible]

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

Pow C(α, β) ℕ

@[implicit_reducible]

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

SMul ℕ C(α, β)

@[simp]

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

⇑(f ^ n) = ⇑f ^ n

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

⇑(n • f) = n • ⇑f

@[simp]

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

(f ^ n) x = f x ^ n

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

(n • f) x = n • f x

@[simp]

theorem ContinuousMap.pow_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [Monoid γ] [ContinuousMul γ] (f : C(β, γ)) (n : ℕ) (g : C(α, β)) :

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

theorem ContinuousMap.nsmul_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [AddMonoid γ] [ContinuousAdd γ] (f : C(β, γ)) (n : ℕ) (g : C(α, β)) :

(n • f).comp g = n • f.comp g

`inv` and `neg` #

@[implicit_reducible]

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

Inv C(α, β)

@[implicit_reducible]

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

Neg C(α, β)

@[simp]

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

⇑f⁻¹ = (⇑f)⁻¹

@[simp]

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

⇑(-f) = -⇑f

@[simp]

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

f⁻¹ x = (f x)⁻¹

@[simp]

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

(-f) x = -f x

@[simp]

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

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

@[simp]

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

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

`div` and `sub` #

@[implicit_reducible]

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

Div C(α, β)

@[implicit_reducible]

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

Sub C(α, β)

@[simp]

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

⇑(f / g) = ⇑f / ⇑g

@[simp]

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

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

@[simp]

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

(f / g) x = f x / g x

@[simp]

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

(f - g) x = f x - g x

@[simp]

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

(f / g).comp h = f.comp h / g.comp h

@[simp]

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

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

`zpow` and `zsmul` #

@[implicit_reducible]

instance ContinuousMap.instZPow {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Group β] [IsTopologicalGroup β] :

Pow C(α, β) ℤ

@[implicit_reducible]

instance ContinuousMap.instZSMul {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [AddGroup β] [IsTopologicalAddGroup β] :

SMul ℤ C(α, β)

@[simp]

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

⇑(f ^ z) = ⇑f ^ z

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

⇑(z • f) = z • ⇑f

@[simp]

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

(f ^ z) x = f x ^ z

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

(z • f) x = z • f x

@[simp]

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

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

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

(z • f).comp g = z • f.comp g

Group structure #

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

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

Submonoid (α → β)

The Submonoid of continuous maps α → β.

Instances For

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

AddSubmonoid (α → β)

The AddSubmonoid of continuous maps α → β.

Instances For

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

Subgroup (α → β)

The subgroup of continuous maps α → β.

Instances For

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

AddSubgroup (α → β)

The AddSubgroup of continuous maps α → β.

Instances For

@[implicit_reducible]

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

Semigroup C(α, β)

@[implicit_reducible]

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

AddSemigroup C(α, β)

@[implicit_reducible]

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

CommSemigroup C(α, β)

@[implicit_reducible]

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

AddCommSemigroup C(α, β)

@[implicit_reducible]

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

MulOneClass C(α, β)

@[implicit_reducible]

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

AddZeroClass C(α, β)

@[implicit_reducible]

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

MulZeroClass C(α, β)

@[implicit_reducible]

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

SemigroupWithZero C(α, β)

@[implicit_reducible]

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

Monoid C(α, β)

@[implicit_reducible]

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

AddMonoid C(α, β)

@[implicit_reducible]

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

MonoidWithZero C(α, β)

@[implicit_reducible]

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

CommMonoid C(α, β)

@[implicit_reducible]

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

AddCommMonoid C(α, β)

@[implicit_reducible]

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

CommMonoidWithZero C(α, β)

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

ContinuousMul C(α, β)

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

ContinuousAdd C(α, β)

def ContinuousMap.coeFnMonoidHom {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Monoid β] [ContinuousMul β] :

C(α, β) →* α → β

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

Instances For

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.

Instances For

@[simp]

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

coeFnMonoidHom f a = f a

@[simp]

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

coeFnAddMonoidHom f a = f a

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

C(α, β) →* C(α, γ)

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

Instances For

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.

Instances For

@[simp]

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

(AddMonoidHom.compLeftContinuous α g hg) f = { toFun := ⇑g, continuous_toFun := hg }.comp f

@[simp]

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

(MonoidHom.compLeftContinuous α g hg) f = { toFun := ⇑g, continuous_toFun := hg }.comp f

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

C(β, γ) →* C(α, γ)

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

Instances For

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

Instances For

@[simp]

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

g.compAddMonoidHom' f = f.comp g

@[simp]

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

g.compMonoidHom' f = f.comp g

@[simp]

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

⇑(∏ i ∈ s, f i) = ∏ i ∈ s, ⇑(f i)

@[simp]

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

⇑(∑ i ∈ s, f i) = ∑ i ∈ s, ⇑(f i)

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

(∏ i ∈ s, f i) a = ∏ i ∈ s, (f i) a

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

(∑ i ∈ s, f i) a = ∑ i ∈ s, (f i) a

@[implicit_reducible]

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

Group C(α, β)

@[implicit_reducible]

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

AddGroup C(α, β)

@[implicit_reducible]

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

CommGroup C(α, β)

@[implicit_reducible]

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

AddCommGroup C(α, β)

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

IsTopologicalGroup C(α, β)

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

IsTopologicalAddGroup C(α, β)

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

HasProd (fun (i : γ) => (f i) x) (g x) L

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

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

HasSum (fun (i : γ) => (f i) x) (g x) L

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

theorem ContinuousMap.multipliable_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [CommMonoid β] [ContinuousMul β] {γ : Type u_3} {f : γ → C(α, β)} {L : SummationFilter γ} (hf : Multipliable f L) (x : α) :

Multipliable (fun (i : γ) => (f i) x) L

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

Summable (fun (i : γ) => (f i) x) L

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

∏'[L] (i : γ), (f i) x = (∏'[L] (i : γ), f i) x

theorem ContinuousMap.tsum_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [T2Space β] [AddCommMonoid β] [ContinuousAdd β] {γ : Type u_3} {f : γ → C(α, β)} {L : SummationFilter γ} (hf : Summable f L) [L.NeBot] (x : α) :

∑'[L] (i : γ), (f i) x = (∑'[L] (i : γ), f i) x

Ring structure #

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

def continuousSubsemiring (α : Type u_1) (R : Type u_2) [TopologicalSpace α] [TopologicalSpace R] [NonAssocSemiring R] [IsTopologicalSemiring R] :

Subsemiring (α → R)

The subsemiring of continuous maps α → β.

Instances For

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

Subring (α → R)

The subring of continuous maps α → β.

Instances For

@[implicit_reducible]

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

NonUnitalNonAssocSemiring C(α, β)

@[implicit_reducible]

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

NonUnitalSemiring C(α, β)

@[implicit_reducible]

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

AddMonoidWithOne C(α, β)

@[implicit_reducible]

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

NonAssocSemiring C(α, β)

@[implicit_reducible]

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

Semiring C(α, β)

@[implicit_reducible]

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

NonUnitalNonAssocRing C(α, β)

@[implicit_reducible]

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

NonUnitalRing C(α, β)

@[implicit_reducible]

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

NonAssocRing C(α, β)

@[implicit_reducible]

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

@[implicit_reducible]

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

NonUnitalCommSemiring C(α, β)

@[implicit_reducible]

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

CommSemiring C(α, β)

@[implicit_reducible]

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

NonUnitalCommRing C(α, β)

@[implicit_reducible]

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

CommRing C(α, β)

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

IsTopologicalSemiring C(α, β)

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

IsTopologicalRing C(α, β)

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

C(α, β) →+* C(α, γ)

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

Instances For

@[simp]

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

((RingHom.compLeftContinuous α g hg) f) a✝ = g (f a✝)

def ContinuousMap.coeFnRingHom {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Semiring β] [IsTopologicalSemiring β] :

C(α, β) →+* α → β

Coercion to a function as a RingHom.

Instances For

@[simp]

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

coeFnRingHom f a = f a

Module structure #

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

def continuousSubmodule (α : Type u_1) [TopologicalSpace α] (R : Type u_2) [Semiring R] (M : Type u_3) [TopologicalSpace M] [AddCommGroup M] [Module R M] [ContinuousConstSMul R M] [IsTopologicalAddGroup M] :

Submodule R (α → M)

The R-submodule of continuous maps α → M.

Instances For

@[implicit_reducible]

instance ContinuousMap.instSMul {α : Type u_1} [TopologicalSpace α] {R : Type u_3} {M : Type u_5} [TopologicalSpace M] [SMul R M] [ContinuousConstSMul R M] :

SMul R C(α, M)

@[implicit_reducible]

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

VAdd R C(α, M)

instance ContinuousMap.instContinuousConstSMul {α : Type u_1} [TopologicalSpace α] {R : Type u_3} {M : Type u_5} [TopologicalSpace M] [SMul R M] [ContinuousConstSMul R M] :

ContinuousConstSMul R C(α, M)

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

ContinuousConstVAdd R C(α, M)

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

ContinuousSMul R C(α, M)

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

ContinuousVAdd R C(α, M)

@[simp]

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

⇑(c • f) = c • ⇑f

@[simp]

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

⇑(c +ᵥ f) = c +ᵥ ⇑f

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

(c • f) a = c • f a

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

(c +ᵥ f) a = c +ᵥ f a

@[simp]

theorem ContinuousMap.smul_comp {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {R : Type u_3} {M : Type u_5} [TopologicalSpace M] [SMul R M] [ContinuousConstSMul R M] (r : R) (f : C(β, M)) (g : C(α, β)) :

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

@[simp]

theorem ContinuousMap.vadd_comp {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {R : Type u_3} {M : Type u_5} [TopologicalSpace M] [VAdd R M] [ContinuousConstVAdd R M] (r : R) (f : C(β, M)) (g : C(α, β)) :

(r +ᵥ f).comp g = r +ᵥ f.comp g

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

SMulCommClass R R₁ C(α, M)

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

VAddCommClass R R₁ C(α, M)

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

IsScalarTower R R₁ C(α, M)

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

IsCentralScalar R C(α, M)

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

IsScalarTower R C(α, M) C(α, M)

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

SMulCommClass R C(α, M) C(α, M)

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

SMulCommClass C(α, M) R C(α, M)

@[implicit_reducible]

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

MulAction R C(α, M)

@[implicit_reducible]

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

DistribMulAction R C(α, M)

@[implicit_reducible]

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

Module R C(α, M)

def ContinuousLinearMap.compLeftContinuous (R : Type u_3) {M : Type u_5} [TopologicalSpace M] {M₂ : Type u_6} [TopologicalSpace M₂] [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [ContinuousAdd M] [Module R M] [ContinuousConstSMul R M] [ContinuousAdd M₂] [Module R M₂] [ContinuousConstSMul R M₂] (α : Type u_7) [TopologicalSpace α] (g : M →L[R] M₂) :

C(α, M) →L[R] C(α, M₂)

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

Instances For

@[simp]

theorem ContinuousLinearMap.compLeftContinuous_apply (R : Type u_3) {M : Type u_5} [TopologicalSpace M] {M₂ : Type u_6} [TopologicalSpace M₂] [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [ContinuousAdd M] [Module R M] [ContinuousConstSMul R M] [ContinuousAdd M₂] [Module R M₂] [ContinuousConstSMul R M₂] (α : Type u_7) [TopologicalSpace α] (g : M →L[R] M₂) (a✝ : C(α, M)) :

(ContinuousLinearMap.compLeftContinuous R α g) a✝ = (↑(AddMonoidHom.compLeftContinuous α (↑g).toAddMonoidHom ⋯)).toFun a✝

def ContinuousLinearMap.const (R : Type u_3) {M : Type u_5} [TopologicalSpace M] [Semiring R] [AddCommMonoid M] [ContinuousAdd M] [Module R M] [ContinuousConstSMul R M] (α : Type u_7) [TopologicalSpace α] :

M →L[R] C(α, M)

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

Instances For

@[simp]

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

((const R α) m) x✝ = m

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

C(α, M) →ₗ[R] α → M

Coercion to a function as a LinearMap.

Instances For

@[simp]

theorem ContinuousMap.coeFnLinearMap_apply {α : Type u_1} [TopologicalSpace α] (R : Type u_3) {M : Type u_5} [TopologicalSpace M] [Semiring R] [AddCommMonoid M] [ContinuousAdd M] [Module R M] [ContinuousConstSMul R M] (a✝ : C(α, M)) (a✝¹ : α) :

(coeFnLinearMap R) a✝ a✝¹ = (↑coeFnAddMonoidHom).toFun a✝ a✝¹

def ContinuousMap.evalCLM {α : Type u_1} [TopologicalSpace α] (R : Type u_3) {M : Type u_5} [TopologicalSpace M] [Semiring R] [AddCommMonoid M] [ContinuousAdd M] [Module R M] [ContinuousConstSMul R M] (x : α) :

C(α, M) →L[R] M

Evaluation at a point, as a continuous linear map.

Instances For

@[simp]

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

(evalCLM R x) f = f x

Algebra structure #

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

def continuousSubalgebra {α : Type u_1} [TopologicalSpace α] {R : Type u_2} [CommSemiring R] {A : Type u_3} [TopologicalSpace A] [Semiring A] [Algebra R A] [IsTopologicalSemiring A] :

Subalgebra R (α → A)

The R-subalgebra of continuous maps α → A.

Instances For

def ContinuousMap.C {α : Type u_1} [TopologicalSpace α] {R : Type u_2} [CommSemiring R] {A : Type u_3} [TopologicalSpace A] [Semiring A] [Algebra R A] [IsTopologicalSemiring A] :

R →+* C(α, A)

Continuous constant functions as a RingHom.

Instances For

@[simp]

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

(C r) a = (algebraMap R A) r

@[implicit_reducible]

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

Algebra R C(α, A)

def AlgHom.compLeftContinuous (R : Type u_2) [CommSemiring R] {A : Type u_3} [TopologicalSpace A] [Semiring A] [Algebra R A] [IsTopologicalSemiring A] {A₂ : Type u_4} [TopologicalSpace A₂] [Semiring A₂] [Algebra R A₂] [IsTopologicalSemiring A₂] {α : Type u_5} [TopologicalSpace α] (g : A →ₐ[R] A₂) (hg : Continuous ⇑g) :

C(α, A) →ₐ[R] C(α, A₂)

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

Instances For

@[simp]

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

((AlgHom.compLeftContinuous R g hg) f) a✝ = g (f a✝)

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

C(β, A) →ₐ[R] C(α, A)

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

Instances For

@[simp]

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

(compRightAlgHom R A f) g = g.comp f

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

Continuous ⇑(compRightAlgHom R A f)

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

C(α, A) →ₐ[R] α → A

Coercion to a function as an AlgHom.

Instances For

@[simp]

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

(coeFnAlgHom R) f a = f a

@[reducible, inline]

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

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

Instances For

theorem Subalgebra.separatesPoints_monotone {α : Type u_1} [TopologicalSpace α] {R : Type u_2} [CommSemiring R] {A : Type u_3} [TopologicalSpace A] [Semiring A] [Algebra R A] [IsTopologicalSemiring A] :

Monotone fun (s : Subalgebra R C(α, A)) => s.SeparatesPoints

@[simp]

theorem algebraMap_apply {α : Type u_1} [TopologicalSpace α] {R : Type u_2} [CommSemiring R] {A : Type u_3} [TopologicalSpace A] [Semiring A] [Algebra R A] [IsTopologicalSemiring A] (k : R) (a : α) :

((algebraMap R C(α, A)) k) a = k • 1

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

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

Instances For

theorem Subalgebra.SeparatesPoints.strongly {α : Type u_1} [TopologicalSpace α] {𝕜 : Type u_5} [TopologicalSpace 𝕜] [Field 𝕜] [IsTopologicalRing 𝕜] {s : Subalgebra 𝕜 C(α, 𝕜)} (h : s.SeparatesPoints) :

(↑s).SeparatesPointsStrongly

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

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

instance ContinuousMap.subsingleton_subalgebra (α : Type u_1) [TopologicalSpace α] (R : Type u_2) [CommSemiring R] [TopologicalSpace R] [IsTopologicalSemiring R] [Subsingleton α] :

Subsingleton (Subalgebra R C(α, R))

Structure as module over scalar functions #

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

@[implicit_reducible]

instance ContinuousMap.instSMul' {α : Type u_1} [TopologicalSpace α] {R : Type u_2} [Semiring R] [TopologicalSpace R] {M : Type u_3} [TopologicalSpace M] [AddCommMonoid M] [Module R M] [ContinuousSMul R M] :

SMul C(α, R) C(α, M)

@[simp]

theorem ContinuousMap.coe_smul' {α : Type u_1} [TopologicalSpace α] {R : Type u_2} [Semiring R] [TopologicalSpace R] {M : Type u_3} [TopologicalSpace M] [AddCommMonoid M] [Module R M] [ContinuousSMul R M] (f : C(α, R)) (g : C(α, M)) :

⇑(f • g) = ⇑f • ⇑g

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

theorem ContinuousMap.smul_apply' {α : Type u_1} [TopologicalSpace α] {R : Type u_2} [Semiring R] [TopologicalSpace R] {M : Type u_3} [TopologicalSpace M] [AddCommMonoid M] [Module R M] [ContinuousSMul R M] (f : C(α, R)) (g : C(α, M)) (x : α) :

(f • g) x = f x • g x

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

@[implicit_reducible]

instance ContinuousMap.module' {α : Type u_1} [TopologicalSpace α] {R : Type u_2} [Semiring R] [TopologicalSpace R] {M : Type u_3} [TopologicalSpace M] [AddCommMonoid M] [Module R M] [ContinuousSMul R M] [IsTopologicalSemiring R] [ContinuousAdd M] :

Module C(α, R) C(α, M)

Evaluation as a bundled map #

def ContinuousMap.evalAlgHom {X : Type u_1} (S : Type u_2) (R : Type u_3) [TopologicalSpace X] [CommSemiring S] [CommSemiring R] [Algebra S R] [TopologicalSpace R] [IsTopologicalSemiring R] (x : X) :

C(X, R) →ₐ[S] R

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

Instances For

@[simp]

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

(evalAlgHom S R x) f = f x