ProCGroups.FoxDifferential.Completed.Continuous.ClosedGeneratedCoordinates.Equiv

18 Theorems | 2 Definitions

The principal declarations in this module are:

separatedClosedGeneratedDerivativeCoordinateLinearEquivProCInteger Coordinate equivalence for the separated completed differential module, obtained from the closed-generated Fox coordinates without assuming algebraic relation-submodule closedness. - closedGeneratedDerivativeCoordinateLinearEquivProCInteger_of_fundamental_formula The closed-generated fundamental formula yields a coordinate equivalence for \(A_{\psi}(C)\); the displayed family map is bijective with inverse given by the closed-generated Fox coordinate map. - separatedClosedGeneratedDerivativeCoordinateLinearEquivProCInteger_toLinearMap The linear map underlying the separated closed-generated derivative-coordinate equivalence is the pro-\(C\) integer derivative-coordinate map. - separatedClosedGeneratedDerivativeCoordinateLinearEquivProCInteger_universal The separated finite family map is a left inverse to the separated closed-generated coordinate lift.

import

ProCGroups.FoxDifferential.Completed.Continuous.ClosedGeneratedCoordinates.Basic

Imported by

Definition CrowellExactSequence.separatedClosedGeneratedDerivativeCoordinateLinearEquivProCInteger

def separatedClosedGeneratedDerivativeCoordinateLinearEquivProCInteger
    [T1Space (ZCFreeFoxCoordinates C (X := X) (H := H))]
    [Nonempty
      (ZCCompletedDifferentialModuleIndex C psi.toMonoidHom)]
    (hdir : Directed (· ≤ ·)
      (id : ZCCompletedDifferentialModuleIndex C psi.toMonoidHom →
        ZCCompletedDifferentialModuleIndex C psi.toMonoidHom))
    (hGbasis : ProCGroups.ProC.HasOpenNormalBasisInClass C (G))
    (hH : ProCGroups.ProC.HasOpenNormalBasisInClass C (H))
    (hφHconv :
      ProCGroups.FreeProC.FamilyConvergesToOneAlongOpenSubgroups
        (G := H) (fun i : X => psi (family i)))
    (hφHgen :
      ProCGroups.Generation.TopologicallyGenerates
        (G := H) (Set.range (fun i : X => psi (family i)))) :
    ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom
      ≃ₗ[ZCCompletedGroupAlgebra C H]
        ZCFreeFoxCoordinates C (X := X) (H := H) :=
  LinearEquiv.ofLinear
    (separatedClosedGeneratedDerivativeCoordinatesLinearMapProCInteger
      (G := G) (H := H) C psi family hfree htarget hφconv
      hdir hGbasis hH hφHconv hφHgen)
    (presentedSeparatedDifferentialFamilyMapProCInteger
      (G := G) (H := H) C psi family)
    (separatedClosedGeneratedDerivativeCoordinatesLinearMapProCInteger_comp_familyMap
      (G := G) (H := H) C psi family hfree htarget hφconv
      hdir hGbasis hH hφHconv hφHgen)
    (presentedSepDifferentialFamilyMapZC_comp_sepClosedGenDerivativeCoordinatesLinearMapZC
      (G := G) (H := H) C psi family hfree htarget hφconv
      hdir hGbasis hH hφHconv hφHgen)

Coordinate equivalence for the separated completed differential module, obtained from the closed-generated Fox coordinates without assuming algebraic relation-submodule closedness.

Theorem CrowellExactSequence.separatedClosedGeneratedDerivativeCoordinateLinearEquivProCInteger_toLinearMap

theorem separatedClosedGeneratedDerivativeCoordinateLinearEquivProCInteger_toLinearMap
    [T1Space (ZCFreeFoxCoordinates C (X := X) (H := H))]
    [Nonempty
      (ZCCompletedDifferentialModuleIndex C psi.toMonoidHom)]
    (hdir : Directed (· ≤ ·)
      (id : ZCCompletedDifferentialModuleIndex C psi.toMonoidHom →
        ZCCompletedDifferentialModuleIndex C psi.toMonoidHom))
    (hGbasis : ProCGroups.ProC.HasOpenNormalBasisInClass C (G))
    (hH : ProCGroups.ProC.HasOpenNormalBasisInClass C (H))
    (hφHconv :
      ProCGroups.FreeProC.FamilyConvergesToOneAlongOpenSubgroups
        (G := H) (fun i : X => psi (family i)))
    (hφHgen :
      ProCGroups.Generation.TopologicallyGenerates
        (G := H) (Set.range (fun i : X => psi (family i)))) :
    (separatedClosedGeneratedDerivativeCoordinateLinearEquivProCInteger
      (G := G) (H := H) C psi family hfree htarget hφconv
      hdir hGbasis hH hφHconv hφHgen).toLinearMap =
    separatedClosedGeneratedDerivativeCoordinatesLinearMapProCInteger
      (G := G) (H := H) C psi family hfree htarget hφconv
      hdir hGbasis hH hφHconv hφHgen

The linear map underlying the separated closed-generated derivative-coordinate equivalence is the pro-\(C\) integer derivative-coordinate map.

Show Lean proof

Theorem CrowellExactSequence.separatedClosedGeneratedDerivativeCoordinateLinearEquivProCInteger_universal

@[simp 900]
theorem separatedClosedGeneratedDerivativeCoordinateLinearEquivProCInteger_universal
    [T1Space (ZCFreeFoxCoordinates C (X := X) (H := H))]
    [Nonempty
      (ZCCompletedDifferentialModuleIndex C psi.toMonoidHom)]
    (hdir : Directed (· ≤ ·)
      (id : ZCCompletedDifferentialModuleIndex C psi.toMonoidHom →
        ZCCompletedDifferentialModuleIndex C psi.toMonoidHom))
    (hGbasis : ProCGroups.ProC.HasOpenNormalBasisInClass C (G))
    (hH : ProCGroups.ProC.HasOpenNormalBasisInClass C (H))
    (hφHconv :
      ProCGroups.FreeProC.FamilyConvergesToOneAlongOpenSubgroups
        (G := H) (fun i : X => psi (family i)))
    (hφHgen :
      ProCGroups.Generation.TopologicallyGenerates
        (G := H) (Set.range (fun i : X => psi (family i))))
    (g : G) :
    separatedClosedGeneratedDerivativeCoordinateLinearEquivProCInteger
        (G := G) (H := H) C psi family hfree htarget hφconv
        hdir hGbasis hH hφHconv hφHgen
        (zcSeparatedUniversalDifferential
          C psi.toMonoidHom g) =
      freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
        (C := C) hfree (fun i : X => psi (family i)) htarget hφconv g

The separated finite family map is a left inverse to the separated closed-generated coordinate lift.

Show Lean proof

Theorem CrowellExactSequence.zcDiffModuleStageProj_eq_familyMap_comp_closedGenCoord

theorem zcDiffModuleStageProj_eq_familyMap_comp_closedGenCoord
    (hH : ProCGroups.ProC.HasOpenNormalBasisInClass C (H))
    (hφHconv :
      ProCGroups.FreeProC.FamilyConvergesToOneAlongOpenSubgroups
        (G := H) (fun i : X => psi (family i)))
    (hφHgen :
      ProCGroups.Generation.TopologicallyGenerates
        (G := H) (Set.range (fun i : X => psi (family i))))
    (i : ZCCompletedDifferentialModuleIndex
        C psi.toMonoidHom) :
    zcCompletedDifferentialModuleStageProjection
        C psi.toMonoidHom i =
      ((zcCompletedDifferentialModuleStageProjection
            C psi.toMonoidHom i).comp
        (presentedCompletedDifferentialFamilyMapProCInteger
          (G := G) (H := H) C psi family)).comp
        (closedGeneratedDerivativeCoordinatesLinearMapProCInteger
          (G := G) (H := H) C psi family hfree htarget hφconv
          hH hφHconv hφHgen)

Every finite-stage projection of \(A_{\psi}(C)\) factors through the closed-generated coordinate lift, without assuming finite-stage separation or closedness of the relation submodule.

Show Lean proof

Theorem CrowellExactSequence.zcCompletedDifferentialModuleStageProjection_eq_of_closedGeneratedCoordinate_eq

omit [Fintype X] in
theorem zcCompletedDifferentialModuleStageProjection_eq_of_closedGeneratedCoordinate_eq
    [Finite X]
    (hH : ProCGroups.ProC.HasOpenNormalBasisInClass C (H))
    (hφHconv :
      ProCGroups.FreeProC.FamilyConvergesToOneAlongOpenSubgroups
        (G := H) (fun i : X => psi (family i)))
    (hφHgen :
      ProCGroups.Generation.TopologicallyGenerates
        (G := H) (Set.range (fun i : X => psi (family i))))
    {a b : ZCCompletedDifferentialModule
        C psi.toMonoidHom}
    (hab :
      closedGeneratedDerivativeCoordinatesLinearMapProCInteger
          (G := G) (H := H) C psi family hfree htarget hφconv
          hH hφHconv hφHgen a =
        closedGeneratedDerivativeCoordinatesLinearMapProCInteger
          (G := G) (H := H) C psi family hfree htarget hφconv
          hH hφHconv hφHgen b)
    (i : ZCCompletedDifferentialModuleIndex
        C psi.toMonoidHom) :
    zcCompletedDifferentialModuleStageProjection
        C psi.toMonoidHom i a =
      zcCompletedDifferentialModuleStageProjection
        C psi.toMonoidHom i b

Equality of closed-generated coordinates implies equality after every finite stage projection.

Show Lean proof

Theorem CrowellExactSequence.closedGenDerivativeCoordinatesLinearMapZC_inj_of_stageProjsSeparate

omit [Fintype X] in
theorem closedGenDerivativeCoordinatesLinearMapZC_inj_of_stageProjsSeparate
    [Finite X]
    (hH : ProCGroups.ProC.HasOpenNormalBasisInClass C (H))
    (hφHconv :
      ProCGroups.FreeProC.FamilyConvergesToOneAlongOpenSubgroups
        (G := H) (fun i : X => psi (family i)))
    (hφHgen :
      ProCGroups.Generation.TopologicallyGenerates
        (G := H) (Set.range (fun i : X => psi (family i))))
    (hsep :
      zcCompletedDifferentialModuleStageProjectionsSeparate
        C psi.toMonoidHom) :
    Function.Injective
      (closedGeneratedDerivativeCoordinatesLinearMapProCInteger
        (G := G) (H := H) C psi family hfree htarget hφconv
        hH hφHconv hφHgen)

If finite stage projections already separate points, then the closed-generated coordinate lift is injective.

Show Lean proof

Theorem CrowellExactSequence.closedGenerated_fundamental_formula_iff_closedGeneratedCoordinate_injective

theorem closedGenerated_fundamental_formula_iff_closedGeneratedCoordinate_injective
    {C : ProCGroups.FiniteGroupClass.{u}}
    {psi : ContinuousMonoidHom G H}
    {family : X → G}
    {hfree htarget hφconv}
    (hH : ProCGroups.ProC.HasOpenNormalBasisInClass C (H))
    (hφHconv :
      ProCGroups.FreeProC.FamilyConvergesToOneAlongOpenSubgroups
        (G := H) (fun i : X => psi (family i)))
    (hφHgen :
      ProCGroups.Generation.TopologicallyGenerates
        (G := H) (Set.range (fun i : X => psi (family i)))) :
    (∀ g : G,
      presentedCompletedDifferentialFamilyMapProCInteger
          (G := G) (H := H) C psi family
          (freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
            (C := C) hfree (fun i : X => psi (family i)) htarget hφconv g) =
        zcUniversalDifferential C psi.toMonoidHom g) ↔
      Function.Injective
        (closedGeneratedDerivativeCoordinatesLinearMapProCInteger
          (G := G) (H := H) (C := C) (psi := psi) (family := family)
          (hfree := hfree) (htarget := htarget) (hφconv := hφconv)
          hH hφHconv hφHgen)

The completed fundamental formula for the closed-generated Fox coordinates is equivalent to injectivity of the closed-generated coordinate lift \(A_{\psi}(C) \to \mathbb{Z}_C\llbracket H\rrbracket^{X}\). The forward direction says that the family map and the coordinate lift are inverse linear maps. The reverse direction is the non-circular reduction used in the Morishita-aligned route: since the coordinate lift is already a left inverse to the family map, injectivity forces the formula \(\sum_i D_i(g) d x_i = d g\) in the algebraic Crowell module.

Show Lean proof

Theorem CrowellExactSequence.zcDiffModuleRelSubmoduleClosed_of_closedGenCoord_hasOpenNormalBasisInClass_of_inj

omit [Fintype X] in
theorem zcDiffModuleRelSubmoduleClosed_of_closedGenCoord_hasOpenNormalBasisInClass_of_inj
    (hGbasis : ProCGroups.ProC.HasOpenNormalBasisInClass C (G))
    (hH : ProCGroups.ProC.HasOpenNormalBasisInClass C (H))
    (hφHconv :
      ProCGroups.FreeProC.FamilyConvergesToOneAlongOpenSubgroups
        (G := H) (fun i : X => psi (family i)))
    (hφHgen :
      ProCGroups.Generation.TopologicallyGenerates
        (G := H) (Set.range (fun i : X => psi (family i))))
    (hcoord_inj :
      Function.Injective
        (closedGeneratedDerivativeCoordinatesLinearMapProCInteger
          (G := G) (H := H) C psi family hfree htarget hφconv
          hH hφHconv hφHgen)) :
    zcCompletedDifferentialModuleRelationSubmoduleClosed
      C psi.toMonoidHom

A direct non-circular closedness criterion through the closed-generated coordinate lift. For a pro-\(C\) source the coordinate lift is continuous for the finite-stage natural topology. Thus injectivity of this lift gives closedness of the defining crossed-differential relation submodule by the general Hausdorff target reflection criterion.

Show Lean proof

Theorem CrowellExactSequence.closedGenerated_fundamental_formula_of_continuous

theorem closedGenerated_fundamental_formula_of_continuous
    [TopologicalSpace (ZCCompletedDifferentialModule
      C psi.toMonoidHom)]
    [T2Space (ZCCompletedDifferentialModule
      C psi.toMonoidHom)]
    (hH : ProCGroups.ProC.HasOpenNormalBasisInClass C (H))
    (hφHconv :
      ProCGroups.FreeProC.FamilyConvergesToOneAlongOpenSubgroups
        (G := H) (fun i : X => psi (family i)))
    (hφHgen :
      ProCGroups.Generation.TopologicallyGenerates
        (G := H) (Set.range (fun i : X => psi (family i))))
    (hmodule_continuous :
      Continuous
        (fun g : G =>
          presentedCompletedDifferentialFamilyMapProCInteger
              (G := G) (H := H) C psi family
              (freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
                (C := C) hfree (fun i : X => psi (family i)) htarget hφconv g)))
    (huniv_continuous :
      Continuous
        (fun g : G =>
          zcUniversalDifferential C psi.toMonoidHom g)) :
    ∀ g : G,
      presentedCompletedDifferentialFamilyMapProCInteger
          (G := G) (H := H) C psi family
          (freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
            (C := C) hfree (fun i : X => psi (family i)) htarget hφconv g) =
        zcUniversalDifferential C psi.toMonoidHom g

Closed-generated module-valued fundamental formula from topological uniqueness of continuous crossed differentials. The extra continuity hypotheses are the precise topological input not supplied by the algebraic definition of the \(\mathbb{Z}_C\)-completed differential module: they say that the displayed closed-generated expansion and the universal differential are continuous into a Hausdorff topology on \(A_{\psi}(C)\).

Show Lean proof

Theorem CrowellExactSequence.closedGenerated_fundamental_formula_naturalTopology_of_separating

theorem closedGenerated_fundamental_formula_naturalTopology_of_separating
    (hsep :
      zcCompletedDifferentialModuleStageProjectionsSeparate
        C psi.toMonoidHom)
    (hH : ProCGroups.ProC.HasOpenNormalBasisInClass C (H))
    (hφHconv :
      ProCGroups.FreeProC.FamilyConvergesToOneAlongOpenSubgroups
        (G := H) (fun i : X => psi (family i)))
    (hφHgen :
      ProCGroups.Generation.TopologicallyGenerates
        (G := H) (Set.range (fun i : X => psi (family i)))) :
    ∀ g : G,
      presentedCompletedDifferentialFamilyMapProCInteger
          (G := G) (H := H) C psi family
          (freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
            (C := C) hfree (fun i : X => psi (family i)) htarget hφconv g) =
        zcUniversalDifferential C psi.toMonoidHom g

Natural-topology form of the closed-generated fundamental formula, assuming the finite-stage projections separate points of \(A_{\psi}(C)\).

Show Lean proof

Theorem CrowellExactSequence.zcDiffModuleRelSubmoduleClosed_iff_closedGenCoord_inj_of_hasOpenNormalBasisInClass

omit [Fintype X] in
theorem zcDiffModuleRelSubmoduleClosed_iff_closedGenCoord_inj_of_hasOpenNormalBasisInClass
    {C : ProCGroups.FiniteGroupClass.{u}}
    {psi : ContinuousMonoidHom G H}
    (family : X → G) (hfree htarget hφconv) [Finite X]
    [Nonempty
      (ZCCompletedDifferentialModuleIndex C psi.toMonoidHom)]
    (hdir : Directed (· ≤ ·)
      (id : ZCCompletedDifferentialModuleIndex C psi.toMonoidHom →
        ZCCompletedDifferentialModuleIndex C psi.toMonoidHom))
    (hGbasis : ProCGroups.ProC.HasOpenNormalBasisInClass C (G))
    (hH : ProCGroups.ProC.HasOpenNormalBasisInClass C (H))
    (hφHconv :
      ProCGroups.FreeProC.FamilyConvergesToOneAlongOpenSubgroups
        (G := H) (fun i : X => psi (family i)))
    (hφHgen :
      ProCGroups.Generation.TopologicallyGenerates
        (G := H) (Set.range (fun i : X => psi (family i)))) :
    zcCompletedDifferentialModuleRelationSubmoduleClosed
        C psi.toMonoidHom ↔
      Function.Injective
        (closedGeneratedDerivativeCoordinatesLinearMapProCInteger
          (G := G) (H := H) (C := C) (psi := psi) (family := family)
          (hfree := hfree) (htarget := htarget) (hφconv := hφconv)
          hH hφHconv hφHgen)

For a pro-\(C\) source, closedness of the algebraic crossed-differential relation submodule is equivalent to injectivity of the closed-generated coordinate lift. This is the precise non-circular frontier left by the Morishita-aligned route. The implication from closedness to injectivity goes through finite-stage separation and the completed fundamental formula. The converse uses only continuity of the coordinate lift for the finite-stage natural topology and the Hausdorff target reflection criterion.

Show Lean proof

Theorem CrowellExactSequence.isPresentedCompletedDifferentialFamilyBasisZC_of_closedGen_fundFormula

theorem isPresentedCompletedDifferentialFamilyBasisZC_of_closedGen_fundFormula
    (hH : ProCGroups.ProC.HasOpenNormalBasisInClass C (H))
    (hφHconv :
      ProCGroups.FreeProC.FamilyConvergesToOneAlongOpenSubgroups
        (G := H) (fun i : X => psi (family i)))
    (hφHgen :
      ProCGroups.Generation.TopologicallyGenerates
        (G := H) (Set.range (fun i : X => psi (family i))))
    (hfundamental :
      ∀ g : G,
        presentedCompletedDifferentialFamilyMapProCInteger
            (G := G) (H := H) C psi family
            (freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
              (C := C) hfree (fun i : X => psi (family i)) htarget hφconv g) =
          zcUniversalDifferential C psi.toMonoidHom g) :
    IsPresentedCompletedDifferentialFamilyBasisProCInteger
      (G := G) (H := H) C psi family

Once the closed-generated Fox vector satisfies the universal fundamental formula in \(A_{\psi}(C)\), the displayed family differentials form a finite coordinate basis of \(A_{\psi}(C)\).

Show Lean proof

Theorem CrowellExactSequence.presentedCompletedDifferentialFamilyCoordinatesProCInteger_eq_of_leftInverse

omit [IsTopologicalGroup G] in
theorem presentedCompletedDifferentialFamilyCoordinatesProCInteger_eq_of_leftInverse
    (psi : ContinuousMonoidHom G H)
    {X : Type v} [Fintype X] (family : X -> G)
    (hbasis_A :
      IsPresentedCompletedDifferentialFamilyBasisProCInteger
        (G := G) (H := H) C psi family)
    (L :
      ZCCompletedDifferentialModule C psi.toMonoidHom →ₗ[ZCCompletedGroupAlgebra C H]
        (X → ZCCompletedGroupAlgebra C H))
    (hL :
      L.comp
        (presentedCompletedDifferentialFamilyMapProCInteger
          (G := G) (H := H) C psi family) =
      LinearMap.id) :
    L =
      (presentedCompletedDifferentialFamilyCoordinatesProCInteger
        (G := G) (H := H) C psi family hbasis_A).toLinearMap

A left inverse to a bijective family map is the coordinate inverse associated to the basis.

Show Lean proof

Definition CrowellExactSequence.closedGeneratedDerivativeCoordinateLinearEquivProCInteger_of_fundamental_formula

def closedGeneratedDerivativeCoordinateLinearEquivProCInteger_of_fundamental_formula
    (hH : ProCGroups.ProC.HasOpenNormalBasisInClass C (H))
    (hφHconv :
      ProCGroups.FreeProC.FamilyConvergesToOneAlongOpenSubgroups
        (G := H) (fun i : X => psi (family i)))
    (hφHgen :
      ProCGroups.Generation.TopologicallyGenerates
        (G := H) (Set.range (fun i : X => psi (family i))))
    (hfundamental :
      ∀ g : G,
        presentedCompletedDifferentialFamilyMapProCInteger
            (G := G) (H := H) C psi family
            (freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
              (C := C) hfree (fun i : X => psi (family i)) htarget hφconv g) =
          zcUniversalDifferential C psi.toMonoidHom g) :
    ZCCompletedDifferentialModule C psi.toMonoidHom
      ≃ₗ[ZCCompletedGroupAlgebra C H]
        ZCFreeFoxCoordinates C (X := X) (H := H) :=
  presentedCompletedDifferentialFamilyCoordinatesProCInteger
    (G := G) (H := H) C psi family
    (isPresentedCompletedDifferentialFamilyBasisZC_of_closedGen_fundFormula
      (G := G) (H := H) C psi family hfree htarget hφconv
      hH hφHconv hφHgen hfundamental)

The closed-generated fundamental formula yields a coordinate equivalence for \(A_{\psi}(C)\); the displayed family map is bijective with inverse given by the closed-generated Fox coordinate map.

Theorem CrowellExactSequence.closedGenDerivativeCoordinateLinearEquivZC_of_fundFormula_toLinearMap

theorem closedGenDerivativeCoordinateLinearEquivZC_of_fundFormula_toLinearMap
    (hH : ProCGroups.ProC.HasOpenNormalBasisInClass C (H))
    (hφHconv :
      ProCGroups.FreeProC.FamilyConvergesToOneAlongOpenSubgroups
        (G := H) (fun i : X => psi (family i)))
    (hφHgen :
      ProCGroups.Generation.TopologicallyGenerates
        (G := H) (Set.range (fun i : X => psi (family i))))
    (hfundamental :
      ∀ g : G,
        presentedCompletedDifferentialFamilyMapProCInteger
            (G := G) (H := H) C psi family
            (freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
              (C := C) hfree (fun i : X => psi (family i)) htarget hφconv g) =
          zcUniversalDifferential C psi.toMonoidHom g) :
    (closedGeneratedDerivativeCoordinateLinearEquivProCInteger_of_fundamental_formula
      (G := G) (H := H) C psi family hfree htarget hφconv
      hH hφHconv hφHgen hfundamental).toLinearMap =
      closedGeneratedDerivativeCoordinatesLinearMapProCInteger
        (G := G) (H := H) C psi family hfree htarget hφconv
        hH hφHconv hφHgen

The coordinate equivalence from the fundamental formula has the closed-generated coordinate map as its forward linear map.

Show Lean proof

Theorem CrowellExactSequence.zcDiffModuleRelSubmoduleClosed_of_closedGenCoordPrequotient_continuous_of_fundFormula

theorem zcDiffModuleRelSubmoduleClosed_of_closedGenCoordPrequotient_continuous_of_fundFormula
    [T1Space (ZCFreeFoxCoordinates C (X := X) (H := H))]
    (hH : ProCGroups.ProC.HasOpenNormalBasisInClass C (H))
    (hφHconv :
      ProCGroups.FreeProC.FamilyConvergesToOneAlongOpenSubgroups
        (G := H) (fun i : X => psi (family i)))
    (hφHgen :
      ProCGroups.Generation.TopologicallyGenerates
        (G := H) (Set.range (fun i : X => psi (family i))))
    (hfundamental :
      ∀ g : G,
        presentedCompletedDifferentialFamilyMapProCInteger
            (G := G) (H := H) C psi family
            (freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
              (C := C) hfree (fun i : X => psi (family i)) htarget hφconv g) =
          zcUniversalDifferential C psi.toMonoidHom g)
    (hprecoord_continuous :
      @Continuous
        (CrossedDifferentialPreModule
          (ZCCompletedGroupAlgebra C H) G)
        (ZCFreeFoxCoordinates C (X := X) (H := H))
        (zcCompletedDifferentialPreModuleNaturalTopology
          C psi.toMonoidHom)
        inferInstance
        (fun x =>
          (closedGeneratedDerivativeCoordinateLinearEquivProCInteger_of_fundamental_formula
            (G := G) (H := H) C psi family hfree htarget hφconv
            hH hφHconv hφHgen hfundamental).toLinearMap
            ((crossedDifferentialRelationSubmodule
              (zcCompletedGroupAlgebraScalar
                C psi.toMonoidHom)).mkQ x))) :
    zcCompletedDifferentialModuleRelationSubmoduleClosed
      C psi.toMonoidHom

A completed coordinate equivalence and continuity of the coordinate map composed with the algebraic quotient map imply closedness for the finite-stage pre-module topology.

Show Lean proof

Theorem CrowellExactSequence.zcDiffRelSubmoduleClosed_of_closedGenCoord_fundFormula

theorem zcDiffRelSubmoduleClosed_of_closedGenCoord_fundFormula
    [T1Space (ZCFreeFoxCoordinates C (X := X) (H := H))]
    (hH : ProCGroups.ProC.HasOpenNormalBasisInClass C (H))
    (hφHconv :
      ProCGroups.FreeProC.FamilyConvergesToOneAlongOpenSubgroups
        (G := H) (fun i : X => psi (family i)))
    (hφHgen :
      ProCGroups.Generation.TopologicallyGenerates
        (G := H) (Set.range (fun i : X => psi (family i))))
    (hfundamental :
      ∀ g : G,
        presentedCompletedDifferentialFamilyMapProCInteger
            (G := G) (H := H) C psi family
            (freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
              (C := C) hfree (fun i : X => psi (family i)) htarget hφconv g) =
          zcUniversalDifferential C psi.toMonoidHom g)
    (hcoord_continuous :
      @Continuous
        (ZCCompletedDifferentialModule C psi.toMonoidHom)
        (ZCFreeFoxCoordinates C (X := X) (H := H))
        (zcCompletedDifferentialModuleNaturalTopology
          C psi.toMonoidHom)
        inferInstance
        (closedGeneratedDerivativeCoordinateLinearEquivProCInteger_of_fundamental_formula
          (G := G) (H := H) C psi family hfree htarget hφconv
          hH hφHconv hφHgen hfundamental).toLinearMap) :
    zcCompletedDifferentialModuleRelationSubmoduleClosed
      C psi.toMonoidHom

The closed-generated coordinate equivalence and continuity of the coordinate map \(A_{\psi}(C) \to \mathbb{Z}_C\llbracket H\rrbracket^{X}\) imply closedness for the quotient finite-stage natural topology.

Show Lean proof

Theorem CrowellExactSequence.zcDiffModuleRelSubmoduleClosed_of_closedGenCoord_stage_factorization_of_fundFormula

theorem zcDiffModuleRelSubmoduleClosed_of_closedGenCoord_stage_factorization_of_fundFormula
    [T1Space (ZCFreeFoxCoordinates C (X := X) (H := H))]
    (hH : ProCGroups.ProC.HasOpenNormalBasisInClass C (H))
    (hφHconv :
      ProCGroups.FreeProC.FamilyConvergesToOneAlongOpenSubgroups
        (G := H) (fun i : X => psi (family i)))
    (hφHgen :
      ProCGroups.Generation.TopologicallyGenerates
        (G := H) (Set.range (fun i : X => psi (family i))))
    (hfundamental :
      ∀ g : G,
        presentedCompletedDifferentialFamilyMapProCInteger
            (G := G) (H := H) C psi family
            (freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
              (C := C) hfree (fun i : X => psi (family i)) htarget hφconv g) =
          zcUniversalDifferential C psi.toMonoidHom g) :
    (∀ (x : X) (j : ZCCompletedGroupAlgebraIndex C H),
        ∃ i : ZCCompletedDifferentialModuleIndex
            C psi.toMonoidHom,
          ∃ stageCoord :
            ZCCompletedDifferentialModuleStage
                C psi.toMonoidHom i →
              ZCCompletedGroupAlgebraStage C H j,
            ∀ a :
              ZCCompletedDifferentialModule C psi.toMonoidHom,
              zcCompletedGroupAlgebraProjection C H j
                  (closedGeneratedDerivativeCoordinatesLinearMapProCInteger
                    (G := G) (H := H) C psi family hfree htarget hφconv
                    hH hφHconv hφHgen a x) =
                stageCoord
                  (zcCompletedDifferentialModuleStageProjection
                    C psi.toMonoidHom i a)) →
    zcCompletedDifferentialModuleRelationSubmoduleClosed
      C psi.toMonoidHom

Closedness from the closed-generated fundamental formula and finite-stage coordinate factorization. The factorization hypothesis is the concrete finite-stage compatibility needed to make the closed-generated coordinate map continuous for the natural topology on the algebraic \(A_{\psi}(C)\).

Show Lean proof

Theorem CrowellExactSequence.zcDiffModuleRelSubmoduleClosed_of_closedGenCoord_hasOpenNormalBasisInClass_of_fundFormula

theorem zcDiffModuleRelSubmoduleClosed_of_closedGenCoord_hasOpenNormalBasisInClass_of_fundFormula
    [T1Space (ZCFreeFoxCoordinates C (X := X) (H := H))]
    (hGbasis : ProCGroups.ProC.HasOpenNormalBasisInClass C (G))
    (hH : ProCGroups.ProC.HasOpenNormalBasisInClass C (H))
    (hφHconv :
      ProCGroups.FreeProC.FamilyConvergesToOneAlongOpenSubgroups
        (G := H) (fun i : X => psi (family i)))
    (hφHgen :
      ProCGroups.Generation.TopologicallyGenerates
        (G := H) (Set.range (fun i : X => psi (family i))))
    (hfundamental :
      ∀ g : G,
        presentedCompletedDifferentialFamilyMapProCInteger
            (G := G) (H := H) C psi family
            (freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
              (C := C) hfree (fun i : X => psi (family i)) htarget hφconv g) =
          zcUniversalDifferential C psi.toMonoidHom g) :
    zcCompletedDifferentialModuleRelationSubmoduleClosed
      C psi.toMonoidHom

Closedness from the completed fundamental formula once the source is a concrete pro-\(C\) group. The finite-stage factorization is supplied internally by the open-normal pro-\(C\) basis of the source, so the only remaining mathematical input is the non-circular module-valued fundamental formula.

Show Lean proof

Theorem CrowellExactSequence.closedGenDerivativeCoordinateLinearEquivZC_of_fundFormula_universal

@[simp 900]
theorem closedGenDerivativeCoordinateLinearEquivZC_of_fundFormula_universal
    (hH : ProCGroups.ProC.HasOpenNormalBasisInClass C (H))
    (hφHconv :
      ProCGroups.FreeProC.FamilyConvergesToOneAlongOpenSubgroups
        (G := H) (fun i : X => psi (family i)))
    (hφHgen :
      ProCGroups.Generation.TopologicallyGenerates
        (G := H) (Set.range (fun i : X => psi (family i))))
    (hfundamental :
      ∀ g : G,
        presentedCompletedDifferentialFamilyMapProCInteger
            (G := G) (H := H) C psi family
            (freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
              (C := C) hfree (fun i : X => psi (family i)) htarget hφconv g) =
          zcUniversalDifferential C psi.toMonoidHom g)
    (g : G) :
    closedGeneratedDerivativeCoordinateLinearEquivProCInteger_of_fundamental_formula
        (G := G) (H := H) C psi family hfree htarget hφconv
        hH hφHconv hφHgen hfundamental
        (zcUniversalDifferential C psi.toMonoidHom g) =
      freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
        (C := C) hfree (fun i : X => psi (family i)) htarget hφconv g

The closed-generated coordinate equivalence sends the universal differential of \(g\) to the completed Fox-derivative coordinate vector of \(g\).

Show Lean proof

ProCGroups.FoxDifferential.Completed.Continuous.ClosedGeneratedCoordinates.Equiv

Declarations