Smooth orbifolds with finite isotropy

The declarations the status of Tau Ceti's roadmap names as Tau Ceti has them at commit ace60277.

TheoremThe linear local model at a fixed point#

Let a finite group G act continuously on a finite-dimensional real manifold without boundary, fixing y, by maps that are C¹ at y. Inside any neighbourhood s of y there is a chart e sending y to 0 whose domain is G-invariant and preconnected and whose target is a positive strict sublevel set of a σ-invariant inner product, in which G acts linearly through a continuous representation σ. Every element of G is retained, including those acting trivially: g acts as the identity near y, that is, lies in the germ kernel at y, exactly when σ g = 1, and exactly when g fixes every point of the domain of e.

TauCeti.exists_equivariant_chart_target_eq_sumOfConjugatesInnerSublevel_of_contMDiffAt.{u_1, u_2,
    u_3, u_4}
  {E : Type u_1} {H : Type u_2} {M : Type u_3} {G : Type u_4} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H}
  [I.Boundaryless] [TopologicalSpace M] [ChartedSpace H M] [Group G] [Fintype G] [MulAction G M]
  [ContinuousConstSMul G M] {y : M} (hsmooth : ∀ (g : G), ContMDiffAt I I 1 (fun x => g • x) y)
  (hy : ∀ (g : G), g • y = y) {s : Set M} (hs : s ∈ nhds y) :
  ∃ σ e c,
    0 < c ∧
      y ∈ e.source ∧
        ↑e y = 0 ∧
          e.source ⊆ s ∧
            e.target =
                (ContRepresentation.toRepresentation ℝ G E σ).sumOfConjugatesInnerSublevel c ∧
              IsPreconnected e.source ∧
                (∀ (g : G), ∀ z ∈ e.source, g • z ∈ e.source ∧ ↑e (g • z) = (σ g) (↑e z)) ∧
                  ∀ (g : G),
                    (σ g = 1 ↔ g ∈ TauCeti.MulAction.germKernel G y) ∧
                      (σ g = 1 ↔ ∀ z ∈ e.source, g • z = z)
Lean

Formalized in Tau Ceti as TauCeti.exists_equivariant_chart_target_eq_sumOfConjugatesInnerSublevel_of_contMDiffAt.

Sources
LeanTauCeti.exists_equivariant_chart_target_eq_sumOfConjugatesInnerSublevel_of_contMDiffAt
Uses 1
Statement usesTauCeti.MulAction.germKernel

TheoremTauCeti.germKernel_eq_ker#

For a group with torsion stabilizers acting by C¹ maps on a preconnected Hausdorff manifold without boundary, the germ kernel at every point is the kernel of the action: an element acting as the identity near one point acts as the identity everywhere.

TauCeti.germKernel_eq_ker.{u_1, u_2, u_3, u_4, u_5} {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3}
  {M : Type u_4} {G : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [I.Boundaryless] [TopologicalSpace M]
  [ChartedSpace H M] [Group G] [MulAction G M] [CompleteSpace E] [T2Space M] [PreconnectedSpace M]
  (hsmooth : ∀ (g : G), ContMDiff I I 1 fun x => g • x)
  (hG : ∀ (x : M), IsMulTorsion ↥(MulAction.stabilizer G x)) (x : M) :
  TauCeti.MulAction.germKernel G x = (MulAction.toPermHom G M).ker
Lean

Formalized in Tau Ceti as TauCeti.germKernel_eq_ker.

Sources
LeanTauCeti.germKernel_eq_ker
Uses 1 · Used by 1
Statement usesTauCeti.MulAction.germKernel
Used byThe principal part of a finite smooth action

TheoremThe principal part of a finite smooth action#

For a finite group acting by C¹ maps on a preconnected Hausdorff manifold without boundary, the points whose stabilizer is the kernel of the action form a dense set. The action need not be faithful: elements acting trivially are retained in every stabilizer, and generically they are the only ones. The set is also open, by TauCeti.isOpen_setOf_stabilizer_eq_ker.

TauCeti.dense_setOf_stabilizer_eq_ker_of_contMDiff.{u_1, u_2, u_3, u_4, u_5} {𝕜 : Type u_1}
  {E : Type u_2} {H : Type u_3} {M : Type u_4} {G : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E]
  [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [I.Boundaryless]
  [TopologicalSpace M] [ChartedSpace H M] [Group G] [MulAction G M] [CompleteSpace E] [Finite G]
  [T2Space M] [PreconnectedSpace M] (hsmooth : ∀ (g : G), ContMDiff I I 1 fun x => g • x) :
  Dense {x | MulAction.stabilizer G x = (MulAction.toPermHom G M).ker}
Lean

Formalized in Tau Ceti as TauCeti.dense_setOf_stabilizer_eq_ker_of_contMDiff.

Sources
LeanTauCeti.dense_setOf_stabilizer_eq_ker_of_contMDiff
Uses 2
Proof usesTauCeti.germKernel_eq_ker · TauCeti.MulAction.germKernel

TheoremGeneric stabilizer of a finite linear action#

For a finite group acting linearly and continuously on a Hausdorff topological module over a ring in which 0 is a limit of units, for instance a finite-dimensional real vector space, the points whose stabilizer is the kernel of the action form a dense set. The action need not be faithful. The set is also open, by TauCeti.isOpen_setOf_stabilizer_eq_ker.

TauCeti.dense_setOf_stabilizer_eq_ker.{u_1, u_3, u_4} {G : Type u_1} [Group G] (R : Type u_3)
  {V : Type u_4} [Ring R] [TopologicalSpace R] [(nhdsWithin 0 {r | IsUnit r}).NeBot]
  [AddCommGroup V] [_root_.Module R V] [TopologicalSpace V] [ContinuousAdd V] [ContinuousSMul R V]
  [DistribMulAction G V] [SMulCommClass G R V] [T2Space V] [ContinuousConstSMul G V] [Finite G] :
  Dense {v | MulAction.stabilizer G v = (MulAction.toPermHom G V).ker}
Lean

Formalized in Tau Ceti as TauCeti.dense_setOf_stabilizer_eq_ker.

Sources
LeanTauCeti.dense_setOf_stabilizer_eq_ker

DefinitionThe averaging contraction#

The identity of the complex of inhomogeneous cochains is homotopic to the averaging projection onto the invariants placed in degree 0, through the homotopy whose component from degree n + 1 to degree n is (-1)^(n+1) times the average over the last argument (TauCeti.groupCohomology.averagingHomotopy_hom_succ).

TauCeti.groupCohomology.averagingHomotopy.{u} {k G : Type u} [CommRing k] [Group G] [Fintype G]
  [Invertible ↑(Fintype.card G)] (A : Rep.{u, u, u} k G) :
  Homotopy (CategoryTheory.CategoryStruct.id (groupCohomology.inhomogeneousCochains A))
    (TauCeti.groupCohomology.averageCochainMap A)
Lean

Formalized in Tau Ceti as TauCeti.groupCohomology.averagingHomotopy.

Sources
LeanTauCeti.groupCohomology.averagingHomotopy

DefinitionCategoryTheory.ActionCategory.stabilizerMulEquivAut#

The stabilizer of x is the automorphism group of the corresponding object of the action groupoid. Every element of the stabilizer, including one acting trivially on all of X, is kept as its own automorphism, and the multiplication matches g * h = h ≫ g.

CategoryTheory.ActionCategory.stabilizerMulEquivAut.{u_1, u_2} (G : Type u_1) [Group G]
  {X : Type u_2} [MulAction G X] (x : X) :
  ↥(MulAction.stabilizer G x) ≃* CategoryTheory.Aut ((CategoryTheory.ActionCategory.objEquiv G X) x)
Lean

Formalized in Tau Ceti as CategoryTheory.ActionCategory.stabilizerMulEquivAut.

Sources
LeanCategoryTheory.ActionCategory.stabilizerMulEquivAut

TheoremCategoryTheory.ActionCategory.isEmpty_equivalence_punit#

If the group is nontrivial, the point quotient [*/G] is not equivalent to a thin category; in particular it is not equivalent to the point with trivial isotropy.

CategoryTheory.ActionCategory.isEmpty_equivalence_punit.{u_1, u_3, u_4, u_5} {G : Type u_1}
  [Group G] [Nontrivial G] {D : Type u_3} [CategoryTheory.Category.{u_4, u_3} D] [Quiver.IsThin D] :
  IsEmpty (CategoryTheory.ActionCategory G PUnit.{u_5 + 1} ≌ D)
Lean

Formalized in Tau Ceti as CategoryTheory.ActionCategory.isEmpty_equivalence_punit.

Sources
LeanCategoryTheory.ActionCategory.isEmpty_equivalence_punit

DefinitionTauCeti.MulAction.germKernel#

The germ kernel of the action of G at x: the subgroup of the elements of G that act as the identity on a neighbourhood of x.

TauCeti.MulAction.germKernel.{u_1, u_2} (G : Type u_1) {X : Type u_2} [Group G] [MulAction G X]
  [TopologicalSpace X] (x : X) : Subgroup G
Lean

Formalized in Tau Ceti as TauCeti.MulAction.germKernel.

Sources
LeanTauCeti.MulAction.germKernel
Used by 3
Used byTauCeti.germKernel_eq_ker · The linear local model at a fixed point · The principal part of a finite smooth action

InstanceTauCeti.Diffeology.instDiffeologicalSpaceQuotient#

The quotient diffeology on a quotient type: the diffeology coinduced by the projection.

TauCeti.Diffeology.instDiffeologicalSpaceQuotient.{u_1} {X : Type u_1} [DiffeologicalSpace X]
  (s : Setoid X) : DiffeologicalSpace (Quotient s)
Lean

Formalized in Tau Ceti as TauCeti.Diffeology.instDiffeologicalSpaceQuotient.

Sources
LeanTauCeti.Diffeology.instDiffeologicalSpaceQuotient

TheoremTauCeti.TopCat.normalSpace_of_isPushout#

Attaching a normal space B to a normal space X along a closed subspace of B gives a normal space: in a pushout square in TopCat whose side m : A ⟶ B is a closed embedding, the corner P is normal.

TauCeti.TopCat.normalSpace_of_isPushout.{u} {A B X P : TopCat} {g : A ⟶ X} {m : A ⟶ B} {f : X ⟶ P}
  {g₂ : B ⟶ P} (sq : CategoryTheory.IsPushout g m f g₂)
  (hm : Topology.IsClosedEmbedding ⇑(CategoryTheory.ConcreteCategory.hom m)) [NormalSpace ↑X]
  [NormalSpace ↑B] : NormalSpace ↑P
Lean

Formalized in Tau Ceti as TauCeti.TopCat.normalSpace_of_isPushout.

Sources
LeanTauCeti.TopCat.normalSpace_of_isPushout

TheoremTauCeti.TopCat.normalSpace_of_isColimit#

The colimit of a sequence of normal spaces in TopCat whose transition maps are closed embeddings is normal.

TauCeti.TopCat.normalSpace_of_isColimit.{u} {F : CategoryTheory.Functor ℕ TopCat}
  {c : CategoryTheory.Limits.Cocone F}
  (hF :
    ∀ (n : ℕ),
      Topology.IsClosedEmbedding
        ⇑(CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE ⋯))))
  (hc : CategoryTheory.Limits.IsColimit c) [∀ (n : ℕ), NormalSpace ↑(F.obj n)] : NormalSpace ↑c.pt
Lean

Formalized in Tau Ceti as TauCeti.TopCat.normalSpace_of_isColimit.

Sources
LeanTauCeti.TopCat.normalSpace_of_isColimit

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.