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

ProCGroups.FoxDifferential.Completed.FreeProC.FundamentalFormula

11 Theorems

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.
imports
Imported by

Declarations

Theorem CrowellExactSequence.freeProCChosenULift_closedGenerated_fundamental_formula_stageProj 
omit [C.ContainsTrivialQuotients] in
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)

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

Show Lean proof
Theorem CrowellExactSequence.freeProCChosenULift_closedGen_fundFormula_of_stageProjsSeparate 
omit [C.ContainsTrivialQuotients] in
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

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

Show Lean proof
Theorem CrowellExactSequence.freeProCChosenULift_closedGen_fundFormula_of_relSubmoduleClosed 
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

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

Show Lean proof
Theorem CrowellExactSequence.freeProC_zcDiffModuleRelSubmoduleClosed_of_closedGen_fundFormula 
omit [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C] in
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

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

Show Lean proof
Theorem CrowellExactSequence.freeProC_zcDiffModuleRelSubmoduleClosed_iff_closedGenCoord_inj 
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)

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

Show Lean proof
Theorem CrowellExactSequence.freeProC_zcDiffModuleRelSubmoduleClosed_of_closedGenCoord_inj 
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

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

Show Lean proof
Theorem CrowellExactSequence.freeProCChosenULift_closedGen_fundFormula_of_closedGenCoord_inj 
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

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

Show Lean proof
Theorem CrowellExactSequence.chosenULift_hbasis_A_of_closedGen_fundFormula 
omit [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C] in
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)

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

Show Lean proof
Theorem CrowellExactSequence.chosenULift_hbasis_A_of_closedGen_fundFormula_continuous 
omit [C.ContainsTrivialQuotients] in
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)

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

Show Lean proof
Theorem CrowellExactSequence.freeProCChosenULiftFamilyOfBasisCard_hbasis_A_of_relationSubmoduleClosed 
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)

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

Show Lean proof
Theorem CrowellExactSequence.freeProCChosenULiftFamilyOfBasisCard_hbasis_A_of_closedGenCoord_inj 
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)

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

Show Lean proof