NYLL
Module

NaturalTopology.lean

Nyll.ProCGroups.FoxDifferential.Completed.FreeProC.NaturalTopology
8 declarations indexed from sourceView source ↗

Module documentation

Fox differential: completed — free pro-\(C\) — natural topology

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.

Imports4
Imported by3

Declarations

theorem

freeProCClosedGeneratedTarget_proC_of_surjective

L50 ↗
CrowellExactSequence.freeProCClosedGeneratedTarget_proC_of_surjective
Documentation

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

Source context 9 commands

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

namespace CrowellExactSequence
noncomputable section
open FoxDifferential
open ProCGroups.ProC
universe u
variable {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
omit [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C] in
Lean source · full declaration
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)) := by
  let family : ULift.{u} (Fin r) → sourceData.carrier :=
    freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis
  have hH : HasOpenNormalBasisInClass C H :=
    HasOpenNormalBasisInClass.of_surjective
      hC.melnikovFormation.formation
      sourceData.isEpimorphicallyFree.hasOpenNormalBasisInClass psi hpsi
  have hAmbient :
      HasOpenNormalBasisInClass C
        (ZCCompletedFoxSemidirect C (ULift.{u} (Fin r)) H) :=
    FoxDifferential.hasOpenNormalBasisInClass_zcCompletedFoxSemidirect_of_hasOpenNormalBasisInClass
      (C := C) (X := ULift.{u} (Fin r)) (H := H)
      hC.melnikovFormation hH
  simpa [family] using
    FoxDifferential.freeProCZCCompletedFoxSemidirectClosedGeneratedTarget_hasOpenNormalBasisInClass
      (C := C) hC.melnikovFormation.formation
      hC.hereditary hAmbient
      (fun i : ULift.{u} (Fin r) => psi (family i))
theorem

freeProC_zcDiffModuleStageProjsSeparate_of_finiteRelationReductionsReflectRelations

L88 ↗
CrowellExactSequence.freeProC_zcDiffModuleStageProjsSeparate_of_finiteRelationReductionsReflectRelations
Documentation

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.

Source context 9 commands

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

namespace CrowellExactSequence
noncomputable section
open FoxDifferential
open ProCGroups.ProC
universe u
variable {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
omit [C.ContainsTrivialQuotients] in
Lean source · statement
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
theorem

freeProC_t2Space_zcDiffModuleNaturalTopology_of_finiteRelationReductionsReflectRelations

L106 ↗
CrowellExactSequence.freeProC_t2Space_zcDiffModuleNaturalTopology_of_finiteRelationReductionsReflectRelations
Documentation

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

Source context 9 commands

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

namespace CrowellExactSequence
noncomputable section
open FoxDifferential
open ProCGroups.ProC
universe u
variable {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
omit [C.ContainsTrivialQuotients] in
Lean source · statement
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)
theorem

freeProC_zcDiffModuleStageProjsSeparate_of_relSubmoduleClosed

L125 ↗
CrowellExactSequence.freeProC_zcDiffModuleStageProjsSeparate_of_relSubmoduleClosed
Documentation

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

Source context 8 commands

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

namespace CrowellExactSequence
noncomputable section
open FoxDifferential
open ProCGroups.ProC
universe u
variable {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
Lean source · statement
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
theorem

freeProC_t2Space_zcDiffModuleNaturalTopology_of_relSubmoduleClosed

L165 ↗
CrowellExactSequence.freeProC_t2Space_zcDiffModuleNaturalTopology_of_relSubmoduleClosed
Documentation

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

Source context 8 commands

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

namespace CrowellExactSequence
noncomputable section
open FoxDifferential
open ProCGroups.ProC
universe u
variable {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
Lean source · statement
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)
theorem

freeProC_zcDiffModuleRelSubmoduleClosed_iff_stageProjsSeparate

L185 ↗
CrowellExactSequence.freeProC_zcDiffModuleRelSubmoduleClosed_iff_stageProjsSeparate
Documentation

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

Source context 8 commands

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

namespace CrowellExactSequence
noncomputable section
open FoxDifferential
open ProCGroups.ProC
universe u
variable {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
Lean source · statement
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
theorem

freeProC_zcDiffModuleRelSubmoduleClosed_iff_t2_naturalTopology

L222 ↗
CrowellExactSequence.freeProC_zcDiffModuleRelSubmoduleClosed_iff_t2_naturalTopology
Documentation

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

Source context 8 commands

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

namespace CrowellExactSequence
noncomputable section
open FoxDifferential
open ProCGroups.ProC
universe u
variable {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
Lean source · statement
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)
theorem

freeProC_hmodule_continuous_naturalTopology

L262 ↗
CrowellExactSequence.freeProC_hmodule_continuous_naturalTopology
Documentation

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

Source context 9 commands

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

namespace CrowellExactSequence
noncomputable section
open FoxDifferential
open ProCGroups.ProC
universe u
variable {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
omit [C.ContainsTrivialQuotients] in
Lean source · full declaration
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)) := by
  let family : ULift.{u} (Fin r) → sourceData.carrier :=
    freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis
  let hfree :=
    freeProCChosenULiftFamilyOfBasisCard_isEpimorphicallyFree (C := C) sourceData hbasis
  let htarget :=
    freeProCClosedGeneratedTarget_proC_of_surjective
      (H := H) (C := C) (hC := hC) sourceData hbasis psi hpsi
  let hφconv :=
    freeProCZCFoxSemiClosedGenGenerator_convergesToOneAlongOpenSubgroups_of_finite
      (C := C) (fun i : ULift.{u} (Fin r) => psi (family i))
  simpa [family, hfree, htarget, hφconv] using
    continuous_closedGenerated_module_expansion_naturalTopology
      (G := sourceData.carrier) (H := H) C psi family hfree htarget hφconv

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.