Yamaguchi Lean 4 Library
ProCGroups.FoxDifferential.Completed.Continuous.PresentedCoordinates
ProCGroups/FoxDifferential/Completed/Continuous/PresentedCoordinates

ProCGroups.FoxDifferential.Completed.Continuous.PresentedCoordinates

7 Theorems | 4 Definitions

The principal declarations in this module are:

  • presentedCompletedDifferentialFamilyMapProCInteger The \(\mathbb{Z}_C\llbracket H\rrbracket\)-linear family map sending the standard coordinate vector \(e_i\) to d(family i). - presentedSeparatedDifferentialFamilyMapProCInteger The finite-family map into the separated completed differential module. - presentedCompletedDifferentialFamilyMapProCInteger_single The finite-family map sends the \(i\)-th standard coordinate vector to \(d(\mathrm{family}\ i)\). - presentedSeparatedDifferentialFamilyMapProCInteger_single The separated finite-family map sends the \(i\)-th standard coordinate vector to the separated differential of \(\mathrm{family}\ i\).
imports
Imported by

Declarations

Definition CrowellExactSequence.presentedCompletedDifferentialFamilyMapProCInteger 
def presentedCompletedDifferentialFamilyMapProCInteger
    (psi : ContinuousMonoidHom G H)
    {X : Type v} [Fintype X] (family : X -> G) :
    (X -> ZCCompletedGroupAlgebra C H) →ₗ[ZCCompletedGroupAlgebra C H]
      ZCCompletedDifferentialModule C psi.toMonoidHom :=
  finiteFamilyLinearMap
    (R := ZCCompletedGroupAlgebra C H)
    (fun i : X => zcUniversalDifferential C psi.toMonoidHom (family i))

The \(\mathbb{Z}_C\llbracket H\rrbracket\)-linear family map sending the standard coordinate vector \(e_i\) to d(family i).

Theorem CrowellExactSequence.presentedCompletedDifferentialFamilyMapProCInteger_single 
omit [IsTopologicalGroup G] in
@[simp]
theorem presentedCompletedDifferentialFamilyMapProCInteger_single
    (psi : ContinuousMonoidHom G H)
    {X : Type v} [Fintype X] [DecidableEq X] (family : X -> G) (i : X) :
    presentedCompletedDifferentialFamilyMapProCInteger
        (G := G) (H := H) C psi family (Pi.single i 1) =
      zcUniversalDifferential C psi.toMonoidHom (family i)

The finite-family map sends the \(i\)-th standard coordinate vector to \(d(\mathrm{family}\ i)\).

Show Lean proof
Definition CrowellExactSequence.presentedSeparatedDifferentialFamilyMapProCInteger 
def presentedSeparatedDifferentialFamilyMapProCInteger
    (psi : ContinuousMonoidHom G H)
    {X : Type v} [Fintype X] (family : X -> G) :
    ZCFreeFoxCoordinates C (X := X) (H := H) →ₗ[ZCCompletedGroupAlgebra C H]
      ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom :=
  finiteFamilyLinearMap
    (R := ZCCompletedGroupAlgebra C H)
    (fun i : X => zcSeparatedUniversalDifferential C psi.toMonoidHom (family i))

The finite-family map into the separated completed differential module.

Theorem CrowellExactSequence.presentedSeparatedDifferentialFamilyMapProCInteger_single 
omit [IsTopologicalGroup G] in
@[simp]
theorem presentedSeparatedDifferentialFamilyMapProCInteger_single
    (psi : ContinuousMonoidHom G H)
    {X : Type v} [Fintype X] [DecidableEq X] (family : X -> G) (i : X) :
    presentedSeparatedDifferentialFamilyMapProCInteger
        (G := G) (H := H) C psi family (Pi.single i 1) =
      zcSeparatedUniversalDifferential C psi.toMonoidHom (family i)

The separated finite-family map sends the \(i\)-th standard coordinate vector to the separated differential of \(\mathrm{family}\ i\).

Show Lean proof
Theorem CrowellExactSequence.zcSepDiffModuleStageProj_comp_presentedSepFamilyMap 
omit [IsTopologicalGroup G] in
theorem zcSepDiffModuleStageProj_comp_presentedSepFamilyMap
    (psi : ContinuousMonoidHom G H)
    {X : Type v} [Fintype X] [DecidableEq X] (family : X -> G)
    (i : ZCCompletedDifferentialModuleIndex C psi.toMonoidHom) :
    (zcSeparatedCompletedDifferentialModuleStageProjectionAdd C psi.toMonoidHom i).comp
        (presentedSeparatedDifferentialFamilyMapProCInteger
          (G := G) (H := H) C psi family) =
      (zcCompletedDifferentialModuleStageProjection C psi.toMonoidHom i).comp
        (presentedCompletedDifferentialFamilyMapProCInteger
          (G := G) (H := H) C psi family)

Projecting the separated finite-family map to a finite stage agrees with projecting the algebraic finite-family map to the same finite stage.

Show Lean proof
Theorem CrowellExactSequence.continuous_presentedCompletedDifferentialFamilyMapProCInteger_naturalTopology 
omit [IsTopologicalGroup G] in
theorem continuous_presentedCompletedDifferentialFamilyMapProCInteger_naturalTopology
    (psi : ContinuousMonoidHom G H)
    {X : Type v} [Fintype X] (family : X -> G) :
    @Continuous
      (ZCFreeFoxCoordinates C (X := X) (H := H))
      (ZCCompletedDifferentialModule C psi.toMonoidHom)
      inferInstance
      (zcCompletedDifferentialModuleNaturalTopology C psi.toMonoidHom)
      (presentedCompletedDifferentialFamilyMapProCInteger
        (G := G) (H := H) C psi family)

The finite-family map into \(A_{\psi}(C)\) is continuous for the finite-stage completed topology on \(A_{\psi}(C)\).

Show Lean proof
Definition CrowellExactSequence.IsPresentedCompletedDifferentialFamilyBasisProCInteger 
def IsPresentedCompletedDifferentialFamilyBasisProCInteger
    (psi : ContinuousMonoidHom G H)
    {X : Type v} [Fintype X] (family : X -> G) : Prop :=
  Function.Bijective
    (presentedCompletedDifferentialFamilyMapProCInteger
      (G := G) (H := H) C psi family)

The basis property for a finite family in the Fox completed differential module.

Theorem CrowellExactSequence.isPresentedCompletedDifferentialFamilyBasisProCInteger_reindex 
omit [IsTopologicalGroup G] in
theorem isPresentedCompletedDifferentialFamilyBasisProCInteger_reindex
    (psi : ContinuousMonoidHom G H)
    {X : Type v} [Fintype X]
    {Y : Type w} [Fintype Y]
    (e : X ≃ Y) (family : Y -> G)
    (hbasis_A :
      IsPresentedCompletedDifferentialFamilyBasisProCInteger
        (G := G) (H := H) C psi family) :
    IsPresentedCompletedDifferentialFamilyBasisProCInteger
      (G := G) (H := H) C psi (fun x : X => family (e x))

The completed differential basis property is invariant under reindexing a finite family.

Show Lean proof
Definition CrowellExactSequence.presentedCompletedDifferentialFamilyCoordinatesProCInteger 
def presentedCompletedDifferentialFamilyCoordinatesProCInteger
    (psi : ContinuousMonoidHom G H)
    {X : Type v} [Fintype X] (family : X -> G)
    (hbasis_A :
      IsPresentedCompletedDifferentialFamilyBasisProCInteger
        (G := G) (H := H) C psi family) :
    ZCCompletedDifferentialModule C psi.toMonoidHom ≃ₗ[ZCCompletedGroupAlgebra C H]
      (X -> ZCCompletedGroupAlgebra C H) :=
  (LinearEquiv.ofBijective
    (presentedCompletedDifferentialFamilyMapProCInteger
      (G := G) (H := H) C psi family)
    hbasis_A).symm

Coordinates associated to a basis family in \(A_{\psi}(C)\).

Theorem CrowellExactSequence.presentedCompletedDifferentialFamilyCoordinatesProCInteger_symm_toLinearMap 
omit [IsTopologicalGroup G] in
theorem presentedCompletedDifferentialFamilyCoordinatesProCInteger_symm_toLinearMap
    (psi : ContinuousMonoidHom G H)
    {X : Type v} [Fintype X] (family : X -> G)
    (hbasis_A :
      IsPresentedCompletedDifferentialFamilyBasisProCInteger
        (G := G) (H := H) C psi family) :
    (presentedCompletedDifferentialFamilyCoordinatesProCInteger
      (G := G) (H := H) C psi family hbasis_A).symm.toLinearMap =
      presentedCompletedDifferentialFamilyMapProCInteger
        (G := G) (H := H) C psi family

The inverse coordinate equivalence has underlying linear map equal to the finite-family map.

Show Lean proof
Theorem CrowellExactSequence.presentedCompletedDifferentialFamilyCoordinatesProCInteger_d_family 
omit [IsTopologicalGroup G] in
@[simp 900]
theorem presentedCompletedDifferentialFamilyCoordinatesProCInteger_d_family
    (psi : ContinuousMonoidHom G H)
    {X : Type v} [Fintype X] [DecidableEq X] (family : X -> G)
    (hbasis_A :
      IsPresentedCompletedDifferentialFamilyBasisProCInteger
        (G := G) (H := H) C psi family) (i : X) :
    presentedCompletedDifferentialFamilyCoordinatesProCInteger
        (G := G) (H := H) C psi family hbasis_A
        (zcUniversalDifferential C psi.toMonoidHom (family i)) =
      Pi.single i (1 : ZCCompletedGroupAlgebra C H)

The coordinate equivalence sends \(d(\mathrm{family}\ i)\) to the \(i\)-th standard coordinate vector.

Show Lean proof