Yamaguchi Lean 4 Library
ProCGroups.Completion.FiniteQuotientSystems
ProCGroups/Completion/FiniteQuotientSystems

ProCGroups.Completion.FiniteQuotientSystems

8 Theorem | 4 Definition | 1 Abbreviation | 2 Structure | 6 Instance

This module sets up the finite-stage and inverse-limit description of the construction. It records the stage maps, projections, and comparison lemmas used to pass back to the completed object.

Open this file on GitHub
import
Imported by

Declarations

Structure ProCGroups.Completion.NormalSubgroupInClass GitHub 
structure NormalSubgroupInClass (C : ProCGroups.FiniteGroupClass.{u}) (G : Type u) [Group G] where
  toSubgroup : Subgroup G
  normal' : toSubgroup.Normal
  quotient_mem' : C (G ⧸ toSubgroup)

Normal subgroups whose corresponding quotient belongs to the chosen class \(C\).

Instance ProCGroups.Completion.NormalSubgroupInClass.instCoeOutNormalSubgroupInClass GitHub 
instance instCoeOutNormalSubgroupInClass : CoeOut (NormalSubgroupInClass C G) (Subgroup G) where
  coe N := N.toSubgroup

The class-restricted finite quotient system carries the bundled order, normality, and transition structure determined by its finite-stage data.

Instance ProCGroups.Completion.NormalSubgroupInClass.instNormalCoeNormalSubgroupInClass GitHub 
instance instNormalCoeNormalSubgroupInClass (N : NormalSubgroupInClass C G) :
    (N : Subgroup G).Normal :=
  N.normal'

The class-restricted finite quotient system carries the bundled order, normality, and transition structure determined by its finite-stage data.

Instance ProCGroups.Completion.NormalSubgroupInClass.instLENormalSubgroupInClass GitHub 
instance instLENormalSubgroupInClass : LE (NormalSubgroupInClass C G) where
  le N M := (M : Subgroup G) ≤ (N : Subgroup G)

The class-restricted finite quotient system carries the bundled order, normality, and transition structure determined by its finite-stage data.

Instance ProCGroups.Completion.NormalSubgroupInClass.instPreorderNormalSubgroupInClass GitHub 
instance instPreorderNormalSubgroupInClass : Preorder (NormalSubgroupInClass C G) where
  le := fun N M => (M : Subgroup G) ≤ (N : Subgroup G)
  le_refl N := show (N : Subgroup G) ≤ (N : Subgroup G) from le_rfl
  le_trans N M K hNM hMK := show (K : Subgroup G) ≤ (N : Subgroup G) from hMK.trans hNM

The class-restricted finite quotient system carries the bundled order, normality, and transition structure determined by its finite-stage data.

Theorem ProCGroups.Completion.NormalSubgroupInClass.quotient_mem GitHub 
theorem quotient_mem (N : NormalSubgroupInClass C G) :
    C (G ⧸ (N : Subgroup G))

The quotient attached to a normal subgroup in the finite-quotient index family lies in \(C\).

Show proof
Definition ProCGroups.Completion.NormalSubgroupInClass.map GitHub 
def map {N M : NormalSubgroupInClass C G}
    (hNM : (M : Subgroup G) ≤ (N : Subgroup G)) :
    G ⧸ (M : Subgroup G) →* G ⧸ (N : Subgroup G) :=
  QuotientGroup.map _ _ (MonoidHom.id G) hNM

The canonical transition map between two quotients in the finite-quotient system.

Theorem ProCGroups.Completion.NormalSubgroupInClass.map_surjective GitHub 
theorem map_surjective {N M : NormalSubgroupInClass C G}
    (hNM : (M : Subgroup G) ≤ (N : Subgroup G)) :
    Function.Surjective (map (C := C) (G := G) hNM)

These transition maps are the natural quotient epimorphisms.

Show proof
Theorem ProCGroups.Completion.NormalSubgroupInClass.map_id GitHub 
theorem map_id (N : NormalSubgroupInClass C G) :
    map (C := C) (G := G)
      (le_rfl : (N : Subgroup G) ≤ (N : Subgroup G)) = MonoidHom.id _

The transition map attached to the same normal subgroup in the finite-quotient system is the identity.

Show proof
Theorem ProCGroups.Completion.NormalSubgroupInClass.map_comp GitHub 
theorem map_comp {N M K : NormalSubgroupInClass C G}
    (hNM : (M : Subgroup G) ≤ (N : Subgroup G))
    (hMK : (K : Subgroup G) ≤ (M : Subgroup G)) :
    (map (C := C) (G := G) hNM).comp (map (C := C) (G := G) hMK) =
      map (C := C) (G := G) (hMK.trans hNM)

Transition maps between normal-subgroup-in-class quotients compose along inclusions.

Show proof
Definition ProCGroups.Completion.normalSubgroupInClassSystem GitHub 
def normalSubgroupInClassSystem (C : ProCGroups.FiniteGroupClass.{u}) (G : Type u) [Group G] :
    ProCGroups.InverseSystems.InverseSystem (I := NormalSubgroupInClass C G) where
  X := fun N => G ⧸ (N : Subgroup G)
  topologicalSpace := fun _ => ⊥
  map := fun {N M} hNM =>
    NormalSubgroupInClass.map (C := C) (G := G) (N := N) (M := M)
      (show (M : Subgroup G) ≤ (N : Subgroup G) from hNM)
  continuous_map := by
    intro N M hNM
    letI : TopologicalSpace (G ⧸ (M : Subgroup G)) := ⊥
    letI : TopologicalSpace (G ⧸ (N : Subgroup G)) := ⊥
    letI : DiscreteTopology (G ⧸ (M : Subgroup G)) := ⟨rfl⟩
    exact continuous_of_discreteTopology
  map_id := by
    intro N
    ext g
    rcases QuotientGroup.mk'_surjective (N : Subgroup G) g with ⟨x, rfl⟩
    rfl
  map_comp := by
    intro N M K hNM hMK
    ext g
    rcases QuotientGroup.mk'_surjective (K : Subgroup G) g with ⟨x, rfl⟩
    rfl

The inverse system of quotients \(G/N\), indexed by reverse inclusion. The coordinates carry the discrete topology, matching the finite-quotient setting.

Instance ProCGroups.Completion.instGroupNormalSubgroupInClassSystemX GitHub 
instance instGroupNormalSubgroupInClassSystemX
    (N : NormalSubgroupInClass C G) :
    Group ((normalSubgroupInClassSystem C G).X N) := by
  dsimp [normalSubgroupInClassSystem]
  infer_instance

The class-restricted finite quotient system carries the bundled order, normality, and transition structure determined by its finite-stage data.

Instance ProCGroups.Completion.instIsGroupSystemNormalSubgroupInClassSystem GitHub 
instance instIsGroupSystemNormalSubgroupInClassSystem :
    ProCGroups.InverseSystems.IsGroupSystem (normalSubgroupInClassSystem C G) where
  map_one := by
    intro i j hij
    change
      NormalSubgroupInClass.map
        (C := C) (G := G) (N := i) (M := j)
        (show (j : Subgroup G) ≤ (i : Subgroup G) from hij) 1 = 1
    exact
      (NormalSubgroupInClass.map
        (C := C) (G := G) (N := i) (M := j)
        (show (j : Subgroup G) ≤ (i : Subgroup G) from hij)).map_one
  map_mul := by
    intro i j hij x y
    change
      NormalSubgroupInClass.map
        (C := C) (G := G) (N := i) (M := j)
        (show (j : Subgroup G) ≤ (i : Subgroup G) from hij) (x * y) =
          NormalSubgroupInClass.map
            (C := C) (G := G) (N := i) (M := j)
            (show (j : Subgroup G) ≤ (i : Subgroup G) from hij) x *
          NormalSubgroupInClass.map
            (C := C) (G := G) (N := i) (M := j)
            (show (j : Subgroup G) ≤ (i : Subgroup G) from hij) y
    exact
      (NormalSubgroupInClass.map
        (C := C) (G := G) (N := i) (M := j)
        (show (j : Subgroup G) ≤ (i : Subgroup G) from hij)).map_mul x y
  map_inv := by
    intro i j hij x
    change
      NormalSubgroupInClass.map
        (C := C) (G := G) (N := i) (M := j)
        (show (j : Subgroup G) ≤ (i : Subgroup G) from hij) x⁻¹ =
          (NormalSubgroupInClass.map
            (C := C) (G := G) (N := i) (M := j)
            (show (j : Subgroup G) ≤ (i : Subgroup G) from hij) x)⁻¹
    exact
      (NormalSubgroupInClass.map
        (C := C) (G := G) (N := i) (M := j)
        (show (j : Subgroup G) ≤ (i : Subgroup G) from hij)).map_inv x

The class-restricted finite quotient system carries the bundled order, normality, and transition structure determined by its finite-stage data.

Theorem ProCGroups.Completion.directed_normalSubgroupInClass GitHub 
theorem directed_normalSubgroupInClass (hForm : ProCGroups.FiniteGroupClass.Formation C) :
    Directed (α := NormalSubgroupInClass C G) (· ≤ ·) fun N => N

Under the formation hypothesis, the finite-quotient indexing family is directed by reverse inclusion.

Show proof
Abbreviation ProCGroups.Completion.ProCCompletionLimitCarrier GitHub 
abbrev ProCCompletionLimitCarrier (C : ProCGroups.FiniteGroupClass.{u}) (G : Type u) [Group G] :=
  (normalSubgroupInClassSystem C G).inverseLimit

The inverse-limit carrier built from the quotients \(G/N\) with N \(\triangleleft\) G and \(G/N \in C\). This is the concrete carrier used in the finite-quotient construction, not the public completion object with its universal property.

Structure ProCGroups.Completion.ProCCompletion GitHub 
structure ProCCompletion
    (T : ProCGroups.ProC.ProCTheory.{u})
    (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] where
  carrier : Type u
  [group : Group carrier]
  [topology : TopologicalSpace carrier]
  [topologicalGroup : IsTopologicalGroup carrier]
  map : G →ₜ* carrier
  isCompletion : IsProCCompletion T.predicate G carrier map

A pro-\(C\) completion object: a target, its completion map, and the universal property.

Definition ProCGroups.Completion.proCCompletionLimitCarrierHom GitHub 
noncomputable def proCCompletionLimitCarrierHom
    (C : ProCGroups.FiniteGroupClass.{u}) (G : Type u) [Group G] :
    G →* ProCCompletionLimitCarrier C G where
  toFun g :=
    ⟨fun N => QuotientGroup.mk' (N : Subgroup G) g, by
      intro N M hNM
      rfl⟩
  map_one' := by
    apply (normalSubgroupInClassSystem C G).ext
    intro N
    rfl
  map_mul' := by
    intro x y
    apply (normalSubgroupInClassSystem C G).ext
    intro N
    rfl

The canonical abstract homomorphism from \(G\) to its finite-quotient inverse-limit carrier.

Definition ProCGroups.Completion.proCCompletionLimitCarrierMap GitHub 
noncomputable def proCCompletionLimitCarrierMap
    (C : ProCGroups.FiniteGroupClass.{u}) (G : Type u)
    [Group G] [TopologicalSpace G] [DiscreteTopology G] :
    G →ₜ* ProCCompletionLimitCarrier C G where
  toMonoidHom := proCCompletionLimitCarrierHom C G
  continuous_toFun := continuous_of_discreteTopology

The canonical continuous map from a discrete group to its finite-quotient inverse-limit carrier.

Theorem ProCGroups.Completion.projection_proCCompletionLimitCarrierHom GitHub 
@[simp] theorem projection_proCCompletionLimitCarrierHom
    (N : NormalSubgroupInClass C G) (g : G) :
    (normalSubgroupInClassSystem C G).projection N (proCCompletionLimitCarrierHom C G g) =
      QuotientGroup.mk' (N : Subgroup G) g

Coordinatewise description of the canonical map to the pro-\(C\) completion.

Show proof
Theorem ProCGroups.Completion.projection_proCCompletionLimitCarrierMap GitHub 
@[simp] theorem projection_proCCompletionLimitCarrierMap
    [TopologicalSpace G] [DiscreteTopology G]
    (N : NormalSubgroupInClass C G) (g : G) :
    (normalSubgroupInClassSystem C G).projection N (proCCompletionLimitCarrierMap C G g) =
      QuotientGroup.mk' (N : Subgroup G) g

Coordinatewise description of the canonical continuous map from a discrete group.

Show proof
Theorem ProCGroups.Completion.proCCompletionLimitCarrier_isCompletion GitHub 
theorem proCCompletionLimitCarrier_isCompletion
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    [TopologicalSpace G] [IsTopologicalGroup G] [DiscreteTopology G]
    [IsTopologicalGroup (ProCCompletionLimitCarrier C G)]
    (hCarrier :
      ProCGroups.ProC.IsProCGroup C (ProCCompletionLimitCarrier C G))
    (hdense : DenseRange (proCCompletionLimitCarrierMap C G))
    (hlifts :
      HasUniqueFiniteDiscreteQuotientLifts C (proCCompletionLimitCarrierMap C G)) :
    IsProCCompletion (ProCGroups.ProC.finiteGroupClassProCPredicate C)
      G (ProCCompletionLimitCarrier C G) (proCCompletionLimitCarrierMap C G)

The finite-quotient inverse-limit carrier is a pro-\(C\) completion once the required construction hypotheses are supplied explicitly.

Show proof