Documentation

TauCeti.Topology.Algebra.Module.ExtendByZero

Continuous linear extension of coordinate functions by zero #

Mathlib's Function.ExtendByZero.linearMap is continuous for the product topologies of module-valued coordinates: each output coordinate is either a fixed input coordinate or zero. No finiteness assumption on the coordinate types is needed. For an injective index map, restriction recovers the original function, including when the target has unused coordinates.

This construction lets affine coordinate formulas pass to enlarged vertex sets of simplicial complexes. It uses Mathlib's existing extension by zero rather than choosing a different extension on unused coordinates.

source
theorem Function.ExtendByZero.continuous_linearMap {ι : Type u_1} {κ : Type u_2} (R : Type u_3) {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] (e : ι → κ) :
Continuous ⇑(linearMap R M e)

Mathlib's Function.ExtendByZero.linearMap is continuous for the product topologies.

source
noncomputable def Function.ExtendByZero.continuousLinearMap {ι : Type u_1} {κ : Type u_2} (R : Type u_3) (M : Type u_4) [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] (e : ι → κ) :
(ι → M) →L[R] κ → M

Extension by zero as a continuous linear map between product spaces of module-valued coordinates. No compatibility of the topology with the module operations is required.

Instances For
    source
    @[simp]
    theorem Function.ExtendByZero.continuousLinearMap_apply {ι : Type u_1} {κ : Type u_2} (R : Type u_3) (M : Type u_4) [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] (e : ι → κ) (x : ι → M) :
    (continuousLinearMap R M e) x = extend e x 0

    The continuous linear extension uses Function.extend with zero outside the image.

    source
    def Function.ExtendByZero.restriction {ι : Type u_1} {κ : Type u_2} (R : Type u_3) [Semiring R] [TopologicalSpace R] (e : ι → κ) :
    (κ → R) →L[R] ι → R

    Restrict coordinate functions along an index map, as a continuous linear map.

    Instances For
      source
      @[simp]
      theorem Function.ExtendByZero.restriction_apply {ι : Type u_1} {κ : Type u_2} (R : Type u_3) [Semiring R] [TopologicalSpace R] (e : ι → κ) (x : κ → R) :
      (restriction R e) x = x ∘ e

      Coordinate restriction is precomposition with the index map.

      source
      theorem Function.ExtendByZero.restriction_leftInverse {ι : Type u_1} {κ : Type u_2} (R : Type u_3) [Semiring R] [TopologicalSpace R] (e : ι → κ) (he : Injective e) :
      LeftInverse ⇑(restriction R e) ⇑(continuousLinearMap R R e)

      Restriction recovers every function extended along an injective index map.