Yamaguchi Lean 4 Library
ProCGroups.FoxDifferential.Completed.FreeProC.NaturalTopology
ProCGroups/FoxDifferential/Completed/FreeProC/NaturalTopology

ProCGroups.FoxDifferential.Completed.FreeProC.NaturalTopology

8 Theorems

The principal declarations in this module are:

  • freeProCClosedGeneratedTarget_proC_of_surjective For a surjective map from a free pro-\(C\) group, the closed-generated target is again pro-\(C\). - freeProC_zcDiffModuleStageProjsSeparate_of_finiteRelationReductionsReflectRelations Free pro-\(C\) finite-stage separation of \(A_{\psi}(C)\), reduced to the relation-reflection form of the finite source, target, and coefficient reductions. The remaining mathematical content is precisely the reflection hypothesis. - freeProC_t2Space_zcDiffModuleNaturalTopology_of_finiteRelationReductionsReflectRelations Free pro-\(C\) Hausdorffness of the finite-stage completed topology on \(A_{\psi}(C)\), reduced to the relation-reflection form of finite-stage separation. - freeProC_zcDiffModuleStageProjsSeparate_of_relSubmoduleClosed Closedness of the completed relation submodule implies that finite-stage projections separate points of the completed differential module.
imports
Imported by

Declarations

Theorem CrowellExactSequence.freeProCClosedGeneratedTarget_proC_of_surjective 
omit [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C] in
theorem freeProCClosedGeneratedTarget_proC_of_surjective
    [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
    (hC : ProCGroups.FiniteGroupClass.FullFormation C)
    (sourceData : ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
    {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
    (psi : ContinuousMonoidHom sourceData.carrier H)
    (hpsi : Function.Surjective psi) :
    HasOpenNormalBasisInClass C
      (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
        (C := C)
        (fun i : ULift.{u} (Fin r) =>
          psi (freeProCChosenULiftFamilyOfBasisCard
            (C := C) sourceData hbasis i)) : Subgroup
          (ZCCompletedFoxSemidirect C (ULift.{u} (Fin r)) H))

For a surjective map from a free pro-\(C\) group, the closed-generated target is again pro-\(C\).

Show Lean proof
Theorem CrowellExactSequence.freeProC_zcDiffModuleStageProjsSeparate_of_finiteRelationReductionsReflectRelations 
omit [C.ContainsTrivialQuotients] in
theorem freeProC_zcDiffModuleStageProjsSeparate_of_finiteRelationReductionsReflectRelations
    (sourceData : ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
    (psi : ContinuousMonoidHom sourceData.carrier H)
    (hreflect :
      zcCompletedDifferentialModuleFiniteRelationReductionsReflectRelations
        C psi.toMonoidHom) :
    zcCompletedDifferentialModuleStageProjectionsSeparate
      C psi.toMonoidHom

Free pro-\(C\) finite-stage separation of \(A_{\psi}(C)\), reduced to the relation-reflection form of the finite source, target, and coefficient reductions. The remaining mathematical content is precisely the reflection hypothesis.

Show Lean proof
Theorem CrowellExactSequence.freeProC_t2Space_zcDiffModuleNaturalTopology_of_finiteRelationReductionsReflectRelations 
omit [C.ContainsTrivialQuotients] in
theorem freeProC_t2Space_zcDiffModuleNaturalTopology_of_finiteRelationReductionsReflectRelations
    (sourceData : ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
    (psi : ContinuousMonoidHom sourceData.carrier H)
    (hreflect :
      zcCompletedDifferentialModuleFiniteRelationReductionsReflectRelations
        C psi.toMonoidHom) :
    @T2Space
      (ZCCompletedDifferentialModule C psi.toMonoidHom)
      (zcCompletedDifferentialModuleNaturalTopology
        C psi.toMonoidHom)

Free pro-\(C\) Hausdorffness of the finite-stage completed topology on \(A_{\psi}(C)\), reduced to the relation-reflection form of finite-stage separation.

Show Lean proof
Theorem CrowellExactSequence.freeProC_zcDiffModuleStageProjsSeparate_of_relSubmoduleClosed 
theorem freeProC_zcDiffModuleStageProjsSeparate_of_relSubmoduleClosed
    (hC : ProCGroups.FiniteGroupClass.FullFormation C)
    (sourceData : ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
    (psi : ContinuousMonoidHom sourceData.carrier H)
    (hclosed :
      zcCompletedDifferentialModuleRelationSubmoduleClosed
        C psi.toMonoidHom) :
    zcCompletedDifferentialModuleStageProjectionsSeparate
      C psi.toMonoidHom

Closedness of the completed relation submodule implies that finite-stage projections separate points of the completed differential module.

Show Lean proof
Theorem CrowellExactSequence.freeProC_t2Space_zcDiffModuleNaturalTopology_of_relSubmoduleClosed 
theorem freeProC_t2Space_zcDiffModuleNaturalTopology_of_relSubmoduleClosed
    (hC : ProCGroups.FiniteGroupClass.FullFormation C)
    (sourceData : ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
    (psi : ContinuousMonoidHom sourceData.carrier H)
    (hclosed :
      zcCompletedDifferentialModuleRelationSubmoduleClosed
        C psi.toMonoidHom) :
    @T2Space
      (ZCCompletedDifferentialModule C psi.toMonoidHom)
      (zcCompletedDifferentialModuleNaturalTopology
        C psi.toMonoidHom)

Closedness of the completed relation submodule makes the natural topology on the completed differential module Hausdorff.

Show Lean proof
Theorem CrowellExactSequence.freeProC_zcDiffModuleRelSubmoduleClosed_iff_stageProjsSeparate 
theorem freeProC_zcDiffModuleRelSubmoduleClosed_iff_stageProjsSeparate
    (hC : ProCGroups.FiniteGroupClass.FullFormation C)
    {sourceData : ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C}
    {psi : ContinuousMonoidHom sourceData.carrier H} :
    zcCompletedDifferentialModuleRelationSubmoduleClosed
        C psi.toMonoidHom ↔
      zcCompletedDifferentialModuleStageProjectionsSeparate
        C psi.toMonoidHom

Closedness of the completed relation submodule is equivalent to separation by all finite-stage projections.

Show Lean proof
Theorem CrowellExactSequence.freeProC_zcDiffModuleRelSubmoduleClosed_iff_t2_naturalTopology 
theorem freeProC_zcDiffModuleRelSubmoduleClosed_iff_t2_naturalTopology
    (hC : ProCGroups.FiniteGroupClass.FullFormation C)
    {sourceData : ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C}
    {psi : ContinuousMonoidHom sourceData.carrier H} :
    zcCompletedDifferentialModuleRelationSubmoduleClosed
        C psi.toMonoidHom ↔
      @T2Space
        (ZCCompletedDifferentialModule C psi.toMonoidHom)
        (zcCompletedDifferentialModuleNaturalTopology
          C psi.toMonoidHom)

Closedness of the completed relation submodule is equivalent to the natural topology being Hausdorff.

Show Lean proof
Theorem CrowellExactSequence.freeProC_hmodule_continuous_naturalTopology 
omit [C.ContainsTrivialQuotients] in
theorem freeProC_hmodule_continuous_naturalTopology
    [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
    (hC : ProCGroups.FiniteGroupClass.FullFormation C)
    (sourceData : ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
    {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
    (psi : ContinuousMonoidHom sourceData.carrier H)
    (hpsi : Function.Surjective psi) :
    @Continuous sourceData.carrier
      (ZCCompletedDifferentialModule C psi.toMonoidHom)
      inferInstance
      (zcCompletedDifferentialModuleNaturalTopology
        C psi.toMonoidHom)
      (fun g : sourceData.carrier =>
        presentedCompletedDifferentialFamilyMapProCInteger
          (G := sourceData.carrier) (H := H) C psi
          (freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis)
          (freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
            (C := C)
            (freeProCChosenULiftFamilyOfBasisCard_isEpimorphicallyFree (C := C) sourceData hbasis)
            (fun i : ULift.{u} (Fin r) =>
              psi (freeProCChosenULiftFamilyOfBasisCard
                (C := C) sourceData hbasis i))
            (freeProCClosedGeneratedTarget_proC_of_surjective
              (H := H) (C := C) (hC := hC) sourceData hbasis psi hpsi)
            (freeProCZCFoxSemiClosedGenGenerator_convergesToOneAlongOpenSubgroups_of_finite
              (C := C)
              (fun i : ULift.{u} (Fin r) =>
                psi (freeProCChosenULiftFamilyOfBasisCard
                  (C := C) sourceData hbasis i)))
            g))

For a finite free pro-\(C\) basis and a surjective presentation, the completed differential-module map is continuous for its natural topology.

Show Lean proof