Documentation

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

Note that one should never use the structure projection ContinuousMapZero.toContinuousMap and instead favor the coercion (↑) : C(X, R)₀ → C(X, R) available from the instance of ContinuousMapClass. All the instances on C(X, R)₀ from C(X, R) passes through this coercion, not the structure projection. Of course, the two are definitionally equal, but not reducibly so.

  • toFun : XR
  • 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

    The type of continuous maps which map zero to zero.

    Note that one should never use the structure projection ContinuousMapZero.toContinuousMap and instead favor the coercion (↑) : C(X, R)₀ → C(X, R) available from the instance of ContinuousMapClass. All the instances on C(X, R)₀ from C(X, R) passes through this coercion, not the structure projection. Of course, the two are definitionally equal, but not reducibly so.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      Equations
      • ContinuousMapZero.instFunLike = { coe := fun (f : ContinuousMapZero X R) => f.toFun, coe_injective' := }
      Equations
      • =
      theorem ContinuousMapZero.ext_iff {X : Type u_1} {R : Type u_3} [Zero X] [Zero R] [TopologicalSpace X] [TopologicalSpace R] {f : ContinuousMapZero X R} {g : ContinuousMapZero X R} :
      f = g ∀ (x : X), f x = g x
      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
      theorem ContinuousMapZero.range_toContinuousMap {X : Type u_1} {R : Type u_3} [Zero X] [Zero R] [TopologicalSpace X] [TopologicalSpace R] :
      Set.range toContinuousMap = {f : C(X, R) | f 0 = 0}

      Composition of continuous maps which map zero to zero.

      Equations
      • g.comp f = { toContinuousMap := (↑g).comp f, 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)
        Equations
        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
        Equations
        Equations
        • =
        Equations
        • =
        Equations
        • =
        Equations
        • =
        Equations
        • =
        Equations
        • =
        @[deprecated ContinuousMapZero.isClosedEmbedding_toContinuousMap]

        Alias of ContinuousMapZero.isClosedEmbedding_toContinuousMap.

        theorem ContinuousMapZero.continuous_comp_left {X : Type u_4} {Y : Type u_5} {Z : Type u_6} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [Zero X] [Zero Y] [Zero Z] (f : ContinuousMapZero X Y) :
        Continuous fun (g : ContinuousMapZero Y Z) => g.comp f
        @[simp]
        theorem ContinuousMapZero.id_toFun {R : Type u_3} [Zero R] [TopologicalSpace R] {s : Set R} [Zero s] (h0 : 0 = 0) :
        ∀ (a : s), (ContinuousMapZero.id h0) a = a
        def ContinuousMapZero.id {R : Type u_3} [Zero R] [TopologicalSpace R] {s : Set R} [Zero s] (h0 : 0 = 0) :

        The identity function as an element of C(s, R)₀ when 0 ∈ (s : Set R).

        Equations
        Instances For
          Equations
          • ContinuousMapZero.instZero = { zero := { toContinuousMap := 0, map_zero' := } }
          @[simp]
          theorem ContinuousMapZero.coe_zero {X : Type u_1} {R : Type u_2} [Zero X] [TopologicalSpace X] [TopologicalSpace R] [Zero R] :
          0 = 0
          Equations
          • ContinuousMapZero.instAdd = { add := fun (f g : ContinuousMapZero X R) => { toContinuousMap := f + g, map_zero' := } }
          @[simp]
          theorem ContinuousMapZero.coe_add {X : Type u_1} {R : Type u_2} [Zero X] [TopologicalSpace X] [TopologicalSpace R] [AddZeroClass R] [ContinuousAdd R] (f : ContinuousMapZero X R) (g : ContinuousMapZero X R) :
          (f + g) = f + g
          Equations
          • ContinuousMapZero.instMul = { mul := fun (f g : ContinuousMapZero X R) => { toContinuousMap := f * g, map_zero' := } }
          @[simp]
          theorem ContinuousMapZero.coe_mul {X : Type u_1} {R : Type u_2} [Zero X] [TopologicalSpace X] [TopologicalSpace R] [MulZeroClass R] [ContinuousMul R] (f : ContinuousMapZero X R) (g : ContinuousMapZero X R) :
          (f * g) = f * g
          Equations
          • ContinuousMapZero.instSMul = { smul := fun (m : M) (f : ContinuousMapZero X R) => { toContinuousMap := m f, map_zero' := } }
          @[simp]
          theorem ContinuousMapZero.coe_smul {X : Type u_1} {R : Type u_2} [Zero X] [TopologicalSpace X] [TopologicalSpace R] {M : Type u_3} [Zero R] [SMulZeroClass M R] [ContinuousConstSMul M R] (m : M) (f : ContinuousMapZero X R) :
          (m f) = m f
          Equations
          Equations
          Equations
          • =
          Equations
          instance ContinuousMapZero.instCanLift {X : Type u_1} {R : Type u_2} [Zero X] [TopologicalSpace X] [TopologicalSpace R] [CommSemiring R] :
          CanLift C(X, R) (ContinuousMapZero X R) toContinuousMap fun (f : C(X, R)) => f 0 = 0
          Equations
          • =
          @[simp]
          theorem ContinuousMapZero.toContinuousMapHom_apply {X : Type u_1} {R : Type u_2} [Zero X] [TopologicalSpace X] [TopologicalSpace R] [CommSemiring R] [TopologicalSemiring R] [StarRing R] [ContinuousStar R] (f : ContinuousMapZero X R) :
          ContinuousMapZero.toContinuousMapHom f = f

          The coercion C(X, R)₀ → C(X, R) bundled as a non-unital star algebra homomorphism.

          Equations
          • ContinuousMapZero.toContinuousMapHom = { toFun := fun (f : ContinuousMapZero X R) => f, map_smul' := , map_zero' := , map_add' := , map_mul' := , map_star' := }
          Instances For
            theorem ContinuousMapZero.coe_toContinuousMapHom {X : Type u_1} {R : Type u_2} [Zero X] [TopologicalSpace X] [TopologicalSpace R] [CommSemiring R] [TopologicalSemiring R] [StarRing R] [ContinuousStar R] :
            ContinuousMapZero.toContinuousMapHom = toContinuousMap

            The coercion C(X, R)₀ → C(X, R) bundled as a continuous linear map.

            Equations
            Instances For
              def ContinuousMapZero.evalCLM {X : Type u_1} [Zero X] [TopologicalSpace X] (𝕜 : Type u_3) {R : Type u_4} [CompactSpace X] [NormedField 𝕜] [NormedCommRing R] [NormedSpace 𝕜 R] (x : X) :

              The evaluation at a point, as a continuous linear map from C(X, R)₀ to R.

              Equations
              Instances For
                @[simp]
                theorem ContinuousMapZero.evalCLM_apply {X : Type u_1} [Zero X] [TopologicalSpace X] {𝕜 : Type u_3} {R : Type u_4} [CompactSpace X] [NormedField 𝕜] [NormedCommRing R] [NormedSpace 𝕜 R] (x : X) (f : ContinuousMapZero X R) :

                Coercion to a function as an AddMonoidHom. Similar to ContinuousMap.coeFnAddMonoidHom.

                Equations
                • ContinuousMapZero.coeFnAddMonoidHom = { toFun := fun (f : ContinuousMapZero X R) => f, map_zero' := , map_add' := }
                Instances For
                  @[simp]
                  theorem ContinuousMapZero.coe_sum {X : Type u_1} {R : Type u_2} [Zero X] [TopologicalSpace X] [TopologicalSpace R] [CommSemiring R] [TopologicalSemiring R] {ι : Type u_3} (s : Finset ι) (f : ιContinuousMapZero X R) :
                  (s.sum f) = is, (f i)
                  Equations
                  • ContinuousMapZero.instSub = { sub := fun (f g : ContinuousMapZero X R) => { toContinuousMap := f - g, map_zero' := } }
                  Equations
                  • ContinuousMapZero.instNeg = { neg := fun (f : ContinuousMapZero X R) => { toContinuousMap := -f, map_zero' := } }
                  Equations
                  @[simp]
                  theorem ContinuousMapZero.coe_neg {X : Type u_3} {R : Type u_4} [Zero X] [TopologicalSpace X] [CommRing R] [TopologicalSpace R] [TopologicalRing R] (f : ContinuousMapZero X R) :
                  (-f) = -f
                  Equations
                  • ContinuousMapZero.instUniformSpace = UniformSpace.comap ContinuousMapZero.toContinuousMap inferInstance
                  @[deprecated ContinuousMapZero.isUniformEmbedding_toContinuousMap]

                  Alias of ContinuousMapZero.isUniformEmbedding_toContinuousMap.

                  theorem ContinuousMapZero.isUniformEmbedding_comp {X : Type u_1} {R : Type u_2} [Zero X] [TopologicalSpace X] [Zero R] [UniformSpace R] {Y : Type u_3} [UniformSpace Y] [Zero Y] (g : ContinuousMapZero Y R) (hg : IsUniformEmbedding g) :
                  IsUniformEmbedding fun (x : ContinuousMapZero X Y) => g.comp x
                  @[deprecated ContinuousMapZero.isUniformEmbedding_comp]
                  theorem ContinuousMapZero.uniformEmbedding_comp {X : Type u_1} {R : Type u_2} [Zero X] [TopologicalSpace X] [Zero R] [UniformSpace R] {Y : Type u_3} [UniformSpace Y] [Zero Y] (g : ContinuousMapZero Y R) (hg : IsUniformEmbedding g) :
                  IsUniformEmbedding fun (x : ContinuousMapZero X Y) => g.comp x

                  Alias of ContinuousMapZero.isUniformEmbedding_comp.

                  def UniformEquiv.arrowCongrLeft₀ {X : Type u_1} {R : Type u_2} [Zero X] [TopologicalSpace X] [Zero R] [UniformSpace R] {Y : Type u_3} [TopologicalSpace Y] [Zero Y] (f : X ≃ₜ Y) (hf : f 0 = 0) :

                  The uniform equivalence C(X, R)₀ ≃ᵤ C(Y, R)₀ induced by a homeomorphism of the domains sending 0 : X to 0 : Y.

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

                    The functor C(·, R)₀ from topological spaces with zero (and ContinuousMapZero maps) to non-unital star algebras.

                    Equations
                    Instances For
                      @[simp]
                      theorem ContinuousMapZero.nonUnitalStarAlgHom_postcomp_apply (X : Type u_1) {M : Type u_3} {R : Type u_4} {S : Type u_5} [Zero X] [CommSemiring M] [TopologicalSpace X] [TopologicalSpace R] [TopologicalSpace S] [CommSemiring R] [StarRing R] [TopologicalSemiring R] [ContinuousStar R] [CommSemiring S] [StarRing S] [TopologicalSemiring S] [ContinuousStar S] [Module M R] [Module M S] [ContinuousConstSMul M R] [ContinuousConstSMul M S] (φ : R →⋆ₙₐ[M] S) (hφ : Continuous φ) (f : ContinuousMapZero X R) :
                      (ContinuousMapZero.nonUnitalStarAlgHom_postcomp X φ ) f = { toFun := φ, continuous_toFun := , map_zero' := }.comp f

                      The functor C(X, ·)₀ from non-unital topological star algebras (with non-unital continuous star homomorphisms) to non-unital star algebras.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        noncomputable instance ContinuousMapZero.instMetricSpace {α : Type u_1} {R : Type u_3} [TopologicalSpace α] [CompactSpace α] [Zero α] [MetricSpace R] [Zero R] :
                        Equations
                        noncomputable instance ContinuousMapZero.instNorm {α : Type u_1} {R : Type u_3} [TopologicalSpace α] [CompactSpace α] [Zero α] [NormedAddCommGroup R] :
                        Equations
                        Equations
                        Equations
                        Equations
                        • =