Documentation

Mathlib.Topology.ContinuousFunction.ContinuousMapZero

Continuous maps sending zero to zero #

This is the type of continuous maps from X to R such that (0 : X) ↦ (0 : R) for which we provide the scoped notation C(X, R)₀. We provide this as a dedicated type solely for the non-unital continuous functional calculus, as using various terms of type Ideal C(X, R) were overly burdensome on type class synthesis.

Of course, one could generalize to maps between pointed topological spaces, but that goes beyond the purpose of this type.

structure ContinuousMapZero (X : Type u_1) (R : Type u_2) [Zero X] [Zero R] [TopologicalSpace X] [TopologicalSpace R] extends ContinuousMap :

Type (max u_1 u_2)

The type of continuous maps which map zero to zero.

toFun : X → R
continuous_toFun : Continuous self.toFun
map_zero' : self.toContinuousMap 0 = 0

Instances For

theorem ContinuousMapZero.map_zero' {X : Type u_1} {R : Type u_2} [Zero X] [Zero R] [TopologicalSpace X] [TopologicalSpace R] (self : ContinuousMapZero X R) :

self.toContinuousMap 0 = 0

def ContinuousMapZero.«termC(_,_)₀» :

Lean.ParserDescr

The type of continuous maps which map zero to zero.

Equations

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

Instances For

instance ContinuousMapZero.instFunLike {X : Type u_1} {R : Type u_3} [Zero X] [Zero R] [TopologicalSpace X] [TopologicalSpace R] :

FunLike (ContinuousMapZero X R) X R

Equations

ContinuousMapZero.instFunLike = { coe := fun (f : ContinuousMapZero X R) => f.toFun, coe_injective' := ⋯ }

instance ContinuousMapZero.instContinuousMapClass {X : Type u_1} {R : Type u_3} [Zero X] [Zero R] [TopologicalSpace X] [TopologicalSpace R] :

ContinuousMapClass (ContinuousMapZero X R) X R

Equations

⋯ = ⋯

instance ContinuousMapZero.instZeroHomClass {X : Type u_1} {R : Type u_3} [Zero X] [Zero R] [TopologicalSpace X] [TopologicalSpace R] :

ZeroHomClass (ContinuousMapZero X R) X R

Equations

⋯ = ⋯

theorem ContinuousMapZero.ext {X : Type u_1} {R : Type u_3} [Zero X] [Zero R] [TopologicalSpace X] [TopologicalSpace R] {f : ContinuousMapZero X R} {g : ContinuousMapZero X R} (h : ∀ (x : X), f x = g x) :

f = g

@[simp]

theorem ContinuousMapZero.coe_mk {X : Type u_1} {R : Type u_3} [Zero X] [Zero R] [TopologicalSpace X] [TopologicalSpace R] {f : C(X, R)} {h0 : f 0 = 0} :

⇑{ toContinuousMap := f, map_zero' := h0 } = ⇑f

def ContinuousMapZero.comp {X : Type u_1} {Y : Type u_2} {R : Type u_3} [Zero X] [Zero Y] [Zero R] [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace R] (g : ContinuousMapZero Y R) (f : ContinuousMapZero X Y) :

ContinuousMapZero X R

Composition of continuous maps which map zero to zero.

Equations

g.comp f = { toContinuousMap := g.comp f.toContinuousMap, map_zero' := ⋯ }

Instances For

@[simp]

theorem ContinuousMapZero.comp_apply {X : Type u_1} {Y : Type u_2} {R : Type u_3} [Zero X] [Zero Y] [Zero R] [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace R] (g : ContinuousMapZero Y R) (f : ContinuousMapZero X Y) (x : X) :

(g.comp f) x = g (f x)

instance ContinuousMapZero.instPartialOrder {X : Type u_1} {R : Type u_3} [Zero X] [Zero R] [TopologicalSpace X] [TopologicalSpace R] [PartialOrder R] :

PartialOrder (ContinuousMapZero X R)

Equations

ContinuousMapZero.instPartialOrder = PartialOrder.lift DFunLike.coe ⋯

theorem ContinuousMapZero.le_def {X : Type u_1} {R : Type u_3} [Zero X] [Zero R] [TopologicalSpace X] [TopologicalSpace R] [PartialOrder R] (f : ContinuousMapZero X R) (g : ContinuousMapZero X R) :

f ≤ g ↔ ∀ (x : X), f x ≤ g x

instance ContinuousMapZero.instZero {X : Type u_1} {R : Type u_2} [Zero X] [TopologicalSpace X] [CommSemiring R] [TopologicalSpace R] :

Zero (ContinuousMapZero X R)

Equations

ContinuousMapZero.instZero = { zero := { toContinuousMap := 0, map_zero' := ⋯ } }

instance ContinuousMapZero.instAdd {X : Type u_1} {R : Type u_2} [Zero X] [TopologicalSpace X] [CommSemiring R] [TopologicalSpace R] [TopologicalSemiring R] :

Add (ContinuousMapZero X R)

Equations

ContinuousMapZero.instAdd = { add := fun (f g : ContinuousMapZero X R) => { toContinuousMap := ↑f + ↑g, map_zero' := ⋯ } }

instance ContinuousMapZero.instMul {X : Type u_1} {R : Type u_2} [Zero X] [TopologicalSpace X] [CommSemiring R] [TopologicalSpace R] [TopologicalSemiring R] :

Mul (ContinuousMapZero X R)

Equations

ContinuousMapZero.instMul = { mul := fun (f g : ContinuousMapZero X R) => { toContinuousMap := ↑f * ↑g, map_zero' := ⋯ } }

instance ContinuousMapZero.instSMul {X : Type u_1} {R : Type u_2} [Zero X] [TopologicalSpace X] [CommSemiring R] [TopologicalSpace R] {M : Type u_3} [SMulZeroClass M R] [ContinuousConstSMul M R] :

SMul M (ContinuousMapZero X R)

Equations

ContinuousMapZero.instSMul = { smul := fun (m : M) (f : ContinuousMapZero X R) => { toContinuousMap := m • ↑f, map_zero' := ⋯ } }

theorem ContinuousMapZero.toContinuousMap_injective {X : Type u_1} {R : Type u_2} [Zero X] [TopologicalSpace X] [CommSemiring R] [TopologicalSpace R] :

Function.Injective ContinuousMapZero.toContinuousMap

instance ContinuousMapZero.instNonUnitalCommSemiring {X : Type u_1} {R : Type u_2} [Zero X] [TopologicalSpace X] [CommSemiring R] [TopologicalSpace R] [TopologicalSemiring R] :

NonUnitalCommSemiring (ContinuousMapZero X R)

Equations

ContinuousMapZero.instNonUnitalCommSemiring = Function.Injective.nonUnitalCommSemiring ContinuousMapZero.toContinuousMap ⋯ ⋯ ⋯ ⋯ ⋯

instance ContinuousMapZero.instModule {X : Type u_1} {R : Type u_2} [Zero X] [TopologicalSpace X] [CommSemiring R] [TopologicalSpace R] [TopologicalSemiring R] {M : Type u_3} [Semiring M] [Module M R] [ContinuousConstSMul M R] :

Module M (ContinuousMapZero X R)

Equations

ContinuousMapZero.instModule = Function.Injective.module M { toFun := fun (self : ContinuousMapZero X R) => self.1, map_zero' := ⋯, map_add' := ⋯ } ⋯ ⋯

instance ContinuousMapZero.instSMulCommClass {X : Type u_1} {R : Type u_2} [Zero X] [TopologicalSpace X] [CommSemiring R] [TopologicalSpace R] {M : Type u_3} {N : Type u_4} [SMulZeroClass M R] [ContinuousConstSMul M R] [SMulZeroClass N R] [ContinuousConstSMul N R] [SMulCommClass M N R] :

SMulCommClass M N (ContinuousMapZero X R)

Equations

⋯ = ⋯

instance ContinuousMapZero.instIsScalarTower {X : Type u_1} {R : Type u_2} [Zero X] [TopologicalSpace X] [CommSemiring R] [TopologicalSpace R] {M : Type u_3} {N : Type u_4} [SMulZeroClass M R] [ContinuousConstSMul M R] [SMulZeroClass N R] [ContinuousConstSMul N R] [SMul M N] [IsScalarTower M N R] :

IsScalarTower M N (ContinuousMapZero X R)

Equations

⋯ = ⋯

instance ContinuousMapZero.instStarRing {X : Type u_1} {R : Type u_2} [Zero X] [TopologicalSpace X] [CommSemiring R] [TopologicalSpace R] [TopologicalSemiring R] [StarRing R] [ContinuousStar R] :

StarRing (ContinuousMapZero X R)

Equations

ContinuousMapZero.instStarRing = StarRing.mk ⋯

instance ContinuousMapZero.instTopologicalSpace {X : Type u_1} {R : Type u_2} [Zero X] [TopologicalSpace X] [CommSemiring R] [TopologicalSpace R] :

TopologicalSpace (ContinuousMapZero X R)

Equations

ContinuousMapZero.instTopologicalSpace = TopologicalSpace.induced ContinuousMapZero.toContinuousMap inferInstance

instance ContinuousMapZero.instSub {X : Type u_1} {R : Type u_2} [Zero X] [TopologicalSpace X] [CommRing R] [TopologicalSpace R] [TopologicalRing R] :

Sub (ContinuousMapZero X R)

Equations

ContinuousMapZero.instSub = { sub := fun (f g : ContinuousMapZero X R) => { toContinuousMap := ↑f - ↑g, map_zero' := ⋯ } }

instance ContinuousMapZero.instNeg {X : Type u_1} {R : Type u_2} [Zero X] [TopologicalSpace X] [CommRing R] [TopologicalSpace R] [TopologicalRing R] :

Neg (ContinuousMapZero X R)

Equations

ContinuousMapZero.instNeg = { neg := fun (f : ContinuousMapZero X R) => { toContinuousMap := -↑f, map_zero' := ⋯ } }

instance ContinuousMapZero.instNonUnitalCommRing {X : Type u_1} {R : Type u_2} [Zero X] [TopologicalSpace X] [CommRing R] [TopologicalSpace R] [TopologicalRing R] :

NonUnitalCommRing (ContinuousMapZero X R)

Equations

ContinuousMapZero.instNonUnitalCommRing = Function.Injective.nonUnitalCommRing ContinuousMapZero.toContinuousMap ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯