Diffeological groups #
Adapted from Mathlib.Topology.Algebra.Group.Basic.
Equations
- DDiffeomorph.mulLeft a = { toEquiv := Equiv.mulLeft a, dsmooth_toFun := ⋯, dsmooth_invFun := ⋯ }
Instances For
def
DDiffeomorph.addLeft
{G : Type u_1}
[DiffeologicalSpace G]
[AddGroup G]
[DSmoothAdd G]
(a : G)
:
Equations
- DDiffeomorph.addLeft a = { toEquiv := Equiv.addLeft a, dsmooth_toFun := ⋯, dsmooth_invFun := ⋯ }
Instances For
@[simp]
theorem
DDiffeomorph.coe_mulLeft
{G : Type u_1}
[DiffeologicalSpace G]
[Group G]
[DSmoothMul G]
(a : G)
:
@[simp]
theorem
DDiffeomorph.coe_addLeft
{G : Type u_1}
[DiffeologicalSpace G]
[AddGroup G]
[DSmoothAdd G]
(a : G)
:
theorem
DDiffeomorph.mulLeft_symm
{G : Type u_1}
[DiffeologicalSpace G]
[Group G]
[DSmoothMul G]
(a : G)
:
theorem
DDiffeomorph.addLeft_symm
{G : Type u_1}
[DiffeologicalSpace G]
[AddGroup G]
[DSmoothAdd G]
(a : G)
:
Equations
- DDiffeomorph.mulRight a = { toEquiv := Equiv.mulRight a, dsmooth_toFun := ⋯, dsmooth_invFun := ⋯ }
Instances For
def
DDiffeomorph.addRight
{G : Type u_1}
[DiffeologicalSpace G]
[AddGroup G]
[DSmoothAdd G]
(a : G)
:
Equations
- DDiffeomorph.addRight a = { toEquiv := Equiv.addRight a, dsmooth_toFun := ⋯, dsmooth_invFun := ⋯ }
Instances For
@[simp]
theorem
DDiffeomorph.coe_mulRight
{G : Type u_1}
[DiffeologicalSpace G]
[Group G]
[DSmoothMul G]
(a : G)
:
@[simp]
theorem
DDiffeomorph.coe_addRight
{G : Type u_1}
[DiffeologicalSpace G]
[AddGroup G]
[DSmoothAdd G]
(a : G)
:
theorem
DDiffeomorph.mulRight_symm
{G : Type u_1}
[DiffeologicalSpace G]
[Group G]
[DSmoothMul G]
(a : G)
:
theorem
DDiffeomorph.addRight_symm
{G : Type u_1}
[DiffeologicalSpace G]
[AddGroup G]
[DSmoothAdd G]
(a : G)
:
DSmoothInv and DSmoothNeg #
Class saying that negation in a type is smooth. A diffeological additive group is then
a type with the instances AddGroup G, DSmoothAdd G and DSmoothNeg G.
Instances
Class saying that inversion in a type is smooth. A diffeological group is then
a type with the instances Group G, DSmoothMul G and DSmoothInv G.
Instances
theorem
DSmooth.inv
{G : Type u_1}
[DiffeologicalSpace G]
[Inv G]
[DSmoothInv G]
{X : Type u_2}
[DiffeologicalSpace X]
{f : X → G}
(hf : DSmooth f)
:
theorem
DSmooth.neg
{G : Type u_1}
[DiffeologicalSpace G]
[Neg G]
[DSmoothNeg G]
{X : Type u_2}
[DiffeologicalSpace X]
{f : X → G}
(hf : DSmooth f)
:
instance
Prod.dsmoothInv
{G : Type u_1}
[DiffeologicalSpace G]
[Inv G]
[DSmoothInv G]
{H : Type u_2}
[DiffeologicalSpace H]
[Inv H]
[DSmoothInv H]
:
DSmoothInv (G × H)
instance
Prod.dsmoothNeg
{G : Type u_1}
[DiffeologicalSpace G]
[Neg G]
[DSmoothNeg G]
{H : Type u_2}
[DiffeologicalSpace H]
[Neg H]
[DSmoothNeg H]
:
DSmoothNeg (G × H)
instance
Pi.dsmoothInv
{ι : Type u_2}
{G : ι → Type u_3}
[(i : ι) → DiffeologicalSpace (G i)]
[(i : ι) → Inv (G i)]
[∀ (i : ι), DSmoothInv (G i)]
:
DSmoothInv ((i : ι) → G i)
instance
Pi.dsmoothNeg
{ι : Type u_2}
{G : ι → Type u_3}
[(i : ι) → DiffeologicalSpace (G i)]
[(i : ι) → Neg (G i)]
[∀ (i : ι), DSmoothNeg (G i)]
:
DSmoothNeg ((i : ι) → G i)
instance
instDSmoothNegAdditiveOfDSmoothInv
{H : Type u_2}
[DiffeologicalSpace H]
[Inv H]
[DSmoothInv H]
:
DSmoothNeg (Additive H)
instance
instDSmoothInvMultiplicativeOfDSmoothNeg
{H : Type u_2}
[DiffeologicalSpace H]
[Neg H]
[DSmoothNeg H]
:
Inversion in a diffeological group as a diffeomorphism.
Equations
- Diffeomorph.inv G = { toEquiv := Equiv.inv G, dsmooth_toFun := ⋯, dsmooth_invFun := ⋯ }
Instances For
Negation in a diffeological group as a diffeomorphism.
Equations
- Diffeomorph.neg G = { toEquiv := Equiv.neg G, dsmooth_toFun := ⋯, dsmooth_invFun := ⋯ }
Instances For
@[simp]
theorem
Diffeomorph.coe_inv
{G : Type u_1}
[DiffeologicalSpace G]
[InvolutiveInv G]
[DSmoothInv G]
:
@[simp]
theorem
Diffeomorph.coe_neg
{G : Type u_1}
[DiffeologicalSpace G]
[InvolutiveNeg G]
[DSmoothNeg G]
:
theorem
dsmoothInv_sInf
{G : Type u_1}
[Inv G]
{D : Set (DiffeologicalSpace G)}
(h : ∀ d ∈ D, DSmoothInv G)
:
theorem
dsmoothNeg_sInf
{G : Type u_1}
[Neg G]
{D : Set (DiffeologicalSpace G)}
(h : ∀ d ∈ D, DSmoothNeg G)
:
theorem
dsmoothInv_iInf
{G : Type u_1}
{ι : Type u_2}
[Inv G]
{D : ι → DiffeologicalSpace G}
(h' : ∀ (i : ι), DSmoothInv G)
:
theorem
dsmoothNeg_iInf
{G : Type u_1}
{ι : Type u_2}
[Neg G]
{D : ι → DiffeologicalSpace G}
(h' : ∀ (i : ι), DSmoothNeg G)
:
theorem
dsmoothInv_inf
{G : Type u_1}
[Inv G]
{d₁ d₂ : DiffeologicalSpace G}
(h₁ : DSmoothInv G)
(h₂ : DSmoothInv G)
:
theorem
dsmoothNeg_inf
{G : Type u_1}
[Neg G]
{d₁ d₂ : DiffeologicalSpace G}
(h₁ : DSmoothNeg G)
(h₂ : DSmoothNeg G)
:
theorem
IsDInducing.dsmoothInv
{G : Type u_1}
{H : Type u_2}
[Inv G]
[Inv H]
[DiffeologicalSpace G]
[DiffeologicalSpace H]
[DSmoothInv H]
{f : G → H}
(hf : IsDInducing f)
(hf_inv : ∀ (x : G), f x⁻¹ = (f x)⁻¹)
:
theorem
IsDInducing.dsmoothNeg
{G : Type u_1}
{H : Type u_2}
[Neg G]
[Neg H]
[DiffeologicalSpace G]
[DiffeologicalSpace H]
[DSmoothNeg H]
{f : G → H}
(hf : IsDInducing f)
(hf_inv : ∀ (x : G), f (-x) = -f x)
:
theorem
dsmoothInv_induced
{G : Type u_1}
{H : Type u_2}
[Inv G]
[Inv H]
[DiffeologicalSpace H]
[DSmoothInv H]
(f : G → H)
(hf_inv : ∀ (x : G), f x⁻¹ = (f x)⁻¹)
:
theorem
dsmoothNeg_induced
{G : Type u_1}
{H : Type u_2}
[Neg G]
[Neg H]
[DiffeologicalSpace H]
[DSmoothNeg H]
(f : G → H)
(hf_inv : ∀ (x : G), f (-x) = -f x)
:
Diffeological groups #
A diffeological group is a group which is also a diffeological space in such a way that the multiplication and inversion operations are smooth.
class
DiffeologicalAddGroup
(G : Type u_1)
[DiffeologicalSpace G]
[AddGroup G]
extends DSmoothAdd G, DSmoothNeg G :
A diffeological (additive) group is a group in which the addition and negation operations are dsmooth.
- dsmooth_add : DSmooth fun (p : G × G) => p.1 + p.2
- dsmooth_neg : DSmooth fun (a : G) => -a
Instances
class
DiffeologicalGroup
(G : Type u_1)
[DiffeologicalSpace G]
[Group G]
extends DSmoothMul G, DSmoothInv G :
A diffeological group is a group in which the multiplication and inversion operations are smooth.
- dsmooth_mul : DSmooth fun (p : G × G) => p.1 * p.2
- dsmooth_inv : DSmooth fun (a : G) => a⁻¹
Instances
theorem
DiffeologicalGroup.dsmooth_conj_prod
{G : Type u_1}
[DiffeologicalSpace G]
[Inv G]
[Mul G]
[DSmoothMul G]
[DSmoothInv G]
:
Conjugation is jointly smooth on G × G when both mul and inv are smooth.
theorem
DiffeologicalAddGroup.dsmooth_conj_sum
{G : Type u_1}
[DiffeologicalSpace G]
[Neg G]
[Add G]
[DSmoothAdd G]
[DSmoothNeg G]
:
Conjugation is jointly smooth on G × G when both add and neg are smooth.
theorem
DiffeologicalGroup.dsmooth_conj
{G : Type u_1}
[DiffeologicalSpace G]
[Inv G]
[Mul G]
[DSmoothMul G]
(g : G)
:
Conjugation by a fixed element is smooth when mul is smooth.
theorem
DiffeologicalAddGroup.dsmooth_conj
{G : Type u_1}
[DiffeologicalSpace G]
[Neg G]
[Add G]
[DSmoothAdd G]
(g : G)
:
Conjugation by a fixed element is smooth when add is smooth.
theorem
DiffeologicalGroup.dsmooth_conj'
{G : Type u_1}
[DiffeologicalSpace G]
[Inv G]
[Mul G]
[DSmoothMul G]
[DSmoothInv G]
(h : G)
:
Conjugation acting on fixed element of the group is smooth when both mul and
inv are smooth.
theorem
DiffeologicalAddGroup.dsmooth_conj'
{G : Type u_1}
[DiffeologicalSpace G]
[Neg G]
[Add G]
[DSmoothAdd G]
[DSmoothNeg G]
(h : G)
:
Conjugation acting on fixed element of the additive group is smooth when both
add and neg are smooth.
instance
instDiffeologicalGroupULift
{G : Type u_1}
[DiffeologicalSpace G]
[Group G]
[DiffeologicalGroup G]
:
theorem
dsmooth_zpow
{G : Type u_1}
[DiffeologicalSpace G]
[Group G]
[DiffeologicalGroup G]
(z : ℤ)
:
theorem
dsmooth_zsmul
{G : Type u_1}
[DiffeologicalSpace G]
[AddGroup G]
[DiffeologicalAddGroup G]
(z : ℤ)
:
theorem
DSmooth.zpow
{G : Type u_1}
[DiffeologicalSpace G]
[Group G]
[DiffeologicalGroup G]
{X : Type u_2}
[DiffeologicalSpace X]
{f : X → G}
(h : DSmooth f)
(z : ℤ)
:
theorem
DSmooth.zsmul
{G : Type u_1}
[DiffeologicalSpace G]
[AddGroup G]
[DiffeologicalAddGroup G]
{X : Type u_2}
[DiffeologicalSpace X]
{f : X → G}
(h : DSmooth f)
(z : ℤ)
:
instance
instDiffeologicalGroupProd
{G : Type u_1}
[DiffeologicalSpace G]
[Group G]
[DiffeologicalGroup G]
{H : Type u_3}
[DiffeologicalSpace H]
[Group H]
[DiffeologicalGroup H]
:
DiffeologicalGroup (G × H)
instance
instDiffeologicalAddGroupSum
{G : Type u_1}
[DiffeologicalSpace G]
[AddGroup G]
[DiffeologicalAddGroup G]
{H : Type u_3}
[DiffeologicalSpace H]
[AddGroup H]
[DiffeologicalAddGroup H]
:
DiffeologicalAddGroup (G × H)
instance
Pi.diffeologicalGroup
{ι : Type u_3}
{G : ι → Type u_4}
[(i : ι) → DiffeologicalSpace (G i)]
[(i : ι) → Group (G i)]
[∀ (i : ι), DiffeologicalGroup (G i)]
:
DiffeologicalGroup ((i : ι) → G i)
instance
Pi.diffeologicalAddGroup
{ι : Type u_3}
{G : ι → Type u_4}
[(i : ι) → DiffeologicalSpace (G i)]
[(i : ι) → AddGroup (G i)]
[∀ (i : ι), DiffeologicalAddGroup (G i)]
:
DiffeologicalAddGroup ((i : ι) → G i)
instance
instDiffeologicalGroupMulOpposite
{G : Type u_3}
[DiffeologicalSpace G]
[Group G]
[DiffeologicalGroup G]
:
If multiplication is continuous in α, then it also is in αᵐᵒᵖ.
instance
instDiffeologicalAddGroupAddOpposite
{G : Type u_3}
[DiffeologicalSpace G]
[AddGroup G]
[DiffeologicalAddGroup G]
:
If addition is continuous in α, then it also is in αᵃᵒᵖ.
def
DDiffeomorph.shearMulRight
(G : Type u_1)
[DiffeologicalSpace G]
[Group G]
[DiffeologicalGroup G]
:
The map (x, y) ↦ (x, x * y) as a diffeomorphism. This is a shear mapping.
Equations
- DDiffeomorph.shearMulRight G = { toEquiv := (Equiv.refl G).prodShear Equiv.mulLeft, dsmooth_toFun := ⋯, dsmooth_invFun := ⋯ }
Instances For
def
DDiffeomorph.shearAddRight
(G : Type u_1)
[DiffeologicalSpace G]
[AddGroup G]
[DiffeologicalAddGroup G]
:
The map (x, y) ↦ (x, x + y) as a homeomorphism. This is a shear mapping.
Equations
- DDiffeomorph.shearAddRight G = { toEquiv := (Equiv.refl G).prodShear Equiv.addLeft, dsmooth_toFun := ⋯, dsmooth_invFun := ⋯ }
Instances For
@[simp]
theorem
DDiffeomorph.shearMulRight_coe
(G : Type u_1)
[DiffeologicalSpace G]
[Group G]
[DiffeologicalGroup G]
:
@[simp]
theorem
DDiffeomorph.shearAddRight_coe
(G : Type u_1)
[DiffeologicalSpace G]
[AddGroup G]
[DiffeologicalAddGroup G]
:
@[simp]
theorem
DDiffeomorph.shearMulRight_symm_coe
(G : Type u_1)
[DiffeologicalSpace G]
[Group G]
[DiffeologicalGroup G]
:
@[simp]
theorem
DDiffeomorph.shearAddRight_symm_coe
(G : Type u_1)
[DiffeologicalSpace G]
[AddGroup G]
[DiffeologicalAddGroup G]
:
theorem
IsDInducing.diffeologicalGroup
{G : Type u_1}
[DiffeologicalSpace G]
[Group G]
[DiffeologicalGroup G]
{H : Type u_2}
{F : Type u_3}
[Group H]
[DiffeologicalSpace H]
[FunLike F H G]
[MonoidHomClass F H G]
(f : F)
(hf : IsDInducing ⇑f)
:
For any group homomorphism to a diffeological group, the induced diffeology makes the domain a diffeological group too.
theorem
IsDInducing.diffeologicalAddGroup
{G : Type u_1}
[DiffeologicalSpace G]
[AddGroup G]
[DiffeologicalAddGroup G]
{H : Type u_2}
{F : Type u_3}
[AddGroup H]
[DiffeologicalSpace H]
[FunLike F H G]
[AddMonoidHomClass F H G]
(f : F)
(hf : IsDInducing ⇑f)
:
For any group homomorphism to a diffeological group, the induced diffeology makes the domain a diffeological group too.
theorem
diffeologicalGroup_induced
{G : Type u_1}
[DiffeologicalSpace G]
[Group G]
[DiffeologicalGroup G]
{H : Type u_2}
{F : Type u_3}
[Group H]
[FunLike F H G]
[MonoidHomClass F H G]
(f : F)
:
theorem
diffeologicalAddGroup_induced
{G : Type u_1}
[DiffeologicalSpace G]
[AddGroup G]
[DiffeologicalAddGroup G]
{H : Type u_2}
{F : Type u_3}
[AddGroup H]
[FunLike F H G]
[AddMonoidHomClass F H G]
(f : F)
:
instance
Subgroup.instDiffeologicalGroupSubtypeMem
{G : Type u_1}
[DiffeologicalSpace G]
[Group G]
[DiffeologicalGroup G]
(S : Subgroup G)
:
instance
AddSubgroup.instDiffeologicalAddGroupSubtypeMem
{G : Type u_1}
[DiffeologicalSpace G]
[AddGroup G]
[DiffeologicalAddGroup G]
(S : AddSubgroup G)
:
instance
QuotientGroup.Quotient.diffeologicalSpace
{G : Type u_1}
[Group G]
[DiffeologicalSpace G]
(N : Subgroup G)
:
DiffeologicalSpace (G ⧸ N)
instance
QuotientAddGroup.Quotient.diffeologicalSpace
{G : Type u_1}
[AddGroup G]
[DiffeologicalSpace G]
(N : AddSubgroup G)
:
DiffeologicalSpace (G ⧸ N)
theorem
QuotientGroup.isSubduction_coe
{G : Type u_1}
[DiffeologicalSpace G]
[Group G]
(N : Subgroup G)
:
theorem
QuotientAddGroup.isSubduction_coe
{G : Type u_1}
[DiffeologicalSpace G]
[AddGroup G]
(N : AddSubgroup G)
:
instance
diffeologicalGroup_quotient
{G : Type u_1}
[DiffeologicalSpace G]
[Group G]
[DiffeologicalGroup G]
(N : Subgroup G)
[N.Normal]
:
DiffeologicalGroup (G ⧸ N)
instance
diffeologicalAddGroup_quotient
{G : Type u_1}
[DiffeologicalSpace G]
[AddGroup G]
[DiffeologicalAddGroup G]
(N : AddSubgroup G)
[N.Normal]
:
DiffeologicalAddGroup (G ⧸ N)
A typeclass saying that p : G × G ↦ p.1 - p.2 is a smooth function. This property
automatically holds for diffeological additive groups but it also holds, e.g., for ℝ≥0.
Instances
A typeclass saying that p : G × G ↦ p.1 / p.2 is a smooth function. This property
automatically holds for diffeological groups. Lemmas using this class have primes.
The unprimed version is for GroupWithZero.
Instances
@[instance 100]
instance
DiffeologicalGroup.to_dsmoothDiv
{G : Type u_1}
[DiffeologicalSpace G]
[Group G]
[DiffeologicalGroup G]
:
@[instance 100]
instance
DiffeologicalAddGroup.to_dsmoothSub
{G : Type u_1}
[DiffeologicalSpace G]
[AddGroup G]
[DiffeologicalAddGroup G]
:
theorem
DSmooth.div'
{G : Type u_1}
[DiffeologicalSpace G]
[Div G]
[DSmoothDiv G]
{X : Type u_2}
[DiffeologicalSpace X]
{f g : X → G}
(hf : DSmooth f)
(hg : DSmooth g)
:
theorem
DSmooth.sub
{G : Type u_1}
[DiffeologicalSpace G]
[Sub G]
[DSmoothSub G]
{X : Type u_2}
[DiffeologicalSpace X]
{f g : X → G}
(hf : DSmooth f)
(hg : DSmooth g)
:
def
DDiffeomorph.divLeft
{G : Type u_1}
[DiffeologicalSpace G]
[Group G]
[DiffeologicalGroup G]
(g : G)
:
A version of DDiffeomorph.mulLeft a b⁻¹ that is defeq to a / b.
Equations
- DDiffeomorph.divLeft g = { toEquiv := Equiv.divLeft g, dsmooth_toFun := ⋯, dsmooth_invFun := ⋯ }
Instances For
def
DDiffeomorph.subLeft
{G : Type u_1}
[DiffeologicalSpace G]
[AddGroup G]
[DiffeologicalAddGroup G]
(g : G)
:
A version of DDiffeomorph.addLeft a (-b) that is defeq to a - b.
Equations
- DDiffeomorph.subLeft g = { toEquiv := Equiv.subLeft g, dsmooth_toFun := ⋯, dsmooth_invFun := ⋯ }
Instances For
@[simp]
theorem
DDiffeomorph.divLeft_toFun
{G : Type u_1}
[DiffeologicalSpace G]
[Group G]
[DiffeologicalGroup G]
(g b : G)
:
@[simp]
theorem
DDiffeomorph.subLeft_toFun
{G : Type u_1}
[DiffeologicalSpace G]
[AddGroup G]
[DiffeologicalAddGroup G]
(g b : G)
:
@[simp]
theorem
DDiffeomorph.subLeft_invFun
{G : Type u_1}
[DiffeologicalSpace G]
[AddGroup G]
[DiffeologicalAddGroup G]
(g b : G)
:
@[simp]
theorem
DDiffeomorph.divLeft_invFun
{G : Type u_1}
[DiffeologicalSpace G]
[Group G]
[DiffeologicalGroup G]
(g b : G)
:
def
DDiffeomorph.divRight
{G : Type u_1}
[DiffeologicalSpace G]
[Group G]
[DiffeologicalGroup G]
(g : G)
:
A version of DDiffeomorph.mulRight a⁻¹ b that is defeq to b / a.
Equations
- DDiffeomorph.divRight g = { toEquiv := Equiv.divRight g, dsmooth_toFun := ⋯, dsmooth_invFun := ⋯ }
Instances For
def
DDiffeomorph.subRight
{G : Type u_1}
[DiffeologicalSpace G]
[AddGroup G]
[DiffeologicalAddGroup G]
(g : G)
:
A version of DDiffeomorph.addRight (-a) b that is defeq to b - a.
Equations
- DDiffeomorph.subRight g = { toEquiv := Equiv.subRight g, dsmooth_toFun := ⋯, dsmooth_invFun := ⋯ }
Instances For
@[simp]
theorem
DDiffeomorph.subRight_invFun
{G : Type u_1}
[DiffeologicalSpace G]
[AddGroup G]
[DiffeologicalAddGroup G]
(g b : G)
:
@[simp]
theorem
DDiffeomorph.divRight_toFun
{G : Type u_1}
[DiffeologicalSpace G]
[Group G]
[DiffeologicalGroup G]
(g b : G)
:
@[simp]
theorem
DDiffeomorph.subRight_toFun
{G : Type u_1}
[DiffeologicalSpace G]
[AddGroup G]
[DiffeologicalAddGroup G]
(g b : G)
:
@[simp]
theorem
DDiffeomorph.divRight_invFun
{G : Type u_1}
[DiffeologicalSpace G]
[Group G]
[DiffeologicalGroup G]
(g b : G)
:
instance
instDiffeologicalAddGroupAdditiveOfDiffeologicalGroup
{G : Type u_1}
[DiffeologicalSpace G]
[Group G]
[DiffeologicalGroup G]
:
instance
instDiffeologicalGroupMultiplicativeOfDiffeologicalAddGroup
{G : Type u_1}
[DiffeologicalSpace G]
[AddGroup G]
[DiffeologicalAddGroup G]
:
A group with smooth inversion is diffeomorphic to its units.
Equations
- toUnits_ddiffeomorph = { toEquiv := toUnits.toEquiv, dsmooth_toFun := ⋯, dsmooth_invFun := ⋯ }
Instances For
An additive group with smooth negation is homeomorphic to its additive units.
Equations
- toAddUnits_ddiffeomorph = { toEquiv := toAddUnits.toEquiv, dsmooth_toFun := ⋯, dsmooth_invFun := ⋯ }
Instances For
instance
Units.instDiffeologicalGroupOfDSmoothMul
{M : Type u_1}
[Monoid M]
[DiffeologicalSpace M]
[DSmoothMul M]
:
instance
AddUnits.instDiffeologicalAddGroupOfDSmoothAdd
{M : Type u_1}
[AddMonoid M]
[DiffeologicalSpace M]
[DSmoothAdd M]
:
def
Units.DDiffeomorph.prodUnits
{M : Type u_1}
{N : Type u_2}
[Monoid M]
[DiffeologicalSpace M]
[Monoid N]
[DiffeologicalSpace N]
:
The diffeological group isomorphism between the units of a product of two monoids, and the product of the units of each monoid.
Equations
- Units.DDiffeomorph.prodUnits = { toEquiv := MulEquiv.prodUnits.toEquiv, dsmooth_toFun := ⋯, dsmooth_invFun := ⋯ }
Instances For
def
AddUnits.DDiffeomorph.sumAddUnits
{M : Type u_1}
{N : Type u_2}
[AddMonoid M]
[DiffeologicalSpace M]
[AddMonoid N]
[DiffeologicalSpace N]
:
The diffeological group isomorphism between the additive units of a product of two additive monoids, and the product of the additive units of each additive monoid.
Equations
- AddUnits.DDiffeomorph.sumAddUnits = { toEquiv := AddEquiv.prodAddUnits.toEquiv, dsmooth_toFun := ⋯, dsmooth_invFun := ⋯ }
Instances For
theorem
diffeologicalGroup_sInf
{G : Type u_1}
[Group G]
{D : Set (DiffeologicalSpace G)}
(h : ∀ d ∈ D, DiffeologicalGroup G)
:
theorem
diffeologicalAddGroup_sInf
{G : Type u_1}
[AddGroup G]
{D : Set (DiffeologicalSpace G)}
(h : ∀ d ∈ D, DiffeologicalAddGroup G)
:
theorem
diffeologicalGroup_iInf
{G : Type u_1}
{ι : Type u_2}
[Group G]
{D : ι → DiffeologicalSpace G}
(h' : ∀ (i : ι), DiffeologicalGroup G)
:
theorem
diffeologicalAddGroup_iInf
{G : Type u_1}
{ι : Type u_2}
[AddGroup G]
{D : ι → DiffeologicalSpace G}
(h' : ∀ (i : ι), DiffeologicalAddGroup G)
:
theorem
diffeologicalGroup_inf
{G : Type u_1}
[Group G]
{d₁ d₂ : DiffeologicalSpace G}
(h₁ : DiffeologicalGroup G)
(h₂ : DiffeologicalGroup G)
:
theorem
diffeologicalAddGroup_inf
{G : Type u_1}
[AddGroup G]
{d₁ d₂ : DiffeologicalSpace G}
(h₁ : DiffeologicalAddGroup G)
(h₂ : DiffeologicalAddGroup G)
:
Lattice of group diffeologies #
We define a type class GroupDiffeology G which endows a group G with a diffeology such
that all group operations are smooth.
Group diffeologies on a fixed group G are ordered by inclusion. They form a complete
lattice, with ⊥ the discrete diffeology and ⊤ the indiscrete diffeology.
Any function f : G → H induces coinduced f : DiffeologicalSpace G → GroupDiffeology H.
An additive version AddGroupDiffeology G is defined as well.
structure
AddGroupDiffeology
(G : Type u)
[AddGroup G]
extends DiffeologicalSpace G, DiffeologicalAddGroup G :
Type u
An additive group diffeology on a group G is a diffeology that makes G into an
additive diffeological group.
- isOpen_iff_preimages_plots {u : Set G} : TopologicalSpace.IsOpen u ↔ ∀ {n : ℕ}, ∀ p ∈ plots n, TopologicalSpace.IsOpen (p ⁻¹' u)
- dsmooth_add : DSmooth fun (p : G × G) => p.1 + p.2
- dsmooth_neg : DSmooth fun (a : G) => -a
Instances For
structure
GroupDiffeology
(G : Type u)
[Group G]
extends DiffeologicalSpace G, DiffeologicalGroup G :
Type u
A group diffeology on a group G is a diffeology that makes G into a
diffeological group.
- isOpen_iff_preimages_plots {u : Set G} : TopologicalSpace.IsOpen u ↔ ∀ {n : ℕ}, ∀ p ∈ plots n, TopologicalSpace.IsOpen (p ⁻¹' u)
- dsmooth_mul : DSmooth fun (p : G × G) => p.1 * p.2
- dsmooth_inv : DSmooth fun (a : G) => a⁻¹
Instances For
A version of the global dsmooth_mul suitable for dot notation.
A version of the global dsmooth_add suitable for dot notation.
A version of the global dsmooth_inv suitable for dot notation.
A version of the global dsmooth_neg suitable for dot notation.
theorem
GroupDiffeology.ext'
{G : Type u_1}
[Group G]
{d₁ d₂ : GroupDiffeology G}
(h : d₁.toDiffeologicalSpace = d₂.toDiffeologicalSpace)
:
theorem
AddGroupDiffeology.ext'
{G : Type u_1}
[AddGroup G]
{d₁ d₂ : AddGroupDiffeology G}
(h : d₁.toDiffeologicalSpace = d₂.toDiffeologicalSpace)
:
@[simp]
theorem
GroupDiffeology.toDiffeologicalSpace_le
{G : Type u_1}
[Group G]
{d₁ d₂ : GroupDiffeology G}
:
@[simp]
theorem
AddGroupDiffeology.toDiffeologicalSpace_le
{G : Type u_1}
[AddGroup G]
{d₁ d₂ : AddGroupDiffeology G}
:
Equations
- GroupDiffeology.instTop = { top := { toDiffeologicalSpace := ⊤, toDiffeologicalGroup := ⋯ } }
Equations
- AddGroupDiffeology.instTop = { top := { toDiffeologicalSpace := ⊤, toDiffeologicalAddGroup := ⋯ } }
@[simp]
@[simp]
Equations
- GroupDiffeology.instBot = { bot := { toDiffeologicalSpace := ⊥, toDiffeologicalGroup := ⋯ } }
Equations
- AddGroupDiffeology.instBot = { bot := { toDiffeologicalSpace := ⊥, toDiffeologicalAddGroup := ⋯ } }
@[simp]
@[simp]
Equations
- GroupDiffeology.instBoundedOrder = { toTop := GroupDiffeology.instTop, le_top := ⋯, toBot := GroupDiffeology.instBot, bot_le := ⋯ }
Equations
- AddGroupDiffeology.instBoundedOrder = { toTop := AddGroupDiffeology.instTop, le_top := ⋯, toBot := AddGroupDiffeology.instBot, bot_le := ⋯ }
Equations
- GroupDiffeology.instMin = { min := fun (d₁ d₂ : GroupDiffeology G) => { toDiffeologicalSpace := d₁.toDiffeologicalSpace ⊓ d₂.toDiffeologicalSpace, toDiffeologicalGroup := ⋯ } }
Equations
- AddGroupDiffeology.instMin = { min := fun (d₁ d₂ : AddGroupDiffeology G) => { toDiffeologicalSpace := d₁.toDiffeologicalSpace ⊓ d₂.toDiffeologicalSpace, toDiffeologicalAddGroup := ⋯ } }
@[simp]
theorem
GroupDiffeology.toDiffeologicalSpace_inf
{G : Type u_1}
[Group G]
(x y : GroupDiffeology G)
:
@[simp]
theorem
AddGroupDiffeology.toDiffeologicalSpace_inf
{G : Type u_1}
[AddGroup G]
(x y : AddGroupDiffeology G)
:
Equations
- GroupDiffeology.instInhabited = { default := ⊤ }
Equations
- AddGroupDiffeology.instInhabited = { default := ⊤ }
Infimum of a collection of group diffeologies.
Equations
- GroupDiffeology.instInfSet = { sInf := fun (D : Set (GroupDiffeology G)) => { toDiffeologicalSpace := sInf (GroupDiffeology.toDiffeologicalSpace '' D), toDiffeologicalGroup := ⋯ } }
Infimum of a collection of additive group diffeologies
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
GroupDiffeology.toDiffeologicalSpace_sInf
{G : Type u_1}
[Group G]
(s : Set (GroupDiffeology G))
:
@[simp]
theorem
AddGroupDiffeology.toDiffeologicalSpace_sInf
{G : Type u_1}
[AddGroup G]
(s : Set (AddGroupDiffeology G))
:
@[simp]
theorem
GroupDiffeology.toDiffeologicalSpace_iInf
{G : Type u_1}
[Group G]
{ι : Type u_2}
(s : ι → GroupDiffeology G)
:
@[simp]
theorem
AddGroupDiffeology.toDiffeologicalSpace_iInf
{G : Type u_1}
[AddGroup G]
{ι : Type u_2}
(s : ι → AddGroupDiffeology G)
:
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
instance
instContinuousInvOfDTopCompatibleOfDSmoothInv
{G : Type u_1}
[DiffeologicalSpace G]
[TopologicalSpace G]
[DTopCompatible G]
[Inv G]
[DSmoothInv G]
:
instance
instContinuousNegOfDTopCompatibleOfDSmoothNeg
{G : Type u_1}
[DiffeologicalSpace G]
[TopologicalSpace G]
[DTopCompatible G]
[Neg G]
[DSmoothNeg G]
:
theorem
DiffeologicalGroup.topologicalGroup
{G : Type u_1}
[DiffeologicalSpace G]
[Group G]
[DiffeologicalGroup G]
[LocallyCompactSpace G]
:
If a diffeological group G is locally compact under the D-topology, then it is also a
topological group. Local compactness is needed here because multiplication is a priori only
continuous with respect to the D-topology on G × G, not the product topology - when G is
locally compact the topologies agree, but otherwise the product topology could be
fine enough for multiplication to not be continuous.
theorem
DiffeologicalAddGroup.topologicalAddGroup
{G : Type u_1}
[DiffeologicalSpace G]
[AddGroup G]
[DiffeologicalAddGroup G]
[LocallyCompactSpace G]
:
If a diffeological group G is locally compact under the D-topology, then it is
also a topological group. Local compactness is needed here because addition is a priori only
continuous with respect to the D-topology on G × G, not the product topology - when G is
locally compact the topologies agree, but otherwise the product topology could be
fine enough for addition to not be continuous.
instance
instIsTopologicalGroupOfDTopCompatibleOfDiffeologicalGroupOfLocallyCompactSpace
{G : Type u_1}
[Group G]
[DiffeologicalSpace G]
[TopologicalSpace G]
[DTopCompatible G]
[DiffeologicalGroup G]
[LocallyCompactSpace G]
:
Variant of DiffeologicalGroup.topologicalGroup phrased in terms of spaces equipped with
DTopCompatible topologies.
instance
instIsTopologicalAddGroupOfDTopCompatibleOfDiffeologicalAddGroupOfLocallyCompactSpace
{G : Type u_1}
[AddGroup G]
[DiffeologicalSpace G]
[TopologicalSpace G]
[DTopCompatible G]
[DiffeologicalAddGroup G]
[LocallyCompactSpace G]
:
Variant of DiffeologicalAddGroup.topologicalAddGroup phrased in terms of
spaces equipped with DTopCompatible topologies.