ProCGroups.FoxDifferential.Completed.FreeProC.FiniteQuotientStages

15 Theorems | 8 Definitions | 2 Instances

The principal declarations in this module are:

freeProCFiniteQuotientStageHom The free-group map to a finite quotient of H induced by a family X \(\to\) H. - freeProCFiniteQuotientStageKernel The finite-stage relation subgroup \(\ker(F_X \to H/U)\). - freeProCFiniteQuotientStageHom_of The finite-quotient stage homomorphism for a free pro-\(C\) group has the stated value on representatives. - freeProCFiniteQuotientStageHom_eq_comp The free quotient-stage map is the quotient projection after the original free-group map.

imports

Imported by

Definition FoxDifferential.freeProCFiniteQuotientStageHom

def freeProCFiniteQuotientStageHom
    (φ : X → H) (U : CompletedGroupAlgebraIndexInClass H C) :
    FreeGroup X →* CompletedGroupAlgebraQuotientInClass H C U :=
  FreeGroup.lift fun x : X =>
    openNormalSubgroupInClassProj (C := C) (G := H) U (φ x)

The free-group map to a finite quotient of H induced by a family X \(\to\) H.

Theorem FoxDifferential.freeProCFiniteQuotientStageHom_of

@[simp]
theorem freeProCFiniteQuotientStageHom_of
    (φ : X → H) (U : CompletedGroupAlgebraIndexInClass H C) (x : X) :
    freeProCFiniteQuotientStageHom (C := C) φ U (FreeGroup.of x) =
      (QuotientGroup.mk (φ x) :
        CompletedGroupAlgebraQuotientInClass H C U)

The finite-quotient stage homomorphism for a free pro-\(C\) group has the stated value on representatives.

Show Lean proof

Theorem FoxDifferential.freeProCFiniteQuotientStageHom_eq_comp

theorem freeProCFiniteQuotientStageHom_eq_comp
    (φ : X → H) (U : CompletedGroupAlgebraIndexInClass H C) :
    freeProCFiniteQuotientStageHom (C := C) φ U =
      (openNormalSubgroupInClassProj (C := C) (G := H) U).comp (FreeGroup.lift φ)

The free quotient-stage map is the quotient projection after the original free-group map.

Show Lean proof

Theorem FoxDifferential.freeProCFiniteQuotientStageHom_transition

theorem freeProCFiniteQuotientStageHom_transition
    (φ : X → H) {U V : CompletedGroupAlgebraIndexInClass H C} (hUV : U ≤ V)
    (w : FreeGroup X) :
    (OpenNormalSubgroupInClass.map
      (C := C) (G := H)
      (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV)
        (freeProCFiniteQuotientStageHom (C := C) φ V w) =
      freeProCFiniteQuotientStageHom (C := C) φ U w

Compatibility of finite quotient-stage maps under quotient refinement.

Show Lean proof

Definition FoxDifferential.freeProCFiniteQuotientStageKernel

def freeProCFiniteQuotientStageKernel
    (φ : X → H) (U : CompletedGroupAlgebraIndexInClass H C) :
    Subgroup (FreeGroup X) :=
  (freeProCFiniteQuotientStageHom (C := C) φ U).ker

The finite-stage relation subgroup \(\ker(F_X \to H/U)\).

Instance FoxDifferential.freeProCFiniteQuotientStageKernel_normal

instance freeProCFiniteQuotientStageKernel_normal
    (φ : X → H) (U : CompletedGroupAlgebraIndexInClass H C) :
    (freeProCFiniteQuotientStageKernel (C := C) φ U).Normal := by
  dsimp [freeProCFiniteQuotientStageKernel]
  infer_instance

The finite-stage relation kernel is a normal subgroup.

Theorem FoxDifferential.freeProCFiniteQuotientStageKernel_antitone

theorem freeProCFiniteQuotientStageKernel_antitone
    (φ : X → H) {U V : CompletedGroupAlgebraIndexInClass H C} (hUV : U ≤ V) :
    freeProCFiniteQuotientStageKernel (C := C) φ V ≤
      freeProCFiniteQuotientStageKernel (C := C) φ U

The finite-stage relation kernels are antitone with respect to quotient refinement.

Show Lean proof

Theorem FoxDifferential.freeProCFiniteQuotientStageHom_surjective_of_topologicallyGenerates

theorem freeProCFiniteQuotientStageHom_surjective_of_topologicallyGenerates
    (φ : X → H) (U : CompletedGroupAlgebraIndexInClass H C)
    [DiscreteTopology (CompletedGroupAlgebraQuotientInClass H C U)]
    (hφgen :
      ProCGroups.Generation.TopologicallyGenerates (G := H) (Set.range φ)) :
    Function.Surjective (freeProCFiniteQuotientStageHom (C := C) φ U)

If the original family topologically generates \(H\), then its image generates every discrete finite quotient \(H/U\), so the corresponding free-group map is surjective.

Show Lean proof

Definition FoxDifferential.freeProCFiniteQuotientStageTargetEquiv

def freeProCFiniteQuotientStageTargetEquiv
    (φ : X → H) (U : CompletedGroupAlgebraIndexInClass H C)
    (hsurj : Function.Surjective (freeProCFiniteQuotientStageHom (C := C) φ U)) :
    foxAlgebraicStageTargetQuotient
        (X := X) (freeProCFiniteQuotientStageKernel (C := C) φ U) ≃*
      CompletedGroupAlgebraQuotientInClass H C U :=
  QuotientGroup.quotientKerEquivOfSurjective
    (freeProCFiniteQuotientStageHom (C := C) φ U) hsurj

The canonical identification \(F_X / \ker(F_X \to H/U) \simeq H/U\).

Theorem FoxDifferential.freeProCFiniteQuotientStageTargetEquiv_mk

@[simp]
theorem freeProCFiniteQuotientStageTargetEquiv_mk
    (φ : X → H) (U : CompletedGroupAlgebraIndexInClass H C)
    (hsurj : Function.Surjective (freeProCFiniteQuotientStageHom (C := C) φ U))
    (w : FreeGroup X) :
    freeProCFiniteQuotientStageTargetEquiv (C := C) φ U hsurj
        (QuotientGroup.mk'
          (freeProCFiniteQuotientStageKernel (C := C) φ U) w) =
      freeProCFiniteQuotientStageHom (C := C) φ U w

The finite-quotient target equivalence sends the class of a free word in the stage quotient to its image under the corresponding finite-stage homomorphism.

Show Lean proof

Definition FoxDifferential.freeProCFiniteQuotientStageQMap

def freeProCFiniteQuotientStageQMap
    (φ : X → H) (U : CompletedGroupAlgebraIndexInClass H C)
    (hsurj : Function.Surjective (freeProCFiniteQuotientStageHom (C := C) φ U)) :
    CompletedGroupAlgebraQuotientInClass H C U →*
      foxAlgebraicStageTargetQuotient
        (X := X) (freeProCFiniteQuotientStageKernel (C := C) φ U) :=
  (freeProCFiniteQuotientStageTargetEquiv (C := C) φ U hsurj).symm.toMonoidHom

The finite quotient stage map sends a target quotient class into the corresponding free-group quotient stage through the inverse of the target equivalence.

Theorem FoxDifferential.freeProCFiniteQuotientStageQMap_injective

theorem freeProCFiniteQuotientStageQMap_injective
    (φ : X → H) (U : CompletedGroupAlgebraIndexInClass H C)
    (hsurj : Function.Surjective (freeProCFiniteQuotientStageHom (C := C) φ U)) :
    Function.Injective (freeProCFiniteQuotientStageQMap (C := C) φ U hsurj)

The finite-quotient stage quotient map is injective.

Show Lean proof

Theorem FoxDifferential.freeProCFiniteQuotientStageQMap_generator

@[simp]
theorem freeProCFiniteQuotientStageQMap_generator
    (φ : X → H) (U : CompletedGroupAlgebraIndexInClass H C)
    (hsurj : Function.Surjective (freeProCFiniteQuotientStageHom (C := C) φ U))
    (x : X) :
    freeProCFiniteQuotientStageQMap (C := C) φ U hsurj
        (QuotientGroup.mk (φ x)) =
      QuotientGroup.mk'
        (freeProCFiniteQuotientStageKernel (C := C) φ U) (FreeGroup.of x)

The finite-quotient stage quotient map sends each generator to its quotient-stage image.

Show Lean proof

Theorem FoxDifferential.freeProCFiniteQuotientStageTargetEquiv_transition

theorem freeProCFiniteQuotientStageTargetEquiv_transition
    (φ : X → H) {U V : CompletedGroupAlgebraIndexInClass H C} (hUV : U ≤ V)
    (hsurjU : Function.Surjective (freeProCFiniteQuotientStageHom (C := C) φ U))
    (hsurjV : Function.Surjective (freeProCFiniteQuotientStageHom (C := C) φ V))
    (y : foxAlgebraicStageTargetQuotient
      (X := X) (freeProCFiniteQuotientStageKernel (C := C) φ V)) :
    freeProCFiniteQuotientStageTargetEquiv (C := C) φ U hsurjU
        (foxAlgebraicStageTargetQuotientMap
          (X := X) (freeProCFiniteQuotientStageKernel_antitone (C := C) φ hUV) y) =
      (OpenNormalSubgroupInClass.map
        (C := C) (G := H)
        (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV)
        (freeProCFiniteQuotientStageTargetEquiv (C := C) φ V hsurjV y)

The compatibility between the canonical \(F_X/kernel \to H/U\) equivalences and quotient refinement.

Show Lean proof

Theorem FoxDifferential.freeProCFiniteQuotientStageQMap_transition

theorem freeProCFiniteQuotientStageQMap_transition
    (φ : X → H) {U V : CompletedGroupAlgebraIndexInClass H C} (hUV : U ≤ V)
    (hsurjU : Function.Surjective (freeProCFiniteQuotientStageHom (C := C) φ U))
    (hsurjV : Function.Surjective (freeProCFiniteQuotientStageHom (C := C) φ V))
    (q : CompletedGroupAlgebraQuotientInClass H C V) :
    freeProCFiniteQuotientStageQMap (C := C) φ U hsurjU
        ((OpenNormalSubgroupInClass.map
          (C := C) (G := H)
          (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV) q) =
      foxAlgebraicStageTargetQuotientMap
        (X := X) (freeProCFiniteQuotientStageKernel_antitone (C := C) φ hUV)
        (freeProCFiniteQuotientStageQMap (C := C) φ V hsurjV q)

The canonical quotient maps commute with quotient refinement.

Show Lean proof

Definition FoxDifferential.freeProCFiniteQuotientStageKernelFamily

def freeProCFiniteQuotientStageKernelFamily
    (φ : X → H) (zcIndex : J → ZCCompletedGroupAlgebraIndex C H) :
    J → Subgroup (FreeGroup X) :=
  fun j => freeProCFiniteQuotientStageKernel (C := C) φ (zcIndex j).2

The finite relation subgroup family attached to a family of \(\mathbb{Z}_C\llbracket H\rrbracket\) stage indices.

Instance FoxDifferential.freeProCFiniteQuotientStageKernelFamily_normal

instance freeProCFiniteQuotientStageKernelFamily_normal
    (φ : X → H) (zcIndex : J → ZCCompletedGroupAlgebraIndex C H) (j : J) :
    (freeProCFiniteQuotientStageKernelFamily (C := C) φ zcIndex j).Normal := by
  dsimp [freeProCFiniteQuotientStageKernelFamily]
  infer_instance

The finite-stage relation kernel is a normal subgroup.

Theorem FoxDifferential.freeProCFiniteQuotientStageKernelFamily_antitone

theorem freeProCFiniteQuotientStageKernelFamily_antitone
    (φ : X → H) (zcIndex : J → ZCCompletedGroupAlgebraIndex C H)
    [Preorder J]
    (hzcIndex : ∀ {i j : J}, i ≤ j → zcIndex i ≤ zcIndex j) :
    ∀ {i j : J}, i ≤ j →
      freeProCFiniteQuotientStageKernelFamily (C := C) φ zcIndex j ≤
        freeProCFiniteQuotientStageKernelFamily (C := C) φ zcIndex i

The finite relation subgroup family is antitone under refinement of the \(\mathbb{Z}_C\llbracket H\rrbracket\) stages.

Show Lean proof

Definition FoxDifferential.freeProCFiniteQuotientStageQMapFamily

def freeProCFiniteQuotientStageQMapFamily
    (φ : X → H) (zcIndex : J → ZCCompletedGroupAlgebraIndex C H)
    [∀ j, DiscreteTopology (CompletedGroupAlgebraQuotientInClass H C (zcIndex j).2)]
    (hφgen :
      ProCGroups.Generation.TopologicallyGenerates (G := H) (Set.range φ)) :
    ∀ j : J,
      CompletedGroupAlgebraQuotientInClass H C (zcIndex j).2 →*
        foxAlgebraicStageTargetQuotient
          (X := X) (freeProCFiniteQuotientStageKernelFamily (C := C) φ zcIndex j) :=
  fun j =>
    freeProCFiniteQuotientStageQMap (C := C) φ (zcIndex j).2
      (freeProCFiniteQuotientStageHom_surjective_of_topologicallyGenerates
        (C := C) φ (zcIndex j).2 hφgen)

The canonical \(H/U_j \to F/N_j\) comparison maps for a finite quotient stage family.

Theorem FoxDifferential.freeProCFiniteQuotientStageQMapFamily_injective

theorem freeProCFiniteQuotientStageQMapFamily_injective
    (φ : X → H) (zcIndex : J → ZCCompletedGroupAlgebraIndex C H)
    [∀ j, DiscreteTopology (CompletedGroupAlgebraQuotientInClass H C (zcIndex j).2)]
    (hφgen :
      ProCGroups.Generation.TopologicallyGenerates (G := H) (Set.range φ)) :
    ∀ j : J,
      Function.Injective
        (freeProCFiniteQuotientStageQMapFamily (C := C) φ zcIndex hφgen j)

The finite-quotient stage family map is injective.

Show Lean proof

Theorem FoxDifferential.freeProCFiniteQuotientStageQMapFamily_generator

@[simp]
theorem freeProCFiniteQuotientStageQMapFamily_generator
    (φ : X → H) (zcIndex : J → ZCCompletedGroupAlgebraIndex C H)
    [∀ j, DiscreteTopology (CompletedGroupAlgebraQuotientInClass H C (zcIndex j).2)]
    (hφgen :
      ProCGroups.Generation.TopologicallyGenerates (G := H) (Set.range φ))
    (j : J) (x : X) :
    freeProCFiniteQuotientStageQMapFamily (C := C) φ zcIndex hφgen j
        (QuotientGroup.mk (φ x)) =
      QuotientGroup.mk'
        (freeProCFiniteQuotientStageKernelFamily (C := C) φ zcIndex j)
        (FreeGroup.of x)

The finite-quotient stage family sends each generator to its quotient-stage image.

Show Lean proof

Theorem FoxDifferential.freeProCFiniteQuotientStageQMapFamily_transition

theorem freeProCFiniteQuotientStageQMapFamily_transition
    (φ : X → H) (zcIndex : J → ZCCompletedGroupAlgebraIndex C H)
    [Preorder J]
    (hzcIndex : ∀ {i j : J}, i ≤ j → zcIndex i ≤ zcIndex j)
    [∀ j, DiscreteTopology (CompletedGroupAlgebraQuotientInClass H C (zcIndex j).2)]
    (hφgen :
      ProCGroups.Generation.TopologicallyGenerates (G := H) (Set.range φ)) :
    ∀ {i j : J} (hij : i ≤ j),
      ∀ q : CompletedGroupAlgebraQuotientInClass H C (zcIndex j).2,
        freeProCFiniteQuotientStageQMapFamily (C := C) φ zcIndex hφgen i
            ((OpenNormalSubgroupInClass.map
              (C := C) (G := H)
              (U := OrderDual.ofDual (zcIndex i).2)
              (V := OrderDual.ofDual (zcIndex j).2)
              (hzcIndex hij).2) q) =
          foxAlgebraicStageTargetQuotientMap
            (X := X)
            (freeProCFiniteQuotientStageKernelFamily_antitone
              (C := C) φ zcIndex hzcIndex hij)
            (freeProCFiniteQuotientStageQMapFamily (C := C) φ zcIndex hφgen j q)

The canonical comparison maps commute with refinement of the \(\mathbb{Z}_C\llbracket H\rrbracket\) stage family.

Show Lean proof

Definition FoxDifferential.freeProCZCBifilteredFiniteQuotientStageCoeffMap

def freeProCZCBifilteredFiniteQuotientStageCoeffMap
    (φ : X → H) (nstage : J → ℕ)
    (zcIndex : J → ZCCompletedGroupAlgebraIndex C H)
    (hmod : ∀ j : J, nstage j ∣ (zcIndex j).1.modulus)
    [∀ j, DiscreteTopology
      (CompletedGroupAlgebraQuotientInClass H C (zcIndex j).2)]
    (hφgen :
      ProCGroups.Generation.TopologicallyGenerates (G := H) (Set.range φ))
    (j : J) :
    ZCCompletedGroupAlgebra C H →+*
      foxAlgebraicStageTargetGroupAlgebra
        (X := X)
        (freeProCFiniteQuotientStageKernelFamily
          (C := C) φ zcIndex j)
        (nstage j) :=
  zcCompletedGroupAlgebraBifilteredStageCoeffMap
    (C := C) (X := X) (H := H)
    (freeProCFiniteQuotientStageKernelFamily
      (C := C) φ zcIndex)
    nstage zcIndex hmod
    (freeProCFiniteQuotientStageQMapFamily
      (C := C) φ zcIndex hφgen) j

The completed-to-finite coefficient map for the actual finite quotient stages \(F_X \to H/U_j\).

Definition FoxDifferential.freeProCZCBifilteredAllFiniteQuotientStageCoeffMap

def freeProCZCBifilteredAllFiniteQuotientStageCoeffMap
    (φ : X → H)
    (hφgen :
      ProCGroups.Generation.TopologicallyGenerates (G := H) (Set.range φ))
    (j : ZCCompletedGroupAlgebraIndex C H) :
    ZCCompletedGroupAlgebra C H →+*
      foxAlgebraicStageTargetGroupAlgebra
        (X := X)
        (freeProCFiniteQuotientStageKernelFamily
          (C := C) φ
          (id : ZCCompletedGroupAlgebraIndex C H →
            ZCCompletedGroupAlgebraIndex C H) j)
        j.1.modulus := by
  letI :
      ∀ j : ZCCompletedGroupAlgebraIndex C H,
        Fact (0 < j.1.modulus) :=
    fun j => ProCIntegerIndex.positiveFact j.1
  letI :
      ∀ j : ZCCompletedGroupAlgebraIndex C H,
        DiscreteTopology
          (CompletedGroupAlgebraQuotientInClass H C j.2) :=
    fun j =>
      QuotientGroup.discreteTopology
        (ProCGroups.openNormalSubgroup_isOpen (G := H)
          ((OrderDual.ofDual j.2).1 : OpenNormalSubgroup H))
  exact
    freeProCZCBifilteredFiniteQuotientStageCoeffMap
      (C := C) (X := X) (H := H) φ (fun j => j.1.modulus)
      (id : ZCCompletedGroupAlgebraIndex C H →
        ZCCompletedGroupAlgebraIndex C H)
      (fun _ => dvd_rfl) hφgen j

The completed-to-finite coefficient map for the standard all-stage family \(j\), a \(\mathbb{Z}_C\)-completed group-algebra index for \(C\) and \(H\), with finite relation subgroup \(\ker(F_X \to H/U_j)\) and the specified coefficient modulus.

Theorem FoxDifferential.zcCompletedGroupAlgebraAllStageQuotientMap_identity_basis_of_hasOpenNormalBasisInClass

omit [IsTopologicalGroup H] in
theorem zcCompletedGroupAlgebraAllStageQuotientMap_identity_basis_of_hasOpenNormalBasisInClass
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hH : HasOpenNormalBasisInClass C H) :
    HasIdentityQuotientKernelNeighbourhoodBasis
      (Y := H)
      (fun j : ZCCompletedGroupAlgebraIndex C H =>
        openNormalSubgroupInClassProj (C := C) (G := H) j.2)

The full family of quotient maps \(H \to H/U\), indexed by the \(\mathbb{Z}_C\)-completed group-algebra indices for \(C\) and \(H\), has identity-neighborhood kernels whenever \(H\) has an open-normal \(C\)-basis. The coefficient coordinate of the index is unspecified here; it is filled with the terminal coefficient quotient.

Show Lean proof

ProCGroups.FoxDifferential.Completed.FreeProC.FiniteQuotientStages

Declarations