Module

FundamentalFormula.lean

Nyll.ProCGroups.FoxDifferential.Completed.FreeProC.FundamentalFormula

11 declarations indexed from sourceView source ↗

Module documentation

Fox differential: completed — free pro-\(C\) — fundamental formula

The principal declarations in this module are:

freeProCChosenULift_closedGenerated_fundamental_formula_stageProj

At each finite stage, the chosen \(U\)-lift closed-generation map satisfies the fundamental formula after projection.

freeProCChosenULift_closedGen_fundFormula_of_stageProjsSeparate

Separation by finite-stage projections implies the closed-generation fundamental formula for the chosen \(U\)-lifts.

freeProCChosenULift_closedGen_fundFormula_of_relSubmoduleClosed

Closedness of the completed relation submodule implies the closed-generation fundamental formula for the chosen \(U\)-lifts.

freeProC_zcDiffModuleRelSubmoduleClosed_of_closedGen_fundFormula

The closed-generation fundamental formula implies closedness of the completed differential-module relation submodule.

Imports2

Imported by2

theorem

freeProCChosenULift_closedGenerated_fundamental_formula_stageProj

L48 ↗

CrowellExactSequence.freeProCChosenULift_closedGenerated_fundamental_formula_stageProj

Documentation

At each finite stage, the chosen \(U\)-lift closed-generation map satisfies the fundamental formula after projection.

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 freeProCChosenULift_closedGenerated_fundamental_formula_stageProj
    [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)
    (i : ZCCompletedDifferentialModuleIndex
        C psi.toMonoidHom)
    (g : sourceData.carrier) :
    zcCompletedDifferentialModuleStageProjection
        C psi.toMonoidHom i
        (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)) =
      zcCompletedDifferentialModuleStageProjection
        C psi.toMonoidHom i
        (zcUniversalDifferential C psi.toMonoidHom 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))
  have hH : ProCGroups.ProC.HasOpenNormalBasisInClass C (H) :=
    HasOpenNormalBasisInClass.of_surjective hC.melnikovFormation.formation
      sourceData.isEpimorphicallyFree.hasOpenNormalBasisInClass psi hpsi
  have hφHconv :
      ProCGroups.FreeProC.FamilyConvergesToOneAlongOpenSubgroups
        (G := H) (fun i : ULift.{u} (Fin r) => psi (family i)) := by
    simpa [family] using
      freeProCChosenULiftFamilyOfBasisCard_image_convergesToOneAlongOpenSubgroups
        (C := C) sourceData hbasis psi.toMonoidHom
  have hφHgen :
      ProCGroups.Generation.TopologicallyGenerates
        (G := H) (Set.range (fun i : ULift.{u} (Fin r) => psi (family i))) := by
    simpa [family] using
      freeProCChosenULiftFamilyOfBasisCard_image_generates_of_surjective
        (C := C) sourceData hbasis psi hpsi
  simpa [family, hfree, htarget, hφconv] using
    closedGenerated_fundamental_formula_stageProj
      (G := sourceData.carrier) (H := H) C psi family hfree htarget hφconv
      hH hφHconv hφHgen i g

theorem

freeProCChosenULift_closedGen_fundFormula_of_stageProjsSeparate

L115 ↗

CrowellExactSequence.freeProCChosenULift_closedGen_fundFormula_of_stageProjsSeparate

Documentation

Separation by finite-stage projections implies the closed-generation fundamental formula for the chosen \(U\)-lifts.

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 freeProCChosenULift_closedGen_fundFormula_of_stageProjsSeparate
    [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)
    (hsep :
      zcCompletedDifferentialModuleStageProjectionsSeparate
        C psi.toMonoidHom) :
    ∀ 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) =
        zcUniversalDifferential C psi.toMonoidHom 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))
  have hH : ProCGroups.ProC.HasOpenNormalBasisInClass C (H) :=
    HasOpenNormalBasisInClass.of_surjective hC.melnikovFormation.formation
      sourceData.isEpimorphicallyFree.hasOpenNormalBasisInClass psi hpsi
  have hφHconv :
      ProCGroups.FreeProC.FamilyConvergesToOneAlongOpenSubgroups
        (G := H) (fun i : ULift.{u} (Fin r) => psi (family i)) := by
    simpa [family] using
      freeProCChosenULiftFamilyOfBasisCard_image_convergesToOneAlongOpenSubgroups
        (C := C) sourceData hbasis psi.toMonoidHom
  have hφHgen :
      ProCGroups.Generation.TopologicallyGenerates
        (G := H) (Set.range (fun i : ULift.{u} (Fin r) => psi (family i))) := by
    simpa [family] using
      freeProCChosenULiftFamilyOfBasisCard_image_generates_of_surjective
        (C := C) sourceData hbasis psi hpsi
  simpa [family, hfree, htarget, hφconv] using
    closedGenerated_fundamental_formula_naturalTopology_of_separating
      (G := sourceData.carrier) (H := H) C psi family hfree htarget hφconv
      hsep hH hφHconv hφHgen

theorem

freeProCChosenULift_closedGen_fundFormula_of_relSubmoduleClosed

L178 ↗

CrowellExactSequence.freeProCChosenULift_closedGen_fundFormula_of_relSubmoduleClosed

Documentation

Closedness of the completed relation submodule implies the closed-generation fundamental formula for the chosen \(U\)-lifts.

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 · full declaration

theorem freeProCChosenULift_closedGen_fundFormula_of_relSubmoduleClosed
    [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)
    (hclosed :
      zcCompletedDifferentialModuleRelationSubmoduleClosed
        C psi.toMonoidHom) :
    ∀ 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) =
        zcUniversalDifferential C psi.toMonoidHom g := by
  exact
    freeProCChosenULift_closedGen_fundFormula_of_stageProjsSeparate
      (H := H) (C := C) (hC := hC) sourceData hbasis psi hpsi
      (freeProC_zcDiffModuleStageProjsSeparate_of_relSubmoduleClosed
        (H := H) (C := C) (hC := hC) sourceData psi hclosed)

theorem

freeProC_zcDiffModuleRelSubmoduleClosed_of_closedGen_fundFormula

L218 ↗

CrowellExactSequence.freeProC_zcDiffModuleRelSubmoduleClosed_of_closedGen_fundFormula

Documentation

The closed-generation fundamental formula implies closedness of the completed differential-module relation submodule.

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 freeProC_zcDiffModuleRelSubmoduleClosed_of_closedGen_fundFormula
    [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)
    (hfundamental :
      let htarget :=
        freeProCClosedGeneratedTarget_proC_of_surjective
          (H := H) (C := C) (hC := hC) sourceData hbasis psi hpsi
      ∀ 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))
              htarget
              (freeProCZCFoxSemiClosedGenGenerator_convergesToOneAlongOpenSubgroups_of_finite
                (C := C)
                (fun i : ULift.{u} (Fin r) =>
                  psi (freeProCChosenULiftFamilyOfBasisCard
                    (C := C) sourceData hbasis i)))
              g) =
          zcUniversalDifferential C psi.toMonoidHom g) :
    zcCompletedDifferentialModuleRelationSubmoduleClosed
      C psi.toMonoidHom := 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))
  have hH : HasOpenNormalBasisInClass C H :=
    HasOpenNormalBasisInClass.of_surjective
      hC.melnikovFormation.formation
      sourceData.isEpimorphicallyFree.hasOpenNormalBasisInClass psi hpsi
  have hφHconv :
      ProCGroups.FreeProC.FamilyConvergesToOneAlongOpenSubgroups
        (G := H) (fun i : ULift.{u} (Fin r) => psi (family i)) := by
    simpa [family] using
      freeProCChosenULiftFamilyOfBasisCard_image_convergesToOneAlongOpenSubgroups
        (C := C) sourceData hbasis psi.toMonoidHom
  have hφHgen :
      ProCGroups.Generation.TopologicallyGenerates
        (G := H) (Set.range (fun i : ULift.{u} (Fin r) => psi (family i))) := by
    simpa [family] using
      freeProCChosenULiftFamilyOfBasisCard_image_generates_of_surjective
        (C := C) sourceData hbasis psi hpsi
  exact
    zcDiffModuleRelSubmoduleClosed_of_closedGenCoord_hasOpenNormalBasisInClass_of_fundFormula
      (G := sourceData.carrier) (H := H) C psi family hfree htarget hφconv
      sourceData.isEpimorphicallyFree.hasOpenNormalBasisInClass hH hφHconv hφHgen
      (by simpa [family, hfree, htarget, hφconv] using hfundamental)

theorem

freeProC_zcDiffModuleRelSubmoduleClosed_iff_closedGenCoord_inj

L284 ↗

CrowellExactSequence.freeProC_zcDiffModuleRelSubmoduleClosed_iff_closedGenCoord_inj

Documentation

For the chosen finite free pro-C basis, relation-submodule closedness is equivalent to injectivity of the closed-generated coordinate map.

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_closedGenCoord_inj
    [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) :
    zcCompletedDifferentialModuleRelationSubmoduleClosed
        C psi.toMonoidHom ↔
      Function.Injective
        (freeProCChosenULift_closedGeneratedCoordinateMap
          (H := H) (C := C) (hC := hC) sourceData hbasis psi hpsi)

theorem

freeProC_zcDiffModuleRelSubmoduleClosed_of_closedGenCoord_inj

L354 ↗

CrowellExactSequence.freeProC_zcDiffModuleRelSubmoduleClosed_of_closedGenCoord_inj

Documentation

Injectivity of the closed-generated coordinate map implies closedness of the completed differential-module relation submodule.

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_of_closedGenCoord_inj
    [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)
    (hcoord_inj :
      Function.Injective
        (freeProCChosenULift_closedGeneratedCoordinateMap
          (H := H) (C := C) (hC := hC) sourceData hbasis psi hpsi)) :
    zcCompletedDifferentialModuleRelationSubmoduleClosed
      C psi.toMonoidHom

theorem

freeProCChosenULift_closedGen_fundFormula_of_closedGenCoord_inj

L375 ↗

CrowellExactSequence.freeProCChosenULift_closedGen_fundFormula_of_closedGenCoord_inj

Documentation

Injectivity of the closed-generated coordinate map implies the closed-generated fundamental formula for the chosen \(U\)-lifts.

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 · full declaration

theorem freeProCChosenULift_closedGen_fundFormula_of_closedGenCoord_inj
    [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)
    (hcoord_inj :
      Function.Injective
        (freeProCChosenULift_closedGeneratedCoordinateMap
          (H := H) (C := C) (hC := hC) sourceData hbasis psi hpsi)) :
    let htarget :=
      freeProCClosedGeneratedTarget_proC_of_surjective
        (H := H) (C := C) (hC := hC) sourceData hbasis psi hpsi
    ∀ 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))
            htarget
            (freeProCZCFoxSemiClosedGenGenerator_convergesToOneAlongOpenSubgroups_of_finite
              (C := C)
              (fun i : ULift.{u} (Fin r) =>
                psi (freeProCChosenULiftFamilyOfBasisCard
                  (C := C) sourceData hbasis i)))
            g) =
        zcUniversalDifferential C psi.toMonoidHom g := by
  exact
    freeProCChosenULift_closedGen_fundFormula_of_relSubmoduleClosed
      (H := H) (C := C) (hC := hC) sourceData hbasis psi hpsi
      (freeProC_zcDiffModuleRelSubmoduleClosed_of_closedGenCoord_inj
        (H := H) (C := C) (hC := hC) sourceData hbasis psi hpsi hcoord_inj)

theorem

chosenULift_hbasis_A_of_closedGen_fundFormula

L418 ↗

CrowellExactSequence.chosenULift_hbasis_A_of_closedGen_fundFormula

Documentation

The closed-generation fundamental formula supplies the required chosen-\(U\)-lift basis data for \(A\).

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 chosenULift_hbasis_A_of_closedGen_fundFormula
    [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
    (hForm : ProCGroups.FiniteGroupClass.Formation 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)
    (htarget :
      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)))
    (hfundamental :
      ∀ 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))
              htarget
              (freeProCZCFoxSemiClosedGenGenerator_convergesToOneAlongOpenSubgroups_of_finite
                (C := C)
                (fun i : ULift.{u} (Fin r) =>
                  psi (freeProCChosenULiftFamilyOfBasisCard
                    (C := C) sourceData hbasis i)))
              g) =
          zcUniversalDifferential C psi.toMonoidHom g) :
    IsPresentedCompletedDifferentialFamilyBasisProCInteger
      (G := sourceData.carrier) (H := H) C psi
      (freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis) := by
  let family : ULift.{u} (Fin r) → sourceData.carrier :=
    freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis
  let hfree :=
    freeProCChosenULiftFamilyOfBasisCard_isEpimorphicallyFree (C := C) sourceData hbasis
  let hφconv :=
    freeProCZCFoxSemiClosedGenGenerator_convergesToOneAlongOpenSubgroups_of_finite
      (C := C) (fun i : ULift.{u} (Fin r) => psi (family i))
  have hH : HasOpenNormalBasisInClass C H :=
    HasOpenNormalBasisInClass.of_surjective
      hForm
      sourceData.isEpimorphicallyFree.hasOpenNormalBasisInClass psi hpsi
  have hφHconv :
      ProCGroups.FreeProC.FamilyConvergesToOneAlongOpenSubgroups
        (G := H) (fun i : ULift.{u} (Fin r) => psi (family i)) := by
    simpa [family] using
      freeProCChosenULiftFamilyOfBasisCard_image_convergesToOneAlongOpenSubgroups
        (C := C) sourceData hbasis psi.toMonoidHom
  have hφHgen :
      ProCGroups.Generation.TopologicallyGenerates
        (G := H) (Set.range (fun i : ULift.{u} (Fin r) => psi (family i))) := by
    simpa [family] using
      freeProCChosenULiftFamilyOfBasisCard_image_generates_of_surjective
        (C := C) sourceData hbasis psi hpsi
  exact
    isPresentedCompletedDifferentialFamilyBasisZC_of_closedGen_fundFormula
      (G := sourceData.carrier) (H := H) C psi family hfree
      (by simpa [family] using htarget) hφconv hH hφHconv hφHgen
      (by simpa [family, hfree, hφconv] using hfundamental)

theorem

chosenULift_hbasis_A_of_closedGen_fundFormula_continuous

L490 ↗

CrowellExactSequence.chosenULift_hbasis_A_of_closedGen_fundFormula_continuous

Documentation

Continuity of the closed-generated and universal differential formulas promotes the chosen lifted finite family to a basis of the presented completed differential module.

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 chosenULift_hbasis_A_of_closedGen_fundFormula_continuous
    [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
    (hForm : ProCGroups.FiniteGroupClass.Formation 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)
    [TopologicalSpace (ZCCompletedDifferentialModule
      C psi.toMonoidHom)]
    [T2Space (ZCCompletedDifferentialModule
      C psi.toMonoidHom)]
    (htarget :
      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)))
    (hmodule_continuous :
      Continuous
        (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))
                htarget
                (freeProCZCFoxSemiClosedGenGenerator_convergesToOneAlongOpenSubgroups_of_finite
                  (C := C)
                  (fun i : ULift.{u} (Fin r) =>
                    psi (freeProCChosenULiftFamilyOfBasisCard
                      (C := C) sourceData hbasis i)))
                g)))
    (huniv_continuous :
      Continuous
        (fun g : sourceData.carrier =>
          zcUniversalDifferential C psi.toMonoidHom g)) :
    IsPresentedCompletedDifferentialFamilyBasisProCInteger
      (G := sourceData.carrier) (H := H) C psi
      (freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis) := by
  let family : ULift.{u} (Fin r) → sourceData.carrier :=
    freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis
  let hfree :=
    freeProCChosenULiftFamilyOfBasisCard_isEpimorphicallyFree (C := C) sourceData hbasis
  let hφconv :=
    freeProCZCFoxSemiClosedGenGenerator_convergesToOneAlongOpenSubgroups_of_finite
      (C := C) (fun i : ULift.{u} (Fin r) => psi (family i))
  have hH : HasOpenNormalBasisInClass C H :=
    HasOpenNormalBasisInClass.of_surjective
      hForm
      sourceData.isEpimorphicallyFree.hasOpenNormalBasisInClass psi hpsi
  have hφHconv :
      ProCGroups.FreeProC.FamilyConvergesToOneAlongOpenSubgroups
        (G := H) (fun i : ULift.{u} (Fin r) => psi (family i)) := by
    simpa [family] using
      freeProCChosenULiftFamilyOfBasisCard_image_convergesToOneAlongOpenSubgroups
        (C := C) sourceData hbasis psi.toMonoidHom
  have hφHgen :
      ProCGroups.Generation.TopologicallyGenerates
        (G := H) (Set.range (fun i : ULift.{u} (Fin r) => psi (family i))) := by
    simpa [family] using
      freeProCChosenULiftFamilyOfBasisCard_image_generates_of_surjective
        (C := C) sourceData hbasis psi hpsi
  have hfundamental :
      ∀ g : sourceData.carrier,
        presentedCompletedDifferentialFamilyMapProCInteger
            (G := sourceData.carrier) (H := H) C psi family
            (freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
              (C := C) hfree (fun i : ULift.{u} (Fin r) => psi (family i))
              (by simpa [family] using htarget) hφconv g) =
          zcUniversalDifferential C psi.toMonoidHom g :=
    closedGenerated_fundamental_formula_of_continuous
      (G := sourceData.carrier) (H := H) C psi family hfree
      (by simpa [family] using htarget) hφconv hH hφHconv hφHgen
      (by simpa [family, hfree, hφconv] using hmodule_continuous)
      (by simpa using huniv_continuous)
  exact
    chosenULift_hbasis_A_of_closedGen_fundFormula
      (H := H) (C := C) hForm sourceData hbasis psi hpsi htarget
      (by simpa [family, hfree, hφconv] using hfundamental)

theorem

freeProCChosenULiftFamilyOfBasisCard_hbasis_A_of_relationSubmoduleClosed

L582 ↗

CrowellExactSequence.freeProCChosenULiftFamilyOfBasisCard_hbasis_A_of_relationSubmoduleClosed

Documentation

Closedness of the completed relation submodule gives the required basis-indexed chosen-\(U\)-lift family in the Crowell module \(A\).

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 freeProCChosenULiftFamilyOfBasisCard_hbasis_A_of_relationSubmoduleClosed
    [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)
    (hclosed :
      zcCompletedDifferentialModuleRelationSubmoduleClosed
        C psi.toMonoidHom) :
    IsPresentedCompletedDifferentialFamilyBasisProCInteger
      (G := sourceData.carrier) (H := H) C psi
      (freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis)

theorem

freeProCChosenULiftFamilyOfBasisCard_hbasis_A_of_closedGenCoord_inj

L629 ↗

CrowellExactSequence.freeProCChosenULiftFamilyOfBasisCard_hbasis_A_of_closedGenCoord_inj

Documentation

Injectivity of the closed-generated coordinate map gives the finite \(A_{\psi}(C)\)-basis theorem for the chosen lifted basis family.

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 freeProCChosenULiftFamilyOfBasisCard_hbasis_A_of_closedGenCoord_inj
    [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)
    (hcoord_inj :
      Function.Injective
        (freeProCChosenULift_closedGeneratedCoordinateMap
          (H := H) (C := C) (hC := hC) sourceData hbasis psi hpsi)) :
    IsPresentedCompletedDifferentialFamilyBasisProCInteger
      (G := sourceData.carrier) (H := H) C psi
      (freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis)

Module documentation

Fox differential: completed — free pro-\(C\) — fundamental formula

Declarations