Module

FiniteQuotientStages.lean

Nyll.ProCGroups.FoxDifferential.Completed.FreeProC.FiniteQuotientStages

25 declarations indexed from sourceView source ↗

Module documentation

Fox differential: completed — free pro-\(C\) — finite quotient stages

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.

Imports2

Imported by3

def

freeProCFiniteQuotientStageHom

L43 ↗

FoxDifferential.freeProCFiniteQuotientStageHom

Documentation

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

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped Topology
open ProCGroups.ProC
open ProCGroups.Completion
universe u v
section OneStage
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X H : Type u}
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

def freeProCFiniteQuotientStageHom
    (φ : X → H) (U : CompletedGroupAlgebraIndexInClass H C) :
    FreeGroup X →* CompletedGroupAlgebraQuotientInClass H C U

theorem

freeProCFiniteQuotientStageHom_of

L54 ↗

FoxDifferential.freeProCFiniteQuotientStageHom_of

Documentation

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

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped Topology
open ProCGroups.ProC
open ProCGroups.Completion
universe u v
section OneStage
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X H : Type u}
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

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)

theorem

freeProCFiniteQuotientStageHom_eq_comp

L70 ↗

FoxDifferential.freeProCFiniteQuotientStageHom_eq_comp

Documentation

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

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped Topology
open ProCGroups.ProC
open ProCGroups.Completion
universe u v
section OneStage
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X H : Type u}
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

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

theorem

freeProCFiniteQuotientStageHom_transition

L95 ↗

FoxDifferential.freeProCFiniteQuotientStageHom_transition

Documentation

Compatibility of finite quotient-stage maps under quotient refinement.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped Topology
open ProCGroups.ProC
open ProCGroups.Completion
universe u v
section OneStage
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X H : Type u}
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

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

def

freeProCFiniteQuotientStageKernel

L110 ↗

FoxDifferential.freeProCFiniteQuotientStageKernel

Documentation

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

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped Topology
open ProCGroups.ProC
open ProCGroups.Completion
universe u v
section OneStage
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X H : Type u}
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

def freeProCFiniteQuotientStageKernel
    (φ : X → H) (U : CompletedGroupAlgebraIndexInClass H C) :
    Subgroup (FreeGroup X)

instance

freeProCFiniteQuotientStageKernel_normal

L116 ↗

FoxDifferential.freeProCFiniteQuotientStageKernel_normal

Documentation

The finite-stage relation kernel is a normal subgroup.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped Topology
open ProCGroups.ProC
open ProCGroups.Completion
universe u v
section OneStage
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X H : Type u}
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

instance freeProCFiniteQuotientStageKernel_normal
    (φ : X → H) (U : CompletedGroupAlgebraIndexInClass H C) :
    (freeProCFiniteQuotientStageKernel (C := C) φ U).Normal

theorem

freeProCFiniteQuotientStageKernel_antitone

L123 ↗

FoxDifferential.freeProCFiniteQuotientStageKernel_antitone

Documentation

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

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped Topology
open ProCGroups.ProC
open ProCGroups.Completion
universe u v
section OneStage
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X H : Type u}
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

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

theorem

freeProCFiniteQuotientStageHom_surjective_of_topologicallyGenerates

L149 ↗

FoxDifferential.freeProCFiniteQuotientStageHom_surjective_of_topologicallyGenerates

Documentation

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.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped Topology
open ProCGroups.ProC
open ProCGroups.Completion
universe u v
section OneStage
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X H : Type u}
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

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)

def

freeProCFiniteQuotientStageTargetEquiv

L178 ↗

FoxDifferential.freeProCFiniteQuotientStageTargetEquiv

Documentation

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

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped Topology
open ProCGroups.ProC
open ProCGroups.Completion
universe u v
section OneStage
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X H : Type u}
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

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

theorem

freeProCFiniteQuotientStageTargetEquiv_mk

L192 ↗

FoxDifferential.freeProCFiniteQuotientStageTargetEquiv_mk

Documentation

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.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped Topology
open ProCGroups.ProC
open ProCGroups.Completion
universe u v
section OneStage
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X H : Type u}
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

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

def

freeProCFiniteQuotientStageQMap

L206 ↗

FoxDifferential.freeProCFiniteQuotientStageQMap

Documentation

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

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped Topology
open ProCGroups.ProC
open ProCGroups.Completion
universe u v
section OneStage
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X H : Type u}
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

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)

theorem

freeProCFiniteQuotientStageQMap_injective

L215 ↗

FoxDifferential.freeProCFiniteQuotientStageQMap_injective

Documentation

The finite-quotient stage quotient map is injective.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped Topology
open ProCGroups.ProC
open ProCGroups.Completion
universe u v
section OneStage
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X H : Type u}
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

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

theorem

freeProCFiniteQuotientStageQMap_generator

L223 ↗

FoxDifferential.freeProCFiniteQuotientStageQMap_generator

Documentation

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

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped Topology
open ProCGroups.ProC
open ProCGroups.Completion
universe u v
section OneStage
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X H : Type u}
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

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)

theorem

freeProCFiniteQuotientStageTargetEquiv_transition

L257 ↗

FoxDifferential.freeProCFiniteQuotientStageTargetEquiv_transition

Documentation

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

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped Topology
open ProCGroups.ProC
open ProCGroups.Completion
universe u v
section OneStage
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X H : Type u}
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

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)

theorem

freeProCFiniteQuotientStageQMap_transition

L278 ↗

FoxDifferential.freeProCFiniteQuotientStageQMap_transition

Documentation

The canonical quotient maps commute with quotient refinement.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped Topology
open ProCGroups.ProC
open ProCGroups.Completion
universe u v
section OneStage
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X H : Type u}
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

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)

def

freeProCFiniteQuotientStageKernelFamily

L327 ↗

FoxDifferential.freeProCFiniteQuotientStageKernelFamily

Documentation

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

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped Topology
open ProCGroups.ProC
open ProCGroups.Completion
universe u v
section StageFamily
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X H : Type u}
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {J : Type v}

Lean source · statement

def freeProCFiniteQuotientStageKernelFamily
    (φ : X → H) (zcIndex : J → ZCCompletedGroupAlgebraIndex C H) :
    J → Subgroup (FreeGroup X)

instance

freeProCFiniteQuotientStageKernelFamily_normal

L333 ↗

FoxDifferential.freeProCFiniteQuotientStageKernelFamily_normal

Documentation

The finite-stage relation kernel is a normal subgroup.

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped Topology
open ProCGroups.ProC
open ProCGroups.Completion
universe u v
section StageFamily
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X H : Type u}
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {J : Type v}

Lean source · statement

instance freeProCFiniteQuotientStageKernelFamily_normal
    (φ : X → H) (zcIndex : J → ZCCompletedGroupAlgebraIndex C H) (j : J) :
    (freeProCFiniteQuotientStageKernelFamily (C := C) φ zcIndex j).Normal

theorem

freeProCFiniteQuotientStageKernelFamily_antitone

L343 ↗

FoxDifferential.freeProCFiniteQuotientStageKernelFamily_antitone

Documentation

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

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped Topology
open ProCGroups.ProC
open ProCGroups.Completion
universe u v
section StageFamily
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X H : Type u}
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {J : Type v}

Lean source · statement

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

def

freeProCFiniteQuotientStageQMapFamily

L354 ↗

FoxDifferential.freeProCFiniteQuotientStageQMapFamily

Documentation

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

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped Topology
open ProCGroups.ProC
open ProCGroups.Completion
universe u v
section StageFamily
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X H : Type u}
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {J : Type v}

Lean source · statement

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)

theorem

freeProCFiniteQuotientStageQMapFamily_injective

L369 ↗

FoxDifferential.freeProCFiniteQuotientStageQMapFamily_injective

Documentation

The finite-quotient stage family map is injective.

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped Topology
open ProCGroups.ProC
open ProCGroups.Completion
universe u v
section StageFamily
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X H : Type u}
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {J : Type v}

Lean source · statement

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)

theorem

freeProCFiniteQuotientStageQMapFamily_generator

L384 ↗

FoxDifferential.freeProCFiniteQuotientStageQMapFamily_generator

Documentation

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

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped Topology
open ProCGroups.ProC
open ProCGroups.Completion
universe u v
section StageFamily
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X H : Type u}
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {J : Type v}

Lean source · statement

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)

theorem

freeProCFiniteQuotientStageQMapFamily_transition

L403 ↗

FoxDifferential.freeProCFiniteQuotientStageQMapFamily_transition

Documentation

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

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped Topology
open ProCGroups.ProC
open ProCGroups.Completion
universe u v
section StageFamily
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X H : Type u}
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {J : Type v}

Lean source · statement

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)

def

freeProCZCBifilteredFiniteQuotientStageCoeffMap

L446 ↗

FoxDifferential.freeProCZCBifilteredFiniteQuotientStageCoeffMap

Documentation

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

Source context 14 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped Topology
open ProCGroups.ProC
open ProCGroups.Completion
universe u v
section BifilteredFiniteQuotientStages
variable {C : ProCGroups.FiniteGroupClass}
variable {X H : Type u}
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
variable {J : Type v} [Preorder J]

Lean source · statement

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)

def

freeProCZCBifilteredAllFiniteQuotientStageCoeffMap

L474 ↗

FoxDifferential.freeProCZCBifilteredAllFiniteQuotientStageCoeffMap

Documentation

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.

Source context 14 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped Topology
open ProCGroups.ProC
open ProCGroups.Completion
universe u v
section BifilteredFiniteQuotientStages
variable {C : ProCGroups.FiniteGroupClass}
variable {X H : Type u}
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
variable {J : Type v} [Preorder J]

Lean source · statement

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

theorem

zcCompletedGroupAlgebraAllStageQuotientMap_identity_basis_of_hasOpenNormalBasisInClass

L519 ↗

FoxDifferential.zcCompletedGroupAlgebraAllStageQuotientMap_identity_basis_of_hasOpenNormalBasisInClass

Documentation

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.

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped Topology
open ProCGroups.ProC
open ProCGroups.Completion
universe u v
section FullStageQuotientBasis
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {H : Type u}
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [IsTopologicalGroup H] in

Lean source · full declaration

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) := by
  intro U hU hUone
  rcases hH U hU hUone with ⟨V, hVU, hCV⟩
  let Vc : OpenNormalSubgroupInClass C H := ⟨V, hCV⟩
  refine ⟨(ProCIntegerIndex.terminal (C := C) inferInstance, OrderDual.toDual Vc), ?_⟩
  intro z hz
  apply hVU
  exact
    (QuotientGroup.eq_one_iff
      (N := ((V : OpenNormalSubgroup H) : Subgroup H)) z).1 hz

Module documentation

Fox differential: completed — free pro-\(C\) — finite quotient stages

Declarations