Yamaguchi Lean 4 Library
ProCGroups.FoxDifferential.Completed.Continuous.ClosedGeneratedCoordinates.Topology
ProCGroups/FoxDifferential/Completed/Continuous/ClosedGeneratedCoordinates/Topology

ProCGroups.FoxDifferential.Completed.Continuous.ClosedGeneratedCoordinates.Topology

8 Theorems | 1 Definition

The principal declarations in this module are:

  • closedGeneratedDerivativeCoordinateTopologyProCInteger_of_fundamental_formula The coordinate topology on \(A_{\psi}(C)\) transported from the closed-generated coordinate equivalence. - continuous_closedGenDerivativeCoordinateLinearEquivZC_of_fundFormula The closed-generated coordinate equivalence is continuous for the transported coordinate topology on \(A_{\psi}(C)\). - t2Space_closedGenDerivativeCoordinateTopologyZC_of_fundFormula The coordinate topology transported to \(A_{\psi}(C)\) is Hausdorff. - continuous_closedGenDerivativeCoordinateLinearEquivZC_of_fundFormula_symm The inverse of the closed-generated coordinate equivalence is continuous for the transported coordinate topology on \(A_{\psi}(C)\). Equivalently, the displayed family map \(\mathbb{Z}_C\llbracket H\rrbracket^{X} \to A_{\psi}(C)\) is continuous for this topology.
import
Imported by

Declarations

Definition CrowellExactSequence.closedGeneratedDerivativeCoordinateTopologyProCInteger_of_fundamental_formula 
@[implicit_reducible]
def closedGeneratedDerivativeCoordinateTopologyProCInteger_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) :
    TopologicalSpace
      (ZCCompletedDifferentialModule C psi.toMonoidHom) :=
  TopologicalSpace.induced
    (closedGeneratedDerivativeCoordinateLinearEquivProCInteger_of_fundamental_formula
      (G := G) (H := H) C psi family hfree htarget hφconv
      hH hφHconv hφHgen hfundamental)
    inferInstance

The coordinate topology on \(A_{\psi}(C)\) transported from the closed-generated coordinate equivalence.

Theorem CrowellExactSequence.continuous_closedGenDerivativeCoordinateLinearEquivZC_of_fundFormula 
theorem continuous_closedGenDerivativeCoordinateLinearEquivZC_of_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) :
    @Continuous
      (ZCCompletedDifferentialModule C psi.toMonoidHom)
      (ZCFreeFoxCoordinates C (X := X) (H := H))
      (closedGeneratedDerivativeCoordinateTopologyProCInteger_of_fundamental_formula
        (G := G) (H := H) C psi family hfree htarget hφconv
        hH hφHconv hφHgen hfundamental)
      inferInstance
      (closedGeneratedDerivativeCoordinateLinearEquivProCInteger_of_fundamental_formula
        (G := G) (H := H) C psi family hfree htarget hφconv
        hH hφHconv hφHgen hfundamental)

The closed-generated coordinate equivalence is continuous for the transported coordinate topology on \(A_{\psi}(C)\).

Show Lean proof
Theorem CrowellExactSequence.t2Space_closedGenDerivativeCoordinateTopologyZC_of_fundFormula 
theorem t2Space_closedGenDerivativeCoordinateTopologyZC_of_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) :
    @T2Space
      (ZCCompletedDifferentialModule C psi.toMonoidHom)
      (closedGeneratedDerivativeCoordinateTopologyProCInteger_of_fundamental_formula
        (G := G) (H := H) C psi family hfree htarget hφconv
        hH hφHconv hφHgen hfundamental)

The coordinate topology transported to \(A_{\psi}(C)\) is Hausdorff.

Show Lean proof
Theorem CrowellExactSequence.continuous_closedGenDerivativeCoordinateLinearEquivZC_of_fundFormula_symm 
theorem continuous_closedGenDerivativeCoordinateLinearEquivZC_of_fundFormula_symm
    (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) :
    @Continuous
      (ZCFreeFoxCoordinates C (X := X) (H := H))
      (ZCCompletedDifferentialModule C psi.toMonoidHom)
      inferInstance
      (closedGeneratedDerivativeCoordinateTopologyProCInteger_of_fundamental_formula
        (G := G) (H := H) C psi family hfree htarget hφconv
        hH hφHconv hφHgen hfundamental)
        (closedGeneratedDerivativeCoordinateLinearEquivProCInteger_of_fundamental_formula
          (G := G) (H := H) C psi family hfree htarget hφconv
          hH hφHconv hφHgen hfundamental).symm

The inverse of the closed-generated coordinate equivalence is continuous for the transported coordinate topology on \(A_{\psi}(C)\). Equivalently, the displayed family map \(\mathbb{Z}_C\llbracket H\rrbracket^{X} \to A_{\psi}(C)\) is continuous for this topology.

Show Lean proof
Theorem CrowellExactSequence.continuous_presentedCompletedDifferentialFamilyMapZC_coordTopology_of_fundFormula 
theorem continuous_presentedCompletedDifferentialFamilyMapZC_coordTopology_of_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) :
    @Continuous
      (ZCFreeFoxCoordinates C (X := X) (H := H))
      (ZCCompletedDifferentialModule C psi.toMonoidHom)
      inferInstance
      (closedGeneratedDerivativeCoordinateTopologyProCInteger_of_fundamental_formula
        (G := G) (H := H) C psi family hfree htarget hφconv
        hH hφHconv hφHgen hfundamental)
        (presentedCompletedDifferentialFamilyMapProCInteger
          (G := G) (H := H) C psi family)

The displayed family map is continuous for the coordinate topology transported to \(A_{\psi}(C)\).

Show Lean proof
Theorem CrowellExactSequence.continuous_zcUniversalDifferential_coordinateTopology_of_fundamental_formula 
theorem continuous_zcUniversalDifferential_coordinateTopology_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) :
    @Continuous G
      (ZCCompletedDifferentialModule C psi.toMonoidHom)
      inferInstance
      (closedGeneratedDerivativeCoordinateTopologyProCInteger_of_fundamental_formula
        (G := G) (H := H) C psi family hfree htarget hφconv
        hH hφHconv hφHgen hfundamental)
        (fun g : G => zcUniversalDifferential C psi.toMonoidHom g)

The universal differential \(g \mapsto d(g)\) is continuous for the coordinate topology transported to \(A_{\psi}(C)\).

Show Lean proof
Theorem CrowellExactSequence.continuous_add_closedGenDerivativeCoordinateTopologyZC_of_fundFormula 
theorem continuous_add_closedGenDerivativeCoordinateTopologyZC_of_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) :
    letI : TopologicalSpace
        (ZCCompletedDifferentialModule C psi.toMonoidHom) :=
      closedGeneratedDerivativeCoordinateTopologyProCInteger_of_fundamental_formula
        (G := G) (H := H) C psi family hfree htarget hφconv
        hH hφHconv hφHgen hfundamental
    Continuous (fun p :
      ZCCompletedDifferentialModule C psi.toMonoidHom ×
        ZCCompletedDifferentialModule C psi.toMonoidHom =>
      p.1 + p.2)

Addition is continuous for the transported coordinate topology on \(A_{\psi}(C)\).

Show Lean proof
Theorem CrowellExactSequence.continuous_neg_closedGenDerivativeCoordinateTopologyZC_of_fundFormula 
theorem continuous_neg_closedGenDerivativeCoordinateTopologyZC_of_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) :
    letI : TopologicalSpace
        (ZCCompletedDifferentialModule C psi.toMonoidHom) :=
      closedGeneratedDerivativeCoordinateTopologyProCInteger_of_fundamental_formula
        (G := G) (H := H) C psi family hfree htarget hφconv
        hH hφHconv hφHgen hfundamental
    Continuous
      (fun a : ZCCompletedDifferentialModule C psi.toMonoidHom => -a)

Negation is continuous for the transported coordinate topology on \(A_{\psi}(C)\).

Show Lean proof
Theorem CrowellExactSequence.continuous_smul_closedGenDerivativeCoordinateTopologyZC_of_fundFormula 
theorem continuous_smul_closedGenDerivativeCoordinateTopologyZC_of_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) :
    letI : TopologicalSpace
        (ZCCompletedDifferentialModule C psi.toMonoidHom) :=
      closedGeneratedDerivativeCoordinateTopologyProCInteger_of_fundamental_formula
        (G := G) (H := H) C psi family hfree htarget hφconv
        hH hφHconv hφHgen hfundamental
    Continuous
      (fun p :
        ZCCompletedGroupAlgebra C H ×
          ZCCompletedDifferentialModule C psi.toMonoidHom =>
        p.1 • p.2)

Scalar multiplication is continuous for the transported coordinate topology on \(A_{\psi}(C)\).

Show Lean proof