Documentation

CatDG.Diffeology.Algebra.Constructions

Diffeological space structure on the opposite monoid and on the units group #

Defines the DiffeologicalSpace structure on Mᵐᵒᵖ, Mᵃᵒᵖ, Mˣ, and AddUnits M. Adapted from Mathlib.Topology.Algebra.Constructions

source
@[implicit_reducible]
instance MulOpposite.instDiffeologicalSpaceMulOpposite {M : Type u_1} [dM : DiffeologicalSpace M] :
DiffeologicalSpace Mᵐᵒᵖ

The opposite monoid is equipped with the same diffeology as the original.

Equations
source
@[implicit_reducible]
instance AddOpposite.instDiffeologicalSpaceAddOpposite {M : Type u_1} [dM : DiffeologicalSpace M] :
DiffeologicalSpace Mᵃᵒᵖ

The opposite monoid is equipped with the same diffeology as the original."

Equations
source
theorem MulOpposite.dsmooth_unop {M : Type u_1} [dM : DiffeologicalSpace M] :
DSmooth unop
source
theorem AddOpposite.dsmooth_unop {M : Type u_1} [dM : DiffeologicalSpace M] :
DSmooth unop
source
theorem MulOpposite.dsmooth_op {M : Type u_1} [dM : DiffeologicalSpace M] :
DSmooth op
source
theorem AddOpposite.dsmooth_op {M : Type u_1} [dM : DiffeologicalSpace M] :
DSmooth op
source
def MulOpposite.opDDiffeomorph {M : Type u_1} [dM : DiffeologicalSpace M] :
M ᵈ≃ Mᵐᵒᵖ

MulOpposite.op as a diffeomorphism.

Equations
Instances For
    source
    def AddOpposite.opDDiffeomorph {M : Type u_1} [dM : DiffeologicalSpace M] :
    M ᵈ≃ Mᵃᵒᵖ

    AddOpposite.op as a diffeomorphism.

    Equations
    Instances For
      source
      @[simp]
      theorem MulOpposite.opDDiffeomorph_invFun {M : Type u_1} [dM : DiffeologicalSpace M] (a✝ : Mᵐᵒᵖ) :
      opDDiffeomorph.invFun a✝ = unop a✝
      source
      @[simp]
      theorem MulOpposite.opDDiffeomorph_toFun {M : Type u_1} [dM : DiffeologicalSpace M] (a✝ : M) :
      opDDiffeomorph a✝ = op a✝
      source
      @[simp]
      theorem AddOpposite.opDDiffeomorph_toFun {M : Type u_1} [dM : DiffeologicalSpace M] (a✝ : M) :
      opDDiffeomorph a✝ = op a✝
      source
      @[simp]
      theorem AddOpposite.opDDiffeomorph_invFun {M : Type u_1} [dM : DiffeologicalSpace M] (a✝ : Mᵃᵒᵖ) :
      opDDiffeomorph.invFun a✝ = unop a✝
      source
      @[implicit_reducible]
      instance Units.instDiffeologicalSpaceUnits {M : Type u_1} [dM : DiffeologicalSpace M] [Monoid M] :
      DiffeologicalSpace Mˣ

      The units of a monoid are equipped with the diffeology induced by the embedding into M × M.

      Equations
      source
      @[implicit_reducible]
      instance AddUnits.instDiffeologicalSpaceAddUnits {M : Type u_1} [dM : DiffeologicalSpace M] [AddMonoid M] :
      DiffeologicalSpace (AddUnits M)

      The units of a monoid are equipped with the diffeology induced by the embedding into M × M.

      Equations
      source
      theorem Units.isInduction_embedProduct {M : Type u_1} [dM : DiffeologicalSpace M] [Monoid M] :
      IsInduction ⇑(embedProduct M)
      source
      theorem AddUnits.isInduction_embedProduct {M : Type u_1} [dM : DiffeologicalSpace M] [AddMonoid M] :
      IsInduction ⇑(embedProduct M)
      source
      theorem Units.diffeology_eq_inf {M : Type u_1} [dM : DiffeologicalSpace M] [Monoid M] :
      instDiffeologicalSpaceUnits = DiffeologicalSpace.induced val dM ⊓ DiffeologicalSpace.induced (fun (u : Mˣ) => ↑u⁻¹) dM
      source
      theorem AddUnits.diffeology_eq_inf {M : Type u_1} [dM : DiffeologicalSpace M] [AddMonoid M] :
      instDiffeologicalSpaceAddUnits = DiffeologicalSpace.induced val dM ⊓ DiffeologicalSpace.induced (fun (u : AddUnits M) => ↑(-u)) dM
      source
      theorem Units.dsmooth_embedProduct {M : Type u_1} [dM : DiffeologicalSpace M] [Monoid M] :
      DSmooth ⇑(embedProduct M)
      source
      theorem AddUnits.dsmooth_embedProduct {M : Type u_1} [dM : DiffeologicalSpace M] [AddMonoid M] :
      DSmooth ⇑(embedProduct M)
      source
      theorem Units.dsmooth_val {M : Type u_1} [dM : DiffeologicalSpace M] [Monoid M] :
      DSmooth val
      source
      theorem AddUnits.dsmooth_val {M : Type u_1} [dM : DiffeologicalSpace M] [AddMonoid M] :
      DSmooth val
      source
      theorem Units.dsmooth_iff {M : Type u_1} {X : Type u_2} [dM : DiffeologicalSpace M] [Monoid M] [DiffeologicalSpace X] {f : X → Mˣ} :
      DSmooth f ↔ DSmooth (val ∘ f) ∧ DSmooth fun (x : X) => ↑(f x)⁻¹
      source
      theorem AddUnits.dsmooth_iff {M : Type u_1} {X : Type u_2} [dM : DiffeologicalSpace M] [AddMonoid M] [DiffeologicalSpace X] {f : X → AddUnits M} :
      DSmooth f ↔ DSmooth (val ∘ f) ∧ DSmooth fun (x : X) => ↑(-f x)
      source
      theorem Units.dsmooth_coe_inv {M : Type u_1} [dM : DiffeologicalSpace M] [Monoid M] :
      DSmooth fun (u : Mˣ) => ↑u⁻¹
      source
      theorem AddUnits.dsmooth_coe_neg {M : Type u_1} [dM : DiffeologicalSpace M] [AddMonoid M] :
      DSmooth fun (u : AddUnits M) => ↑(-u)