ProCGroups.FoxDifferential.Completed.FreeProC.RelationReflection

8 Theorems | 6 Definitions | 2 Abbreviations | 2 Instances

This module supplies the finite free-basis family used to reflect completed Fox relations through finite quotient stages, and relates stagewise vanishing to equality in the completed differential module.

imports

Imported by

Abbreviation CrowellExactSequence.freeProCReflectionFamily

abbrev freeProCReflectionFamily
    (sourceData :
      ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
    {r : Nat}
    (hbasis : Cardinal.mk sourceData.basis = r) : ULift.{u} (Fin r) → sourceData.carrier :=
  freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis

The universe-lifted finite free basis supplies the relation-reflection family.

Theorem CrowellExactSequence.freeProCReflectionFamily_target_generates

omit [T2Space H] in
theorem freeProCReflectionFamily_target_generates
    (sourceData :
      ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
    {r : Nat}
    (hbasis : Cardinal.mk sourceData.basis = r)
    (psi : ContinuousMonoidHom sourceData.carrier H)
    (hpsi : Function.Surjective psi) :
    ProCGroups.Generation.TopologicallyGenerates
      (G := H)
      (Set.range (fun i : ULift.{u} (Fin r) =>
        psi (freeProCReflectionFamily (C := C) sourceData hbasis i)))

The target images of the chosen basis topologically generate a surjective target.

Show Lean proof

Definition CrowellExactSequence.freeProCRelationReflectionStageSourceHom

def freeProCRelationReflectionStageSourceHom
    (sourceData :
      ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
    {r : Nat}
    (hbasis : Cardinal.mk sourceData.basis = r)
    (psi : ContinuousMonoidHom sourceData.carrier H)
    (i : ZCCompletedDifferentialModuleIndex
      C psi.toMonoidHom) :
    FreeGroup (ULift.{u} (Fin r)) →*
      zcCompletedDifferentialModuleStageSource
        C psi.toMonoidHom i :=
  (zcCompletedDifferentialModuleStageSourceProj
      C psi.toMonoidHom i).comp
    (FreeGroup.lift (freeProCReflectionFamily (C := C) sourceData hbasis))

The free-group map onto the source quotient used by a differential-module finite stage.

Definition CrowellExactSequence.freeProCRelationReflectionStageKernel

def freeProCRelationReflectionStageKernel
    (sourceData :
      ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
    {r : Nat}
    (hbasis : Cardinal.mk sourceData.basis = r)
    (psi : ContinuousMonoidHom sourceData.carrier H)
    (i : ZCCompletedDifferentialModuleIndex
      C psi.toMonoidHom) :
    Subgroup (FreeGroup (ULift.{u} (Fin r))) :=
  MonoidHom.ker
    (freeProCRelationReflectionStageSourceHom (C := C) sourceData hbasis psi i)

The source kernel used by a differential-module stage, pulled back to the abstract free group on the chosen basis.

Instance CrowellExactSequence.freeProCRelationReflectionStageKernel_normal

instance freeProCRelationReflectionStageKernel_normal
    (sourceData :
      ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
    {r : Nat}
    (hbasis : Cardinal.mk sourceData.basis = r)
    (psi : ContinuousMonoidHom sourceData.carrier H)
    (i : ZCCompletedDifferentialModuleIndex
      C psi.toMonoidHom) :
    (freeProCRelationReflectionStageKernel (C := C) sourceData hbasis psi i).Normal := by
  dsimp [freeProCRelationReflectionStageKernel]
  infer_instance

The relation-reflection stage kernel is a normal subgroup of the free group on the lifted finite basis.

Theorem CrowellExactSequence.freeProCRelationReflectionStageSourceHom_surjective

omit [IsTopologicalGroup H] [T2Space H] in
theorem freeProCRelationReflectionStageSourceHom_surjective
    (sourceData :
      ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
    {r : Nat}
    (hbasis : Cardinal.mk sourceData.basis = r)
    (psi : ContinuousMonoidHom sourceData.carrier H)
    (i : ZCCompletedDifferentialModuleIndex
      C psi.toMonoidHom) :
    Function.Surjective
      (freeProCRelationReflectionStageSourceHom (C := C) sourceData hbasis psi i)

The chosen free basis surjects onto every finite source quotient stage.

Show Lean proof

Definition CrowellExactSequence.freeProCRelationReflectionStageSourceEquiv

def freeProCRelationReflectionStageSourceEquiv
    (sourceData :
      ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
    {r : Nat}
    (hbasis : Cardinal.mk sourceData.basis = r)
    (psi : ContinuousMonoidHom sourceData.carrier H)
    (i : ZCCompletedDifferentialModuleIndex
      C psi.toMonoidHom) :
    foxAlgebraicStageTargetQuotient
        (X := ULift.{u} (Fin r))
        (freeProCRelationReflectionStageKernel (C := C) sourceData hbasis psi i) ≃*
      zcCompletedDifferentialModuleStageSource
        C psi.toMonoidHom i :=
  QuotientGroup.quotientKerEquivOfSurjective
    (freeProCRelationReflectionStageSourceHom (C := C) sourceData hbasis psi i)
    (freeProCRelationReflectionStageSourceHom_surjective
      (C := C) sourceData hbasis psi i)

Identification of the source quotient stage with the corresponding free-group quotient.

Theorem CrowellExactSequence.freeProCRelationReflectionStageSourceEquiv_mk

omit [IsTopologicalGroup H] [T2Space H] in
@[simp]
theorem freeProCRelationReflectionStageSourceEquiv_mk
    (sourceData :
      ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
    {r : Nat}
    (hbasis : Cardinal.mk sourceData.basis = r)
    (psi : ContinuousMonoidHom sourceData.carrier H)
    (i : ZCCompletedDifferentialModuleIndex
      C psi.toMonoidHom)
    (w : FreeGroup (ULift.{u} (Fin r))) :
    freeProCRelationReflectionStageSourceEquiv (C := C) sourceData hbasis psi i
        (QuotientGroup.mk'
          (freeProCRelationReflectionStageKernel (C := C) sourceData hbasis psi i) w) =
      freeProCRelationReflectionStageSourceHom (C := C) sourceData hbasis psi i w

The relation-reflection source-stage equivalence sends the quotient class of a free word to its image under the corresponding source-stage homomorphism.

Show Lean proof

Abbreviation CrowellExactSequence.freeProCRelationReflectionTargetStageKernel

abbrev freeProCRelationReflectionTargetStageKernel
    (sourceData :
      ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
    {r : Nat}
    (hbasis : Cardinal.mk sourceData.basis = r)
    (psi : ContinuousMonoidHom sourceData.carrier H)
    (i : ZCCompletedDifferentialModuleIndex
      C psi.toMonoidHom) :
    Subgroup (FreeGroup (ULift.{u} (Fin r))) :=
  freeProCFiniteQuotientStageKernel
    (C := C)
    (fun x : ULift.{u} (Fin r) =>
      psi (freeProCReflectionFamily (C := C) sourceData hbasis x))
    i.target.2

The target finite Fox relation kernel attached to the target quotient of a \(\mathbb{Z}_C\)-completed differential-module index.

Instance CrowellExactSequence.freeProCRelationReflectionTargetStageKernel_normal

instance freeProCRelationReflectionTargetStageKernel_normal
    (sourceData :
      ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
    {r : Nat}
    (hbasis : Cardinal.mk sourceData.basis = r)
    (psi : ContinuousMonoidHom sourceData.carrier H)
    (i : ZCCompletedDifferentialModuleIndex
      C psi.toMonoidHom) :
    (freeProCRelationReflectionTargetStageKernel (C := C) sourceData hbasis psi i).Normal :=
  inferInstance

The target finite Fox relation kernel is normal.

Theorem CrowellExactSequence.freeProCRelationReflectionTargetStageKernel_antitone

omit [T2Space H] in
theorem freeProCRelationReflectionTargetStageKernel_antitone
    (sourceData :
      ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
    {r : Nat}
    (hbasis : Cardinal.mk sourceData.basis = r)
    (psi : ContinuousMonoidHom sourceData.carrier H)
    {i j : ZCCompletedDifferentialModuleIndex
      C psi.toMonoidHom} (hij : i ≤ j) :
    freeProCRelationReflectionTargetStageKernel (C := C) sourceData hbasis psi j ≤
      freeProCRelationReflectionTargetStageKernel (C := C) sourceData hbasis psi i

Target finite Fox kernels are antitone along differential-module stage refinement.

Show Lean proof

Definition CrowellExactSequence.freeProCRelationReflectionTargetStageQMap

def freeProCRelationReflectionTargetStageQMap
    (sourceData :
      ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
    {r : Nat}
    (hbasis : Cardinal.mk sourceData.basis = r)
    (psi : ContinuousMonoidHom sourceData.carrier H)
    (hpsi : Function.Surjective psi)
    (i : ZCCompletedDifferentialModuleIndex
      C psi.toMonoidHom) :
    CompletedGroupAlgebraQuotientInClass H C i.target.2 →*
      foxAlgebraicStageTargetQuotient
        (X := ULift.{u} (Fin r))
        (freeProCRelationReflectionTargetStageKernel (C := C) sourceData hbasis psi i) := by
  let φ : ULift.{u} (Fin r) → H := fun x =>
    psi (freeProCReflectionFamily (C := C) sourceData hbasis x)
  have hφgen :
      ProCGroups.Generation.TopologicallyGenerates (G := H) (Set.range φ) := by
    simpa [φ] using
      freeProCReflectionFamily_target_generates (C := C) sourceData hbasis psi hpsi
  letI : DiscreteTopology
      (CompletedGroupAlgebraQuotientInClass H C i.target.2) :=
    QuotientGroup.discreteTopology
      (ProCGroups.openNormalSubgroup_isOpen (G := H)
        ((OrderDual.ofDual i.target.2).1 : OpenNormalSubgroup H))
  exact freeProCFiniteQuotientStageQMap
    (C := C) φ i.target.2
    (freeProCFiniteQuotientStageHom_surjective_of_topologicallyGenerates
      (C := C) φ i.target.2 hφgen)

The canonical target quotient comparison map \(H/U_i \to F_X/N_i\).

Theorem CrowellExactSequence.freeProCRelationReflectionTargetStageQMap_generator

omit [T2Space H] in
@[simp 900]
theorem freeProCRelationReflectionTargetStageQMap_generator
    (sourceData :
      ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
    {r : Nat}
    (hbasis : Cardinal.mk sourceData.basis = r)
    (psi : ContinuousMonoidHom sourceData.carrier H)
    (hpsi : Function.Surjective psi)
    (i : ZCCompletedDifferentialModuleIndex
      C psi.toMonoidHom)
    (x : ULift.{u} (Fin r)) :
    freeProCRelationReflectionTargetStageQMap (C := C) sourceData hbasis psi hpsi i
        (QuotientGroup.mk
          (psi (freeProCReflectionFamily (C := C) sourceData hbasis x))) =
      QuotientGroup.mk'
        (freeProCRelationReflectionTargetStageKernel (C := C) sourceData hbasis psi i)
        (FreeGroup.of x)

The generator formula for the free pro-\(C\) relation-reflection target finite-stage quotient map identifies the specified Crowell boundary or coordinate map.

Show Lean proof

Theorem CrowellExactSequence.freeProCRelationReflectionTargetStageQMap_transition

omit [T2Space H] in
theorem freeProCRelationReflectionTargetStageQMap_transition
    (sourceData :
      ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
    {r : Nat}
    (hbasis : Cardinal.mk sourceData.basis = r)
    (psi : ContinuousMonoidHom sourceData.carrier H)
    (hpsi : Function.Surjective psi)
    {i j : ZCCompletedDifferentialModuleIndex
      C psi.toMonoidHom} (hij : i ≤ j)
    (q : CompletedGroupAlgebraQuotientInClass H C j.target.2) :
    freeProCRelationReflectionTargetStageQMap (C := C) sourceData hbasis psi hpsi i
        ((OpenNormalSubgroupInClass.map
          (C := C) (G := H)
          (U := OrderDual.ofDual i.target.2)
          (V := OrderDual.ofDual j.target.2) hij.2.2) q) =
      foxAlgebraicStageTargetQuotientMap
        (X := ULift.{u} (Fin r))
        (freeProCRelationReflectionTargetStageKernel_antitone
          (C := C) sourceData hbasis psi hij)
        (freeProCRelationReflectionTargetStageQMap
          (C := C) sourceData hbasis psi hpsi j q)

Target quotient comparison maps commute with differential-module stage refinement.

Show Lean proof

Definition CrowellExactSequence.freeProCRelationReflectionTargetStageRight

def freeProCRelationReflectionTargetStageRight
    (sourceData :
      ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
    {r : Nat}
    (hbasis : Cardinal.mk sourceData.basis = r)
    (psi : ContinuousMonoidHom sourceData.carrier H)
    (hpsi : Function.Surjective psi)
    (i : ZCCompletedDifferentialModuleIndex
      C psi.toMonoidHom) :
    H →* foxAlgebraicStageTargetQuotient
        (X := ULift.{u} (Fin r))
        (freeProCRelationReflectionTargetStageKernel (C := C) sourceData hbasis psi i) :=
  (freeProCRelationReflectionTargetStageQMap
    (C := C) sourceData hbasis psi hpsi i).comp
    (openNormalSubgroupInClassProj
      (C := C) (G := H) i.target.2)

The target component map used by finite Fox semidirect stages.

Theorem CrowellExactSequence.freeProCRelationReflectionTargetStageRight_generator

omit [T2Space H] in
@[simp 900]
theorem freeProCRelationReflectionTargetStageRight_generator
    (sourceData :
      ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
    {r : Nat}
    (hbasis : Cardinal.mk sourceData.basis = r)
    (psi : ContinuousMonoidHom sourceData.carrier H)
    (hpsi : Function.Surjective psi)
    (i : ZCCompletedDifferentialModuleIndex
      C psi.toMonoidHom)
    (x : ULift.{u} (Fin r)) :
    freeProCRelationReflectionTargetStageRight (C := C) sourceData hbasis psi hpsi i
        (psi (freeProCReflectionFamily (C := C) sourceData hbasis x)) =
      QuotientGroup.mk'
        (freeProCRelationReflectionTargetStageKernel (C := C) sourceData hbasis psi i)
        (FreeGroup.of x)

The target-stage right map sends the chosen generator to its quotient class in the relation-reflection target stage.

Show Lean proof

Definition CrowellExactSequence.freeProCRelationReflectionTargetStageMap

def freeProCRelationReflectionTargetStageMap
    (sourceData :
      ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
    {r : Nat}
    (hbasis : Cardinal.mk sourceData.basis = r)
    (psi : ContinuousMonoidHom sourceData.carrier H)
    (hpsi : Function.Surjective psi)
    (i : ZCCompletedDifferentialModuleIndex
      C psi.toMonoidHom) :
    ZCCompletedFoxSemidirect C (ULift.{u} (Fin r)) H →*
      FoxAlgebraicStageSemidirect
        (X := ULift.{u} (Fin r))
        (freeProCRelationReflectionTargetStageKernel (C := C) sourceData hbasis psi i)
        i.target.1.modulus := by
  letI : ∀ j : ZCCompletedDifferentialModuleIndex
      C psi.toMonoidHom,
      Fact (0 < j.target.1.modulus) :=
    fun j => ProCGroups.Completion.ProCIntegerIndex.positiveFact j.target.1
  exact
    freeProCZCCompletedFoxSemidirectZCBifilteredStageMap
      (C := C) (X := ULift.{u} (Fin r)) (H := H)
      (Nstage := fun j =>
        freeProCRelationReflectionTargetStageKernel (C := C) sourceData hbasis psi j)
      (nstage := fun j => j.target.1.modulus)
      (zcIndex := fun j => j.target)
      (hmod := fun _ => dvd_rfl)
      (qmap := fun j =>
        freeProCRelationReflectionTargetStageQMap
          (C := C) sourceData hbasis psi hpsi j)
      i

The finite Fox semidirect projection attached to one target quotient stage.

Theorem CrowellExactSequence.freeProCRelationReflection_finiteStage_relationBoundaryModuleExact

omit [T2Space H] in
theorem freeProCRelationReflection_finiteStage_relationBoundaryModuleExact
    (sourceData :
      ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
    {r : Nat}
    (hbasis : Cardinal.mk sourceData.basis = r)
    (psi : ContinuousMonoidHom sourceData.carrier H)
    (i : ZCCompletedDifferentialModuleIndex
      C psi.toMonoidHom) :
    foxAlgebraicStageRelationBoundaryModuleExact
      (X := ULift.{u} (Fin r))
      (freeProCRelationReflectionTargetStageKernel (C := C) sourceData hbasis psi i)
      i.target.1.modulus

Each target finite stage attached to the chosen free pro-\(C\) basis satisfies the finite Fox relation-boundary module exactness needed by the approximation theorem.

Show Lean proof

ProCGroups.FoxDifferential.Completed.FreeProC.RelationReflection

Declarations