Module

PresentedCoordinates.lean

Nyll.ProCGroups.FoxDifferential.Completed.Continuous.PresentedCoordinates

11 declarations indexed from sourceView source ↗

Module documentation

Fox differential: completed — continuous — presented coordinates

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\).

Imports3

Imported by2

def

presentedCompletedDifferentialFamilyMapProCInteger

L48 ↗

CrowellExactSequence.presentedCompletedDifferentialFamilyMapProCInteger

Documentation

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

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace CrowellExactSequence
noncomputable section
open scoped BigOperators
open FoxDifferential
universe u v w
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (C : ProCGroups.FiniteGroupClass.{u})

Lean source · statement

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

theorem

presentedCompletedDifferentialFamilyMapProCInteger_single

L63 ↗

CrowellExactSequence.presentedCompletedDifferentialFamilyMapProCInteger_single

Documentation

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

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace CrowellExactSequence
noncomputable section
open scoped BigOperators
open FoxDifferential
universe u v w
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (C : ProCGroups.FiniteGroupClass.{u})
omit [IsTopologicalGroup G] in

Lean source · statement

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)

def

presentedSeparatedDifferentialFamilyMapProCInteger

L75 ↗

CrowellExactSequence.presentedSeparatedDifferentialFamilyMapProCInteger

Documentation

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

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace CrowellExactSequence
noncomputable section
open scoped BigOperators
open FoxDifferential
universe u v w
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (C : ProCGroups.FiniteGroupClass.{u})

Lean source · statement

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

theorem

presentedSeparatedDifferentialFamilyMapProCInteger_single

L90 ↗

CrowellExactSequence.presentedSeparatedDifferentialFamilyMapProCInteger_single

Documentation

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

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace CrowellExactSequence
noncomputable section
open scoped BigOperators
open FoxDifferential
universe u v w
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (C : ProCGroups.FiniteGroupClass.{u})
omit [IsTopologicalGroup G] in

Lean source · statement

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)

theorem

zcSepDiffModuleStageProj_comp_presentedSepFamilyMap

L106 ↗

CrowellExactSequence.zcSepDiffModuleStageProj_comp_presentedSepFamilyMap

Documentation

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

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace CrowellExactSequence
noncomputable section
open scoped BigOperators
open FoxDifferential
universe u v w
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (C : ProCGroups.FiniteGroupClass.{u})
omit [IsTopologicalGroup G] in

Lean source · statement

theorem zcSepDiffModuleStageProj_comp_presentedSepFamilyMap
    (psi : ContinuousMonoidHom G H)
    {X : Type v} [Fintype 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)

theorem

continuous_presentedCompletedDifferentialFamilyMapProCInteger_naturalTopology

L130 ↗

CrowellExactSequence.continuous_presentedCompletedDifferentialFamilyMapProCInteger_naturalTopology

Documentation

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

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace CrowellExactSequence
noncomputable section
open scoped BigOperators
open FoxDifferential
universe u v w
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (C : ProCGroups.FiniteGroupClass.{u})
omit [IsTopologicalGroup G] in

Lean source · statement

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)

def

IsPresentedCompletedDifferentialFamilyBasisProCInteger

L196 ↗

CrowellExactSequence.IsPresentedCompletedDifferentialFamilyBasisProCInteger

Documentation

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

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace CrowellExactSequence
noncomputable section
open scoped BigOperators
open FoxDifferential
universe u v w
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (C : ProCGroups.FiniteGroupClass.{u})

Lean source · statement

def IsPresentedCompletedDifferentialFamilyBasisProCInteger
    (psi : ContinuousMonoidHom G H)
    {X : Type v} [Fintype X] (family : X -> G) : Prop

theorem

isPresentedCompletedDifferentialFamilyBasisProCInteger_reindex

L205 ↗

CrowellExactSequence.isPresentedCompletedDifferentialFamilyBasisProCInteger_reindex

Documentation

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

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace CrowellExactSequence
noncomputable section
open scoped BigOperators
open FoxDifferential
universe u v w
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (C : ProCGroups.FiniteGroupClass.{u})
omit [IsTopologicalGroup G] in

Lean source · full declaration

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)) := by
  classical
  dsimp [IsPresentedCompletedDifferentialFamilyBasisProCInteger]
  have hmap :
      presentedCompletedDifferentialFamilyMapProCInteger
          (G := G) (H := H) C psi (fun x : X => family (e x)) =
        (presentedCompletedDifferentialFamilyMapProCInteger
          (G := G) (H := H) C psi family).comp
          (piReindexLinearEquiv
            (R := ZCCompletedGroupAlgebra C H) e).toLinearMap := by
    simpa [presentedCompletedDifferentialFamilyMapProCInteger] using
      (finiteFamilyLinearMap_reindex
        (R := ZCCompletedGroupAlgebra C H)
        (M := ZCCompletedDifferentialModule C psi.toMonoidHom)
        e (fun y : Y => zcUniversalDifferential C psi.toMonoidHom (family y)))
  rw [hmap]
  exact hbasis_A.comp
    (piReindexLinearEquiv
      (R := ZCCompletedGroupAlgebra C H) e).bijective

def

presentedCompletedDifferentialFamilyCoordinatesProCInteger

L235 ↗

CrowellExactSequence.presentedCompletedDifferentialFamilyCoordinatesProCInteger

Documentation

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

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace CrowellExactSequence
noncomputable section
open scoped BigOperators
open FoxDifferential
universe u v w
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (C : ProCGroups.FiniteGroupClass.{u})

Lean source · statement

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)

theorem

presentedCompletedDifferentialFamilyCoordinatesProCInteger_symm_toLinearMap

L250 ↗

CrowellExactSequence.presentedCompletedDifferentialFamilyCoordinatesProCInteger_symm_toLinearMap

Documentation

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

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace CrowellExactSequence
noncomputable section
open scoped BigOperators
open FoxDifferential
universe u v w
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (C : ProCGroups.FiniteGroupClass.{u})
omit [IsTopologicalGroup G] in

Lean source · statement

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

theorem

presentedCompletedDifferentialFamilyCoordinatesProCInteger_d_family

L268 ↗

CrowellExactSequence.presentedCompletedDifferentialFamilyCoordinatesProCInteger_d_family

Documentation

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

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace CrowellExactSequence
noncomputable section
open scoped BigOperators
open FoxDifferential
universe u v w
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (C : ProCGroups.FiniteGroupClass.{u})
omit [IsTopologicalGroup G] in

Lean source · statement

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)

Module documentation

Fox differential: completed — continuous — presented coordinates

Declarations