Documentation

Mathlib.Topology.Algebra.SeparationQuotient

Algebraic operations on SeparationQuotient #

In this file we define algebraic operations (multiplication, addition etc) on the separation quotient of a topological space with corresponding operation, provided that the original operation is continuous.

We also prove continuity of these operations and show that they satisfy the same kind of laws (Monoid etc) as the original ones.

Finally, we construct a section of the quotient map which is a continuous linear map SeparationQuotient E →L[K] E.

Equations
  • SeparationQuotient.instVAdd = { vadd := fun (c : M) => Quotient.map' (fun (x : X) => c +ᵥ x) }
Equations
  • SeparationQuotient.instSMul = { smul := fun (c : M) => Quotient.map' (fun (x : X) => c x) }
@[simp]
@[simp]
Equations
  • =
Equations
  • =
Equations
  • =
Equations
  • =
Equations
  • SeparationQuotient.instSMulZeroClass = { toFun := SeparationQuotient.mk, map_zero' := }.smulZeroClass
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations

SeparationQuotient.mk as an AddMonoidHom.

Equations
  • SeparationQuotient.mkAddMonoidHom = { toFun := SeparationQuotient.mk, map_zero' := , map_add' := }
Instances For
    @[simp]
    theorem SeparationQuotient.mkAddMonoidHom_apply {M : Type u_1} [TopologicalSpace M] [AddZeroClass M] [ContinuousAdd M] :
    ∀ (a : M), SeparationQuotient.mkAddMonoidHom a = SeparationQuotient.mk a
    @[simp]
    theorem SeparationQuotient.mkMonoidHom_apply {M : Type u_1} [TopologicalSpace M] [MulOneClass M] [ContinuousMul M] :
    ∀ (a : M), SeparationQuotient.mkMonoidHom a = SeparationQuotient.mk a

    SeparationQuotient.mk as a MonoidHom.

    Equations
    • SeparationQuotient.mkMonoidHom = { toFun := SeparationQuotient.mk, map_one' := , map_mul' := }
    Instances For
      Equations
      • SeparationQuotient.instNSmul = inferInstance
      Equations
      Equations
      Equations
      Equations
      Equations
      Equations
      • SeparationQuotient.instNeg = { neg := Quotient.map' (fun (x : G) => -x) }
      Equations
      Equations
      Equations
      Equations
      Equations
      Equations
      theorem SeparationQuotient.instSub.proof_1 {G : Type u_1} [TopologicalSpace G] [Sub G] [ContinuousSub G] :
      ∀ (x x_1 : G), (inseparableSetoid G) x x_1∀ (x_2 x_3 : G), (inseparableSetoid G) x_2 x_3Inseparable ((x, x_2).1 - (x, x_2).2) ((x_1, x_3).1 - (x_1, x_3).2)
      Equations
      Equations
      • SeparationQuotient.instZSMul = inferInstance
      Equations
      Equations
      Equations
      Equations
      Equations
      Equations
      Equations
      Equations
      Equations
      Equations
      Equations
      Equations
      Equations
      Equations
      Equations
      Equations
      Equations
      Equations
      Equations
      Equations
      Equations
      Equations
      Equations
      Equations
      Equations
      Equations
      Equations
      @[simp]
      theorem SeparationQuotient.mkRingHom_apply {R : Type u_1} [TopologicalSpace R] [NonAssocSemiring R] [TopologicalSemiring R] :
      ∀ (a : R), SeparationQuotient.mkRingHom a = SeparationQuotient.mk a

      SeparationQuotient.mk as a RingHom.

      Equations
      • SeparationQuotient.mkRingHom = { toFun := SeparationQuotient.mk, map_one' := , map_mul' := , map_zero' := , map_add' := }
      Instances For
        Equations
        Equations
        Equations
        Equations

        SeparationQuotient.mk as a continuous linear map.

        Equations
        Instances For
          Equations

          There exists a continuous K-linear map from SeparationQuotient E to E such that mk (outCLM x) = x for all x.

          Note that continuity of this map comes for free, because mk is a topology inducing map.

          A continuous K-linear map from SeparationQuotient E to E such that mk (outCLM x) = x for all x.

          Equations
          Instances For
            @[simp]
            @[deprecated SeparationQuotient.outCLM_isUniformInducing]

            Alias of SeparationQuotient.outCLM_isUniformInducing.