Module

FiniteStage.lean

Nyll.ProCGroups.FoxDifferential.Completed.Continuous.Universal.FiniteStage

84 declarations indexed from sourceView source ↗

Module documentation

Fox differential: completed — continuous — universal — finite stage

The principal declarations in this module are:

ZCCompletedDifferentialModuleIndex

A finite stage for the completed universal differential module. It consists of a finite source quotient \(G/V\), a coefficient-and-target stage \((\mathbb{Z}/n\mathbb{Z})[H/U]\) of \(\mathbb{Z}_C\llbracket H\rrbracket\), and the compatibility \(\psi(V)\leq U\) needed to descend \(\psi\) to \(G/V\to H/U\).

zcCompletedDifferentialModuleComapIndex

The finite stage whose source quotient is the pullback of a target finite quotient along a continuous homomorphism.

le_def

The order on completed differential-module indices is the simultaneous refinement order on source, target, and coefficient stages.

nonempty_zcCompletedDifferentialModuleIndex

The finite-stage index type is nonempty for a continuous homomorphism: take the pullback of the terminal completed group-algebra target stage.

Imports2

Imported by3

structure

ZCCompletedDifferentialModuleIndex

L51 ↗

FoxDifferential.ZCCompletedDifferentialModuleIndex

Documentation

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · full declaration

structure ZCCompletedDifferentialModuleIndex (ψ : G →* H) where
  /-- The open-normal source subgroup defining the finite quotient of \(G\). -/
  source : OpenNormalSubgroupInClass C G
  /-- The coefficient-and-target stage of the completed group algebra of \(H\). -/
  target : ZCCompletedGroupAlgebraIndex C H
  /-- The source subgroup maps into the target subgroup, so \(\psi\) descends to the quotients. -/
  compatible :
    (source.1 : Subgroup G) ≤
      ((OrderDual.ofDual target.2).1 : Subgroup H).comap ψ

instance

instLE

L70 ↗

FoxDifferential.ZCCompletedDifferentialModuleIndex.instLE

Documentation

Completed differential-module indices order source subgroups contravariantly and target stages covariantly.

Source context 12 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
namespace ZCCompletedDifferentialModuleIndex
variable {C}
variable {ψ : G →* H}

Lean source · full declaration

instance instLE : LE (ZCCompletedDifferentialModuleIndex C ψ) where
  le i j :=
    (j.source.1 : Subgroup G) ≤ (i.source.1 : Subgroup G) ∧ i.target ≤ j.target

instance

instPreorder

L75 ↗

FoxDifferential.ZCCompletedDifferentialModuleIndex.instPreorder

Documentation

The simultaneous source-and-target refinement relation defines a preorder on stage indices.

Source context 12 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
namespace ZCCompletedDifferentialModuleIndex
variable {C}
variable {ψ : G →* H}

Lean source · full declaration

instance instPreorder : Preorder (ZCCompletedDifferentialModuleIndex C ψ) where
  le := (· ≤ ·)
  le_refl i := ⟨le_rfl, le_rfl⟩
  le_trans i j k hij hjk :=
    ⟨hjk.1.trans hij.1, hij.2.trans hjk.2⟩

theorem

le_def

L87 ↗

FoxDifferential.ZCCompletedDifferentialModuleIndex.le_def

Documentation

The order on completed differential-module indices is the simultaneous refinement order on source, target, and coefficient stages.

Source context 13 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
namespace ZCCompletedDifferentialModuleIndex
variable {C}
variable {ψ : G →* H}
omit [IsTopologicalGroup G] [IsTopologicalGroup H] in

Lean source · statement

theorem le_def {i j : ZCCompletedDifferentialModuleIndex C ψ} :
    i ≤ j ↔
      (j.source.1 : Subgroup G) ≤ (i.source.1 : Subgroup G) ∧ i.target ≤ j.target

def

zcCompletedDifferentialModuleComapIndex

L100 ↗

FoxDifferential.zcCompletedDifferentialModuleComapIndex

Documentation

The finite stage whose source quotient is the pullback of a target finite quotient along a continuous homomorphism.

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (ψ : G →* H)

Lean source · full declaration

def zcCompletedDifferentialModuleComapIndex
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (ψc : ContinuousMonoidHom G H)
    (i : ZCCompletedGroupAlgebraIndex C H) :
    ZCCompletedDifferentialModuleIndex C ψc.toMonoidHom where
  source := OrderDual.ofDual
    (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hC ψc i.2)
  target := i
  compatible := by
    intro g hg
    change ψc.toMonoidHom g ∈
      ((((OrderDual.ofDual i.2).1 : OpenNormalSubgroup H) : Subgroup H))
    simpa [completedGroupAlgebraComapIndexInClass] using hg

theorem

nonempty_zcCompletedDifferentialModuleIndex

L119 ↗

FoxDifferential.nonempty_zcCompletedDifferentialModuleIndex

Documentation

The finite-stage index type is nonempty for a continuous homomorphism: take the pullback of the terminal completed group-algebra target stage.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (ψ : G →* H)
omit [IsTopologicalGroup G] in

Lean source · statement

theorem nonempty_zcCompletedDifferentialModuleIndex
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (ψc : ContinuousMonoidHom G H) :
    Nonempty (ZCCompletedDifferentialModuleIndex C ψc.toMonoidHom)

theorem

directed_zcCompletedDifferentialModuleIndex

L134 ↗

FoxDifferential.directed_zcCompletedDifferentialModuleIndex

Documentation

The compatible finite source/target/coefficient stages are directed for a continuous homomorphism, provided the finite quotient class is closed under the usual formation and hereditary operations.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (ψ : G →* H)
omit [IsTopologicalGroup G] in

Lean source · statement

theorem directed_zcCompletedDifferentialModuleIndex
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
    (ψc : ContinuousMonoidHom G H) :
    Directed (· ≤ ·)
      (id : ZCCompletedDifferentialModuleIndex C ψc.toMonoidHom →
        ZCCompletedDifferentialModuleIndex C ψc.toMonoidHom)

abbrev

zcCompletedDifferentialModuleStageSource

L180 ↗

FoxDifferential.zcCompletedDifferentialModuleStageSource

Documentation

The source quotient \(G/V\) at one finite differential-module stage.

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (ψ : G →* H)

Lean source · statement

abbrev zcCompletedDifferentialModuleStageSource
    (i : ZCCompletedDifferentialModuleIndex C ψ) : Type u

abbrev

zcCompletedDifferentialModuleStageTarget

L185 ↗

FoxDifferential.zcCompletedDifferentialModuleStageTarget

Documentation

The target finite quotient \(H/U\) underlying the group-algebra stage.

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (ψ : G →* H)

Lean source · statement

abbrev zcCompletedDifferentialModuleStageTarget
    (i : ZCCompletedDifferentialModuleIndex C ψ) : Type u

abbrev

zcCompletedDifferentialModuleStageRing

L193 ↗

FoxDifferential.zcCompletedDifferentialModuleStageRing

Documentation

The finite coefficient ring \((\mathbb{Z}/n\mathbb{Z})[H/U]\) acting on one finite differential-module stage.

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (ψ : G →* H)

Lean source · statement

abbrev zcCompletedDifferentialModuleStageRing
    (i : ZCCompletedDifferentialModuleIndex C ψ) : Type u

def

zcCompletedDifferentialModuleStagePsi

L198 ↗

FoxDifferential.zcCompletedDifferentialModuleStagePsi

Documentation

The target map \(G/V \to H/U\) induced by \(\psi\) at a compatible finite stage.

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (ψ : G →* H)

Lean source · statement

def zcCompletedDifferentialModuleStagePsi
    (i : ZCCompletedDifferentialModuleIndex C ψ) :
    zcCompletedDifferentialModuleStageSource C ψ i →*
      zcCompletedDifferentialModuleStageTarget C ψ i

def

zcCompletedDifferentialModuleStageScalar

L208 ↗

FoxDifferential.zcCompletedDifferentialModuleStageScalar

Documentation

The stage coefficient homomorphism \(G/V \to (\mathbb{Z}/n\mathbb{Z})[H/U]\).

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (ψ : G →* H)

Lean source · statement

def zcCompletedDifferentialModuleStageScalar
    (i : ZCCompletedDifferentialModuleIndex C ψ) :
    zcCompletedDifferentialModuleStageSource C ψ i →*
      zcCompletedDifferentialModuleStageRing C ψ i

abbrev

ZCCompletedDifferentialModuleStage

L217 ↗

FoxDifferential.ZCCompletedDifferentialModuleStage

Documentation

The finite crossed-differential module at one source/target/coefficient stage.

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (ψ : G →* H)

Lean source · statement

abbrev ZCCompletedDifferentialModuleStage
    (i : ZCCompletedDifferentialModuleIndex C ψ) : Type u

instance

instTopologicalSpaceZCCompletedDifferentialModuleStage

L222 ↗

FoxDifferential.instTopologicalSpaceZCCompletedDifferentialModuleStage

Documentation

Finite completed differential-module stages carry the discrete topology.

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (ψ : G →* H)

Lean source · statement

instance instTopologicalSpaceZCCompletedDifferentialModuleStage
    (i : ZCCompletedDifferentialModuleIndex C ψ) :
    TopologicalSpace (ZCCompletedDifferentialModuleStage C ψ i)

instance

instDiscreteTopologyZCCompletedDifferentialModuleStage

L228 ↗

FoxDifferential.instDiscreteTopologyZCCompletedDifferentialModuleStage

Documentation

Finite completed differential-module stages carry the discrete topology.

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (ψ : G →* H)

Lean source · statement

instance instDiscreteTopologyZCCompletedDifferentialModuleStage
    (i : ZCCompletedDifferentialModuleIndex C ψ) :
    DiscreteTopology (ZCCompletedDifferentialModuleStage C ψ i)

instance

instT2SpaceZCCompletedDifferentialModuleStage

L234 ↗

FoxDifferential.instT2SpaceZCCompletedDifferentialModuleStage

Documentation

Finite completed differential-module stages are Hausdorff.

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (ψ : G →* H)

Lean source · statement

instance instT2SpaceZCCompletedDifferentialModuleStage
    (i : ZCCompletedDifferentialModuleIndex C ψ) :
    T2Space (ZCCompletedDifferentialModuleStage C ψ i)

instance

instIsTopologicalAddGroupZCCompletedDifferentialModuleStage

L240 ↗

FoxDifferential.instIsTopologicalAddGroupZCCompletedDifferentialModuleStage

Documentation

Finite completed differential-module stages are topological additive groups.

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (ψ : G →* H)

Lean source · statement

instance instIsTopologicalAddGroupZCCompletedDifferentialModuleStage
    (i : ZCCompletedDifferentialModuleIndex C ψ) :
    IsTopologicalAddGroup (ZCCompletedDifferentialModuleStage C ψ i)

instance

instModuleZCCompletedGroupAlgebraZCCompletedDifferentialModuleStage

L249 ↗

FoxDifferential.instModuleZCCompletedGroupAlgebraZCCompletedDifferentialModuleStage

Documentation

The completed differential-module stage is a module over the corresponding \(\mathbb{Z}_C\)-completed group-algebra stage.

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (ψ : G →* H)

Lean source · statement

instance instModuleZCCompletedGroupAlgebraZCCompletedDifferentialModuleStage
    (i : ZCCompletedDifferentialModuleIndex C ψ) :
    Module (ZCCompletedGroupAlgebra C H) (ZCCompletedDifferentialModuleStage C ψ i)

def

zcCompletedDifferentialModuleStageSourceProj

L255 ↗

FoxDifferential.zcCompletedDifferentialModuleStageSourceProj

Documentation

The quotient map from the source group into a finite differential-module stage source.

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (ψ : G →* H)

Lean source · statement

def zcCompletedDifferentialModuleStageSourceProj
    (i : ZCCompletedDifferentialModuleIndex C ψ) :
    G →* zcCompletedDifferentialModuleStageSource C ψ i

theorem

zcCompletedDifferentialModuleStageSourceProj_apply

L266 ↗

FoxDifferential.zcCompletedDifferentialModuleStageSourceProj_apply

Documentation

The finite-stage source projection is the quotient map by the source subgroup of the differential-module stage.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (ψ : G →* H)
omit [IsTopologicalGroup G] [IsTopologicalGroup H] in

Lean source · statement

theorem zcCompletedDifferentialModuleStageSourceProj_apply
    (i : ZCCompletedDifferentialModuleIndex C ψ) (g : G) :
    zcCompletedDifferentialModuleStageSourceProj C ψ i g =
      QuotientGroup.mk' (i.source.1 : Subgroup G) g

theorem

zcCompletedDifferentialModuleStagePsi_mk

L278 ↗

FoxDifferential.zcCompletedDifferentialModuleStagePsi_mk

Documentation

The finite-stage \(\psi\)-map for the \(\mathbb{Z}_C\)-completed differential module is the coordinate map determined by the source projection.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (ψ : G →* H)
omit [IsTopologicalGroup G] in

Lean source · statement

theorem zcCompletedDifferentialModuleStagePsi_mk
    (i : ZCCompletedDifferentialModuleIndex C ψ) (g : G) :
    zcCompletedDifferentialModuleStagePsi C ψ i
        (QuotientGroup.mk' (i.source.1 : Subgroup G) g) =
      QuotientGroup.mk' ((OrderDual.ofDual i.target.2).1 : Subgroup H) (ψ g)

theorem

zcCompletedDifferentialModuleStageScalar_mk

L291 ↗

FoxDifferential.zcCompletedDifferentialModuleStageScalar_mk

Documentation

The scalar structure on the \(\mathbb{Z}_C\)-completed differential-module stage is computed by the finite-stage scalar action.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (ψ : G →* H)
omit [IsTopologicalGroup G] in

Lean source · statement

theorem zcCompletedDifferentialModuleStageScalar_mk
    (i : ZCCompletedDifferentialModuleIndex C ψ) (g : G) :
    zcCompletedDifferentialModuleStageScalar C ψ i
        (QuotientGroup.mk' (i.source.1 : Subgroup G) g) =
      MonoidAlgebra.of (ModNCompletedCoeff i.target.1.modulus)
        (zcCompletedDifferentialModuleStageTarget C ψ i)
        (QuotientGroup.mk' ((OrderDual.ofDual i.target.2).1 : Subgroup H) (ψ g))

theorem

zcCompletedDifferentialModuleStagePsi_coe

L306 ↗

FoxDifferential.zcCompletedDifferentialModuleStagePsi_coe

Documentation

The finite-stage \(\psi\)-map for the \(\mathbb{Z}_C\)-completed differential module is the coordinate map determined by the source projection.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (ψ : G →* H)
omit [IsTopologicalGroup G] in

Lean source · statement

theorem zcCompletedDifferentialModuleStagePsi_coe
    (i : ZCCompletedDifferentialModuleIndex C ψ) (g : G) :
    zcCompletedDifferentialModuleStagePsi C ψ i
        (QuotientGroup.mk g : zcCompletedDifferentialModuleStageSource C ψ i) =
      (QuotientGroup.mk (ψ g) : zcCompletedDifferentialModuleStageTarget C ψ i)

theorem

zcCompletedDifferentialModuleStageScalar_coe

L319 ↗

FoxDifferential.zcCompletedDifferentialModuleStageScalar_coe

Documentation

The scalar structure on the \(\mathbb{Z}_C\)-completed differential-module stage is computed by the finite-stage scalar action.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (ψ : G →* H)
omit [IsTopologicalGroup G] in

Lean source · statement

theorem zcCompletedDifferentialModuleStageScalar_coe
    (i : ZCCompletedDifferentialModuleIndex C ψ) (g : G) :
    zcCompletedDifferentialModuleStageScalar C ψ i
        (QuotientGroup.mk g : zcCompletedDifferentialModuleStageSource C ψ i) =
      MonoidAlgebra.of (ModNCompletedCoeff i.target.1.modulus)
        (zcCompletedDifferentialModuleStageTarget C ψ i)
        (QuotientGroup.mk (ψ g) : zcCompletedDifferentialModuleStageTarget C ψ i)

theorem

zcCompletedDifferentialModuleStagePsi_sourceProj

L334 ↗

FoxDifferential.zcCompletedDifferentialModuleStagePsi_sourceProj

Documentation

The finite-stage \(\psi\)-map for the \(\mathbb{Z}_C\)-completed differential module is the coordinate map determined by the source projection.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (ψ : G →* H)
omit [IsTopologicalGroup G] in

Lean source · statement

theorem zcCompletedDifferentialModuleStagePsi_sourceProj
    (i : ZCCompletedDifferentialModuleIndex C ψ) (g : G) :
    zcCompletedDifferentialModuleStagePsi C ψ i
        (zcCompletedDifferentialModuleStageSourceProj C ψ i g) =
      QuotientGroup.mk' ((OrderDual.ofDual i.target.2).1 : Subgroup H) (ψ g)

theorem

zcCompletedDifferentialModuleStageScalar_sourceProj

L349 ↗

FoxDifferential.zcCompletedDifferentialModuleStageScalar_sourceProj

Documentation

The scalar structure on the \(\mathbb{Z}_C\)-completed differential-module stage is computed by the finite-stage scalar action.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (ψ : G →* H)
omit [IsTopologicalGroup G] in

Lean source · statement

theorem zcCompletedDifferentialModuleStageScalar_sourceProj
    (i : ZCCompletedDifferentialModuleIndex C ψ) (g : G) :
    zcCompletedDifferentialModuleStageScalar C ψ i
        (zcCompletedDifferentialModuleStageSourceProj C ψ i g) =
      MonoidAlgebra.of (ModNCompletedCoeff i.target.1.modulus)
        (zcCompletedDifferentialModuleStageTarget C ψ i)
        (QuotientGroup.mk' ((OrderDual.ofDual i.target.2).1 : Subgroup H) (ψ g))

def

zcCompletedDifferentialModuleIdentitySourceIndex

L363 ↗

FoxDifferential.zcCompletedDifferentialModuleIdentitySourceIndex

Documentation

The source-identity finite stage attached to a \(\psi\)-stage. It has the same source quotient and coefficient modulus, and its target quotient is the same source quotient.

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (ψ : G →* H)

Lean source · full declaration

def zcCompletedDifferentialModuleIdentitySourceIndex
    (i : ZCCompletedDifferentialModuleIndex C ψ) :
    ZCCompletedDifferentialModuleIndex C (MonoidHom.id G) where
  source := i.source
  target := (i.target.1, OrderDual.toDual i.source)
  compatible := by
    intro g hg
    simpa using hg

theorem

zcCompletedDifferentialModuleIdentitySourceIndex_source

L375 ↗

FoxDifferential.zcCompletedDifferentialModuleIdentitySourceIndex_source

Documentation

The identity-source index associated to i has the same source quotient as i.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (ψ : G →* H)
omit [IsTopologicalGroup G] [IsTopologicalGroup H] in

Lean source · statement

theorem zcCompletedDifferentialModuleIdentitySourceIndex_source
    (i : ZCCompletedDifferentialModuleIndex C ψ) :
    (zcCompletedDifferentialModuleIdentitySourceIndex C ψ i).source = i.source

theorem

zcCompletedDifferentialModuleIdentitySourceIndex_target_fst

L383 ↗

FoxDifferential.zcCompletedDifferentialModuleIdentitySourceIndex_target_fst

Documentation

The identity-source index associated to i retains the coefficient component of i.target.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (ψ : G →* H)
omit [IsTopologicalGroup G] [IsTopologicalGroup H] in

Lean source · statement

theorem zcCompletedDifferentialModuleIdentitySourceIndex_target_fst
    (i : ZCCompletedDifferentialModuleIndex C ψ) :
    (zcCompletedDifferentialModuleIdentitySourceIndex C ψ i).target.1 = i.target.1

theorem

zcCompletedDifferentialModuleStageSourceProj_identitySourceIndex

L394 ↗

FoxDifferential.zcCompletedDifferentialModuleStageSourceProj_identitySourceIndex

Documentation

At an identity-source index, the source projection for MonoidHom.id G agrees with the source projection for ψ.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (ψ : G →* H)
omit [IsTopologicalGroup G] [IsTopologicalGroup H] in

Lean source · statement

theorem zcCompletedDifferentialModuleStageSourceProj_identitySourceIndex
    (i : ZCCompletedDifferentialModuleIndex C ψ) (g : G) :
    zcCompletedDifferentialModuleStageSourceProj C (MonoidHom.id G)
        (zcCompletedDifferentialModuleIdentitySourceIndex C ψ i) g =
      zcCompletedDifferentialModuleStageSourceProj C ψ i g

theorem

zcCompletedDifferentialModuleStagePsi_identitySourceIndex_sourceProj

L404 ↗

FoxDifferential.zcCompletedDifferentialModuleStagePsi_identitySourceIndex_sourceProj

Documentation

The identity-stage map fixes every element obtained from the original source projection.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (ψ : G →* H)
omit [IsTopologicalGroup H] in

Lean source · statement

theorem zcCompletedDifferentialModuleStagePsi_identitySourceIndex_sourceProj
    (i : ZCCompletedDifferentialModuleIndex C ψ) (g : G) :
    zcCompletedDifferentialModuleStagePsi C (MonoidHom.id G)
        (zcCompletedDifferentialModuleIdentitySourceIndex C ψ i)
        (zcCompletedDifferentialModuleStageSourceProj C ψ i g) =
      zcCompletedDifferentialModuleStageSourceProj C ψ i g

theorem

zcCompletedDifferentialModuleStageScalar_identitySourceIndex_sourceProj

L418 ↗

FoxDifferential.zcCompletedDifferentialModuleStageScalar_identitySourceIndex_sourceProj

Documentation

At the identity-source index, the scalar attached to a projected source element is the corresponding group-like basis element.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (ψ : G →* H)
omit [IsTopologicalGroup H] in

Lean source · statement

theorem zcCompletedDifferentialModuleStageScalar_identitySourceIndex_sourceProj
    (i : ZCCompletedDifferentialModuleIndex C ψ) (g : G) :
    zcCompletedDifferentialModuleStageScalar C (MonoidHom.id G)
        (zcCompletedDifferentialModuleIdentitySourceIndex C ψ i)
        (zcCompletedDifferentialModuleStageSourceProj C ψ i g) =
      MonoidAlgebra.of (ModNCompletedCoeff i.target.1.modulus)
        (zcCompletedDifferentialModuleStageSource C ψ i)
        (zcCompletedDifferentialModuleStageSourceProj C ψ i g)

def

zcCompletedDifferentialModuleIdentitySourceStageRingHom

L432 ↗

FoxDifferential.zcCompletedDifferentialModuleIdentitySourceStageRingHom

Documentation

The finite group-algebra map from the source-identity stage attached to \(i\) to the \(\psi\)-stage \(i\), induced by the finite target map \(G/V \to H/U\).

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (ψ : G →* H)

Lean source · statement

def zcCompletedDifferentialModuleIdentitySourceStageRingHom
    (i : ZCCompletedDifferentialModuleIndex C ψ) :
    RingHom
      (zcCompletedDifferentialModuleStageRing C (MonoidHom.id G)
        (zcCompletedDifferentialModuleIdentitySourceIndex C ψ i))
      (zcCompletedDifferentialModuleStageRing C ψ i)

theorem

zcCompletedDifferentialModuleIdentitySourceStageRingHom_stageScalar

L446 ↗

FoxDifferential.zcCompletedDifferentialModuleIdentitySourceStageRingHom_stageScalar

Documentation

The identity-source stage ring homomorphism sends the identity-stage scalar of q to the scalar of q at the original stage.

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (ψ : G →* H)

Lean source · statement

theorem zcCompletedDifferentialModuleIdentitySourceStageRingHom_stageScalar
    (i : ZCCompletedDifferentialModuleIndex C ψ)
    (q : zcCompletedDifferentialModuleStageSource C ψ i) :
    zcCompletedDifferentialModuleIdentitySourceStageRingHom C ψ i
        (zcCompletedDifferentialModuleStageScalar C (MonoidHom.id G)
          (zcCompletedDifferentialModuleIdentitySourceIndex C ψ i) q) =
      zcCompletedDifferentialModuleStageScalar C ψ i q

def

zcCompletedDifferentialModuleIdentitySourceStageToStageCrossedHom

L471 ↗

FoxDifferential.zcCompletedDifferentialModuleIdentitySourceStageToStageCrossedHom

Documentation

The universal differential on a \(\psi\)-stage, bundled for the source-identity stage scalars after restriction along the finite-stage ring map.

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (ψ : G →* H)

Lean source · full declaration

def zcCompletedDifferentialModuleIdentitySourceStageToStageCrossedHom
    (i : ZCCompletedDifferentialModuleIndex C ψ) :
    letI : Module
        (zcCompletedDifferentialModuleStageRing C (MonoidHom.id G)
          (zcCompletedDifferentialModuleIdentitySourceIndex C ψ i))
        (ZCCompletedDifferentialModuleStage C ψ i) :=
      Module.compHom _ (zcCompletedDifferentialModuleIdentitySourceStageRingHom C ψ i)
    ScalarCrossedHom
      (zcCompletedDifferentialModuleStageScalar C (MonoidHom.id G)
        (zcCompletedDifferentialModuleIdentitySourceIndex C ψ i))
      (ZCCompletedDifferentialModuleStage C ψ i) := by
  letI : Module
      (zcCompletedDifferentialModuleStageRing C (MonoidHom.id G)
        (zcCompletedDifferentialModuleIdentitySourceIndex C ψ i))
      (ZCCompletedDifferentialModuleStage C ψ i) :=
    Module.compHom _ (zcCompletedDifferentialModuleIdentitySourceStageRingHom C ψ i)
  exact
    { toFun := fun q =>
        universalCrossedDifferential
          (zcCompletedDifferentialModuleStageScalar C ψ i) q
      map_mul' := by
        intro q r
        dsimp only [zcCompletedDifferentialModuleIdentitySourceIndex] at q r ⊢
        change
          universalCrossedDifferential
                (zcCompletedDifferentialModuleStageScalar C ψ i) (q * r) =
            universalCrossedDifferential
                (zcCompletedDifferentialModuleStageScalar C ψ i) q +
              zcCompletedDifferentialModuleStageScalar C (MonoidHom.id G)
                (zcCompletedDifferentialModuleIdentitySourceIndex C ψ i) q •
                universalCrossedDifferential
                  (zcCompletedDifferentialModuleStageScalar C ψ i) r
        rw [universalCrossedDifferential_mul]
        congr 1
        symm
        change
          zcCompletedDifferentialModuleIdentitySourceStageRingHom C ψ i
              (zcCompletedDifferentialModuleStageScalar C (MonoidHom.id G)
                (zcCompletedDifferentialModuleIdentitySourceIndex C ψ i) q) •
              universalCrossedDifferential
                (zcCompletedDifferentialModuleStageScalar C ψ i) r =
            zcCompletedDifferentialModuleStageScalar C ψ i q •
              universalCrossedDifferential
                (zcCompletedDifferentialModuleStageScalar C ψ i) r
        rw [zcCompletedDifferentialModuleIdentitySourceStageRingHom_stageScalar] }

def

zcCompletedDifferentialModuleIdentitySourceStageToStage

L521 ↗

FoxDifferential.zcCompletedDifferentialModuleIdentitySourceStageToStage

Documentation

The finite-stage comparison from the source-identity stage attached to i to the \(\psi\)-stage i, sending d q to d q.

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (ψ : G →* H)

Lean source · full declaration

def zcCompletedDifferentialModuleIdentitySourceStageToStage
    (i : ZCCompletedDifferentialModuleIndex C ψ) :
    letI : Module
        (zcCompletedDifferentialModuleStageRing C (MonoidHom.id G)
          (zcCompletedDifferentialModuleIdentitySourceIndex C ψ i))
        (ZCCompletedDifferentialModuleStage C ψ i) :=
      Module.compHom _ (zcCompletedDifferentialModuleIdentitySourceStageRingHom C ψ i)
    ZCCompletedDifferentialModuleStage C (MonoidHom.id G)
        (zcCompletedDifferentialModuleIdentitySourceIndex C ψ i) →ₗ[
      zcCompletedDifferentialModuleStageRing C (MonoidHom.id G)
        (zcCompletedDifferentialModuleIdentitySourceIndex C ψ i)]
      ZCCompletedDifferentialModuleStage C ψ i := by
  letI : Module
      (zcCompletedDifferentialModuleStageRing C (MonoidHom.id G)
        (zcCompletedDifferentialModuleIdentitySourceIndex C ψ i))
      (ZCCompletedDifferentialModuleStage C ψ i) :=
    Module.compHom _ (zcCompletedDifferentialModuleIdentitySourceStageRingHom C ψ i)
  exact crossedHomModuleLift
    (A := ZCCompletedDifferentialModuleStage C ψ i)
    (zcCompletedDifferentialModuleStageScalar C (MonoidHom.id G)
      (zcCompletedDifferentialModuleIdentitySourceIndex C ψ i))
    (zcCompletedDifferentialModuleIdentitySourceStageToStageCrossedHom C ψ i)

theorem

zcCompletedDifferentialModuleIdentitySourceStageToStage_universal

L549 ↗

FoxDifferential.zcCompletedDifferentialModuleIdentitySourceStageToStage_universal

Documentation

The comparison from the identity-source stage carries the universal crossed differential of q to the universal crossed differential at the original stage.

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (ψ : G →* H)

Lean source · statement

theorem zcCompletedDifferentialModuleIdentitySourceStageToStage_universal
    (i : ZCCompletedDifferentialModuleIndex C ψ)
    (q : zcCompletedDifferentialModuleStageSource C (MonoidHom.id G)
        (zcCompletedDifferentialModuleIdentitySourceIndex C ψ i)) :
    zcCompletedDifferentialModuleIdentitySourceStageToStage C ψ i
        (universalCrossedDifferential
          (zcCompletedDifferentialModuleStageScalar C (MonoidHom.id G)
            (zcCompletedDifferentialModuleIdentitySourceIndex C ψ i)) q) =
      universalCrossedDifferential (zcCompletedDifferentialModuleStageScalar C ψ i) q

theorem

zcCompletedDifferentialModuleStage_completed_smul

L575 ↗

FoxDifferential.zcCompletedDifferentialModuleStage_completed_smul

Documentation

Finite-stage scalar multiplication agrees with first projecting the completed group-algebra scalar and the completed differential-module element.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (ψ : G →* H)
omit [IsTopologicalGroup G] in

Lean source · statement

theorem zcCompletedDifferentialModuleStage_completed_smul
    (i : ZCCompletedDifferentialModuleIndex C ψ)
    (a : ZCCompletedGroupAlgebra C H)
    (m : ZCCompletedDifferentialModuleStage C ψ i) :
    a • m =
      zcCompletedGroupAlgebraProjectionRingHom C H i.target a • m

theorem

zcCompletedDifferentialModuleStage_completed_groupLike_smul

L589 ↗

FoxDifferential.zcCompletedDifferentialModuleStage_completed_groupLike_smul

Documentation

Group-like completed scalars act at a finite stage through the corresponding projected target-group basis element.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (ψ : G →* H)
omit [IsTopologicalGroup G] in

Lean source · statement

theorem zcCompletedDifferentialModuleStage_completed_groupLike_smul
    (i : ZCCompletedDifferentialModuleIndex C ψ) (g : G)
    (m : ZCCompletedDifferentialModuleStage C ψ i) :
    zcCompletedGroupAlgebraScalar C ψ g • m =
      zcCompletedDifferentialModuleStageScalar C ψ i
        (zcCompletedDifferentialModuleStageSourceProj C ψ i g) • m

def

zcCompletedDifferentialModuleStageDifferential

L603 ↗

FoxDifferential.zcCompletedDifferentialModuleStageDifferential

Documentation

The finite-stage universal differential, with scalars restricted from the completed group algebra.

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (ψ : G →* H)

Lean source · full declaration

def zcCompletedDifferentialModuleStageDifferential
    (i : ZCCompletedDifferentialModuleIndex C ψ) :
    ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ)
      (ZCCompletedDifferentialModuleStage C ψ i) where
  toFun g :=
    universalCrossedDifferential (zcCompletedDifferentialModuleStageScalar C ψ i)
      (zcCompletedDifferentialModuleStageSourceProj C ψ i g)
  map_mul' := by
    intro g h
    change
      universalCrossedDifferential (zcCompletedDifferentialModuleStageScalar C ψ i)
          (zcCompletedDifferentialModuleStageSourceProj C ψ i (g * h)) =
        universalCrossedDifferential (zcCompletedDifferentialModuleStageScalar C ψ i)
            (zcCompletedDifferentialModuleStageSourceProj C ψ i g) +
          zcCompletedGroupAlgebraScalar C ψ g •
            universalCrossedDifferential (zcCompletedDifferentialModuleStageScalar C ψ i)
              (zcCompletedDifferentialModuleStageSourceProj C ψ i h)
    rw [map_mul, universalCrossedDifferential_mul,
      zcCompletedDifferentialModuleStage_completed_groupLike_smul]

theorem

zcCompletedDifferentialModuleStageDifferential_one

L626 ↗

FoxDifferential.zcCompletedDifferentialModuleStageDifferential_one

Documentation

The finite-stage completed differential sends the identity element to zero.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (ψ : G →* H)
omit [IsTopologicalGroup G] in

Lean source · statement

theorem zcCompletedDifferentialModuleStageDifferential_one
    (i : ZCCompletedDifferentialModuleIndex C ψ) :
    zcCompletedDifferentialModuleStageDifferential C ψ i (1 : G) = 0

def

zcCompletedDifferentialModuleStageBoundary

L632 ↗

FoxDifferential.zcCompletedDifferentialModuleStageBoundary

Documentation

Boundary map from a finite differential-module stage to its coefficient group algebra stage.

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (ψ : G →* H)

Lean source · statement

def zcCompletedDifferentialModuleStageBoundary
    (i : ZCCompletedDifferentialModuleIndex C ψ) :
    ZCCompletedDifferentialModuleStage C ψ i →ₗ[zcCompletedDifferentialModuleStageRing C ψ i]
      zcCompletedDifferentialModuleStageRing C ψ i

theorem

zcCompletedDifferentialModuleStageBoundary_differential

L648 ↗

FoxDifferential.zcCompletedDifferentialModuleStageBoundary_differential

Documentation

The \(\mathbb{Z}_C\)-completed differential-module boundary is the finite-stage boundary obtained from the source and target coordinates.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (ψ : G →* H)
omit [IsTopologicalGroup G] in

Lean source · statement

theorem zcCompletedDifferentialModuleStageBoundary_differential
    (i : ZCCompletedDifferentialModuleIndex C ψ) (g : G) :
    zcCompletedDifferentialModuleStageBoundary C ψ i
        (zcCompletedDifferentialModuleStageDifferential C ψ i g) =
      zcCompletedDifferentialModuleStageScalar C ψ i
        (zcCompletedDifferentialModuleStageSourceProj C ψ i g) - 1

def

zcCompletedDifferentialModuleStageBoundaryCompletedLinearMap

L670 ↗

FoxDifferential.zcCompletedDifferentialModuleStageBoundaryCompletedLinearMap

Documentation

The finite-stage boundary as a completed-ring-linear map, using restriction of scalars through the coefficient stage projection.

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (ψ : G →* H)

Lean source · full declaration

def zcCompletedDifferentialModuleStageBoundaryCompletedLinearMap
    (i : ZCCompletedDifferentialModuleIndex C ψ) :
    ZCCompletedDifferentialModuleStage C ψ i →ₗ[ZCCompletedGroupAlgebra C H]
      ZCCompletedGroupAlgebraStage C H i.target where
  toFun := zcCompletedDifferentialModuleStageBoundary C ψ i
  map_add' x y := by
    exact map_add (zcCompletedDifferentialModuleStageBoundary C ψ i) x y
  map_smul' r x := by
    change zcCompletedDifferentialModuleStageBoundary C ψ i
        (zcCompletedGroupAlgebraProjectionRingHom C H i.target r • x) =
      zcCompletedGroupAlgebraProjectionRingHom C H i.target r •
        zcCompletedDifferentialModuleStageBoundary C ψ i x
    exact map_smul (zcCompletedDifferentialModuleStageBoundary C ψ i)
      (zcCompletedGroupAlgebraProjectionRingHom C H i.target r) x

theorem

zcCompletedDifferentialModuleStageBoundaryCompletedLinearMap_apply

L691 ↗

FoxDifferential.zcCompletedDifferentialModuleStageBoundaryCompletedLinearMap_apply

Documentation

The completed Fox boundary linear map is evaluated by applying the finite-stage boundary formula to each coordinate.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (ψ : G →* H)
omit [IsTopologicalGroup G] in

Lean source · statement

theorem zcCompletedDifferentialModuleStageBoundaryCompletedLinearMap_apply
    (i : ZCCompletedDifferentialModuleIndex C ψ)
    (x : ZCCompletedDifferentialModuleStage C ψ i) :
    zcCompletedDifferentialModuleStageBoundaryCompletedLinearMap C ψ i x =
      zcCompletedDifferentialModuleStageBoundary C ψ i x

def

zcCompletedDifferentialModuleStageProjection

L701 ↗

FoxDifferential.zcCompletedDifferentialModuleStageProjection

Documentation

The projection from the algebraic completed module to a finite source/target/coefficient stage.

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (ψ : G →* H)

Lean source · statement

def zcCompletedDifferentialModuleStageProjection
    (i : ZCCompletedDifferentialModuleIndex C ψ) :
    ZCCompletedDifferentialModule C ψ →ₗ[ZCCompletedGroupAlgebra C H]
      ZCCompletedDifferentialModuleStage C ψ i

theorem

zcCompletedDifferentialModuleStageProjection_universal

L716 ↗

FoxDifferential.zcCompletedDifferentialModuleStageProjection_universal

Documentation

The finite-stage projection sends the universal differential to the corresponding finite-stage differential.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (ψ : G →* H)
omit [IsTopologicalGroup G] in

Lean source · statement

theorem zcCompletedDifferentialModuleStageProjection_universal
    (i : ZCCompletedDifferentialModuleIndex C ψ) (g : G) :
    zcCompletedDifferentialModuleStageProjection C ψ i
        (zcUniversalDifferential C ψ g) =
      zcCompletedDifferentialModuleStageDifferential C ψ i g

theorem

zcDiffModuleIdentitySourceStageToStage_stageProj_universal

L731 ↗

FoxDifferential.zcDiffModuleIdentitySourceStageToStage_stageProj_universal

Documentation

The identity-source comparison carries the projected universal differential of g to its projection at the original stage.

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (ψ : G →* H)

Lean source · statement

theorem zcDiffModuleIdentitySourceStageToStage_stageProj_universal
    (i : ZCCompletedDifferentialModuleIndex C ψ) (g : G) :
    zcCompletedDifferentialModuleIdentitySourceStageToStage C ψ i
        (zcCompletedDifferentialModuleStageProjection C (MonoidHom.id G)
          (zcCompletedDifferentialModuleIdentitySourceIndex C ψ i)
          (zcUniversalDifferential C (MonoidHom.id G) g)) =
      zcCompletedDifferentialModuleStageProjection C ψ i
        (zcUniversalDifferential C ψ g)

theorem

zcCompletedDifferentialModuleStageProjection_mkQ

L756 ↗

FoxDifferential.zcCompletedDifferentialModuleStageProjection_mkQ

Documentation

The finite-stage projection evaluated on a representative of the universal quotient module.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (ψ : G →* H)
omit [IsTopologicalGroup G] in

Lean source · statement

theorem zcCompletedDifferentialModuleStageProjection_mkQ
    (i : ZCCompletedDifferentialModuleIndex C ψ)
    (x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :
    zcCompletedDifferentialModuleStageProjection C ψ i
        ((crossedDifferentialRelationSubmodule
          (zcCompletedGroupAlgebraScalar C ψ)).mkQ x) =
      crossedDifferentialModuleLiftLinear
        (R := ZCCompletedGroupAlgebra C H)
        (zcCompletedDifferentialModuleStageDifferential C ψ i) x

def

zcCompletedDifferentialModulePreStageMap

L774 ↗

FoxDifferential.zcCompletedDifferentialModulePreStageMap

Documentation

The pre-module map obtained by reducing coefficients to a finite target stage and source generators to the corresponding finite source quotient.

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (ψ : G →* H)

Lean source · statement

def zcCompletedDifferentialModulePreStageMap
    (i : ZCCompletedDifferentialModuleIndex C ψ) :
    CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G →ₗ[ZCCompletedGroupAlgebra C H]
      CrossedDifferentialPreModule
        (zcCompletedDifferentialModuleStageRing C ψ i)
        (zcCompletedDifferentialModuleStageSource C ψ i)

theorem

zcCompletedDifferentialModulePreStageMap_single

L793 ↗

FoxDifferential.zcCompletedDifferentialModulePreStageMap_single

Documentation

The finite pre-stage map evaluates a basis differential by the corresponding finite-stage source and target coordinates.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (ψ : G →* H)
omit [IsTopologicalGroup G] in

Lean source · statement

theorem zcCompletedDifferentialModulePreStageMap_single
    (i : ZCCompletedDifferentialModuleIndex C ψ)
    (g : G) (a : ZCCompletedGroupAlgebra C H) :
    zcCompletedDifferentialModulePreStageMap C ψ i (Finsupp.single g a) =
      Finsupp.single (zcCompletedDifferentialModuleStageSourceProj C ψ i g)
        (zcCompletedGroupAlgebraProjection C H i.target a)

theorem

zcCompletedDifferentialModulePreStageMap_relationElement

L811 ↗

FoxDifferential.zcCompletedDifferentialModulePreStageMap_relationElement

Documentation

The explicit finite pre-stage map carries completed crossed-differential relation generators to the corresponding finite relation generators.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (ψ : G →* H)
omit [IsTopologicalGroup G] in

Lean source · statement

theorem zcCompletedDifferentialModulePreStageMap_relationElement
    (i : ZCCompletedDifferentialModuleIndex C ψ) (g h : G) :
    zcCompletedDifferentialModulePreStageMap C ψ i
        (crossedDifferentialRelationElement (zcCompletedGroupAlgebraScalar C ψ) g h) =
      crossedDifferentialRelationElement
        (zcCompletedDifferentialModuleStageScalar C ψ i)
        (zcCompletedDifferentialModuleStageSourceProj C ψ i g)
        (zcCompletedDifferentialModuleStageSourceProj C ψ i h)

theorem

zcCompletedDifferentialModulePreStageMap_relationSubmodule_surjective

L832 ↗

FoxDifferential.zcCompletedDifferentialModulePreStageMap_relationSubmodule_surjective

Documentation

Every finite crossed-differential relation is the reduction of a completed crossed-differential relation.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (ψ : G →* H)
omit [IsTopologicalGroup G] in

Lean source · statement

theorem zcCompletedDifferentialModulePreStageMap_relationSubmodule_surjective
    (i : ZCCompletedDifferentialModuleIndex C ψ)
    {y : CrossedDifferentialPreModule
        (zcCompletedDifferentialModuleStageRing C ψ i)
        (zcCompletedDifferentialModuleStageSource C ψ i)}
    (hy : y ∈ crossedDifferentialRelationSubmodule
        (zcCompletedDifferentialModuleStageScalar C ψ i)) :
    ∃ x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G,
      x ∈ crossedDifferentialRelationSubmodule (zcCompletedGroupAlgebraScalar C ψ) ∧
        zcCompletedDifferentialModulePreStageMap C ψ i x = y

theorem

zcCompletedDifferentialModulePreStageMap_mkQ

L885 ↗

FoxDifferential.zcCompletedDifferentialModulePreStageMap_mkQ

Documentation

The finite-stage lift from the completed pre-module is obtained by applying the quotient map after the explicit source-and-coefficient finite-stage pre-map.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (ψ : G →* H)
omit [IsTopologicalGroup G] in

Lean source · statement

theorem zcCompletedDifferentialModulePreStageMap_mkQ
    (i : ZCCompletedDifferentialModuleIndex C ψ)
    (x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :
    (crossedDifferentialRelationSubmodule
      (zcCompletedDifferentialModuleStageScalar C ψ i)).mkQ
        (zcCompletedDifferentialModulePreStageMap C ψ i x) =
      crossedDifferentialModuleLiftLinear
        (R := ZCCompletedGroupAlgebra C H)
        (zcCompletedDifferentialModuleStageDifferential C ψ i) x

theorem

zcDiffModuleStageBoundaryCompletedLinearMap_comp_stageProj

L940 ↗

FoxDifferential.zcDiffModuleStageBoundaryCompletedLinearMap_comp_stageProj

Documentation

Applying the completed boundary and then projecting to a finite coefficient stage agrees with first projecting \(A_{\psi}(C)\) to the corresponding finite crossed-differential stage and then taking the finite-stage boundary.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (ψ : G →* H)
omit [IsTopologicalGroup G] in

Lean source · statement

theorem zcDiffModuleStageBoundaryCompletedLinearMap_comp_stageProj
    (i : ZCCompletedDifferentialModuleIndex C ψ) :
    (zcCompletedDifferentialModuleStageBoundaryCompletedLinearMap C ψ i).comp
        (zcCompletedDifferentialModuleStageProjection C ψ i) =
      (zcCompletedGroupAlgebraProjectionLinearMap C H i.target).comp
        (zcToCompletedGroupAlgebra C ψ)

theorem

zcDiffModuleIdentitySourceStageProj_eq_zero_of_boundary_eq_zero

L977 ↗

FoxDifferential.zcDiffModuleIdentitySourceStageProj_eq_zero_of_boundary_eq_zero

Documentation

At a source-identity finite stage, vanishing finite boundary forces vanishing in the finite crossed-differential stage.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (ψ : G →* H)
omit [IsTopologicalGroup H] in

Lean source · statement

theorem zcDiffModuleIdentitySourceStageProj_eq_zero_of_boundary_eq_zero
    (i : ZCCompletedDifferentialModuleIndex C ψ)
    (x : ZCCompletedDifferentialModule C (MonoidHom.id G))
    (hx :
      zcCompletedDifferentialModuleStageBoundary C (MonoidHom.id G)
          (zcCompletedDifferentialModuleIdentitySourceIndex C ψ i)
          (zcCompletedDifferentialModuleStageProjection C (MonoidHom.id G)
            (zcCompletedDifferentialModuleIdentitySourceIndex C ψ i) x) = 0) :
    zcCompletedDifferentialModuleStageProjection C (MonoidHom.id G)
        (zcCompletedDifferentialModuleIdentitySourceIndex C ψ i) x = 0

theorem

zcDiffModuleIdentitySourceStageProj_eq_zero_of_zcTo_eq_zero

L1079 ↗

FoxDifferential.zcDiffModuleIdentitySourceStageProj_eq_zero_of_zcTo_eq_zero

Documentation

A zero source-identity completed Fox tail has zero projection to every source-identity finite stage attached to a \(\psi\)-stage.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (ψ : G →* H)
omit [IsTopologicalGroup H] in

Lean source · statement

theorem zcDiffModuleIdentitySourceStageProj_eq_zero_of_zcTo_eq_zero
    (i : ZCCompletedDifferentialModuleIndex C ψ)
    (x : ZCCompletedDifferentialModule C (MonoidHom.id G))
    (hx : zcToCompletedGroupAlgebra C (MonoidHom.id G) x = 0) :
    zcCompletedDifferentialModuleStageProjection C (MonoidHom.id G)
        (zcCompletedDifferentialModuleIdentitySourceIndex C ψ i) x = 0

def

zcCompletedDifferentialModuleStageSourceTransition

L1098 ↗

FoxDifferential.zcCompletedDifferentialModuleStageSourceTransition

Documentation

The source transition \((G/V)_j\to (G/V)_i\) for \(i\leq j\).

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (ψ : G →* H)

Lean source · statement

def zcCompletedDifferentialModuleStageSourceTransition
    {i j : ZCCompletedDifferentialModuleIndex C ψ} (hij : i ≤ j) :
    zcCompletedDifferentialModuleStageSource C ψ j →*
      zcCompletedDifferentialModuleStageSource C ψ i

theorem

zcCompletedDifferentialModuleStageSourceTransition_coe

L1110 ↗

FoxDifferential.zcCompletedDifferentialModuleStageSourceTransition_coe

Documentation

The source transition sends the quotient class of g at the finer stage to the quotient class of g at the coarser stage.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (ψ : G →* H)
omit [IsTopologicalGroup G] [IsTopologicalGroup H] in

Lean source · statement

theorem zcCompletedDifferentialModuleStageSourceTransition_coe
    {i j : ZCCompletedDifferentialModuleIndex C ψ} (hij : i ≤ j) (g : G) :
    zcCompletedDifferentialModuleStageSourceTransition C ψ hij
        (QuotientGroup.mk g : zcCompletedDifferentialModuleStageSource C ψ j) =
      (QuotientGroup.mk g : zcCompletedDifferentialModuleStageSource C ψ i)

theorem

zcCompletedDifferentialModuleStageSourceTransition_mk

L1123 ↗

FoxDifferential.zcCompletedDifferentialModuleStageSourceTransition_mk

Documentation

The source transition carries QuotientGroup.mk' for the finer source subgroup to QuotientGroup.mk' for the coarser source subgroup.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (ψ : G →* H)
omit [IsTopologicalGroup G] [IsTopologicalGroup H] in

Lean source · statement

theorem zcCompletedDifferentialModuleStageSourceTransition_mk
    {i j : ZCCompletedDifferentialModuleIndex C ψ} (hij : i ≤ j) (g : G) :
    zcCompletedDifferentialModuleStageSourceTransition C ψ hij
        (QuotientGroup.mk' (j.source.1 : Subgroup G) g) =
      QuotientGroup.mk' (i.source.1 : Subgroup G) g

theorem

zcCompletedDifferentialModuleStageSourceTransition_sourceProj

L1133 ↗

FoxDifferential.zcCompletedDifferentialModuleStageSourceTransition_sourceProj

Documentation

Source projection commutes with the source transition between differential-module stages.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (ψ : G →* H)
omit [IsTopologicalGroup G] [IsTopologicalGroup H] in

Lean source · statement

theorem zcCompletedDifferentialModuleStageSourceTransition_sourceProj
    {i j : ZCCompletedDifferentialModuleIndex C ψ} (hij : i ≤ j) (g : G) :
    zcCompletedDifferentialModuleStageSourceTransition C ψ hij
        (zcCompletedDifferentialModuleStageSourceProj C ψ j g) =
      zcCompletedDifferentialModuleStageSourceProj C ψ i g

theorem

zcCompletedDifferentialModuleStageSourceTransition_id

L1144 ↗

FoxDifferential.zcCompletedDifferentialModuleStageSourceTransition_id

Documentation

The source transition attached to a reflexive refinement fixes every source-stage element.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (ψ : G →* H)
omit [IsTopologicalGroup G] [IsTopologicalGroup H] in

Lean source · statement

theorem zcCompletedDifferentialModuleStageSourceTransition_id
    (i : ZCCompletedDifferentialModuleIndex C ψ)
    (x : zcCompletedDifferentialModuleStageSource C ψ i) :
    zcCompletedDifferentialModuleStageSourceTransition C ψ (le_rfl : i ≤ i) x = x

theorem

zcCompletedDifferentialModuleStageSourceTransition_comp

L1154 ↗

FoxDifferential.zcCompletedDifferentialModuleStageSourceTransition_comp

Documentation

Successive source transitions agree with the source transition for the composite refinement.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (ψ : G →* H)
omit [IsTopologicalGroup G] [IsTopologicalGroup H] in

Lean source · statement

theorem zcCompletedDifferentialModuleStageSourceTransition_comp
    {i j k : ZCCompletedDifferentialModuleIndex C ψ}
    (hij : i ≤ j) (hjk : j ≤ k)
    (x : zcCompletedDifferentialModuleStageSource C ψ k) :
    zcCompletedDifferentialModuleStageSourceTransition C ψ hij
        (zcCompletedDifferentialModuleStageSourceTransition C ψ hjk x) =
      zcCompletedDifferentialModuleStageSourceTransition C ψ (hij.trans hjk) x

def

zcCompletedDifferentialModuleStageTargetTransition

L1165 ↗

FoxDifferential.zcCompletedDifferentialModuleStageTargetTransition

Documentation

The target transition \(H/U_j \to H/U_i\) underlying the coefficient transition.

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (ψ : G →* H)

Lean source · statement

def zcCompletedDifferentialModuleStageTargetTransition
    {i j : ZCCompletedDifferentialModuleIndex C ψ} (hij : i ≤ j) :
    zcCompletedDifferentialModuleStageTarget C ψ j →*
      zcCompletedDifferentialModuleStageTarget C ψ i

theorem

zcCompletedDifferentialModuleStageTargetTransition_coe

L1178 ↗

FoxDifferential.zcCompletedDifferentialModuleStageTargetTransition_coe

Documentation

The target transition sends the quotient class of h at the finer stage to its class at the coarser stage.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (ψ : G →* H)
omit [IsTopologicalGroup G] in

Lean source · statement

theorem zcCompletedDifferentialModuleStageTargetTransition_coe
    {i j : ZCCompletedDifferentialModuleIndex C ψ} (hij : i ≤ j) (h : H) :
    zcCompletedDifferentialModuleStageTargetTransition C ψ hij
        (QuotientGroup.mk h : zcCompletedDifferentialModuleStageTarget C ψ j) =
      (QuotientGroup.mk h : zcCompletedDifferentialModuleStageTarget C ψ i)

theorem

zcCompletedDifferentialModuleStageTargetTransition_mk

L1191 ↗

FoxDifferential.zcCompletedDifferentialModuleStageTargetTransition_mk

Documentation

The target transition carries QuotientGroup.mk' for the finer target subgroup to QuotientGroup.mk' for the coarser target subgroup.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (ψ : G →* H)
omit [IsTopologicalGroup G] in

Lean source · statement

theorem zcCompletedDifferentialModuleStageTargetTransition_mk
    {i j : ZCCompletedDifferentialModuleIndex C ψ} (hij : i ≤ j) (h : H) :
    zcCompletedDifferentialModuleStageTargetTransition C ψ hij
        (QuotientGroup.mk' ((OrderDual.ofDual j.target.2).1 : Subgroup H) h) =
      QuotientGroup.mk' ((OrderDual.ofDual i.target.2).1 : Subgroup H) h

theorem

zcCompletedDifferentialModuleStageTargetTransition_id

L1201 ↗

FoxDifferential.zcCompletedDifferentialModuleStageTargetTransition_id

Documentation

The target transition attached to a reflexive refinement fixes every target-stage element.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (ψ : G →* H)
omit [IsTopologicalGroup G] in

Lean source · statement

theorem zcCompletedDifferentialModuleStageTargetTransition_id
    (i : ZCCompletedDifferentialModuleIndex C ψ)
    (x : zcCompletedDifferentialModuleStageTarget C ψ i) :
    zcCompletedDifferentialModuleStageTargetTransition C ψ (le_rfl : i ≤ i) x = x

theorem

zcCompletedDifferentialModuleStageTargetTransition_comp

L1213 ↗

FoxDifferential.zcCompletedDifferentialModuleStageTargetTransition_comp

Documentation

Successive target transitions agree with the target transition for the composite refinement.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (ψ : G →* H)
omit [IsTopologicalGroup G] in

Lean source · statement

theorem zcCompletedDifferentialModuleStageTargetTransition_comp
    {i j k : ZCCompletedDifferentialModuleIndex C ψ}
    (hij : i ≤ j) (hjk : j ≤ k)
    (x : zcCompletedDifferentialModuleStageTarget C ψ k) :
    zcCompletedDifferentialModuleStageTargetTransition C ψ hij
        (zcCompletedDifferentialModuleStageTargetTransition C ψ hjk x) =
      zcCompletedDifferentialModuleStageTargetTransition C ψ (hij.trans hjk) x

theorem

zcCompletedDifferentialModuleStagePsi_transition

L1228 ↗

FoxDifferential.zcCompletedDifferentialModuleStagePsi_transition

Documentation

The source-to-target stage map commutes with the source and target transition maps.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (ψ : G →* H)
omit [IsTopologicalGroup G] in

Lean source · statement

theorem zcCompletedDifferentialModuleStagePsi_transition
    {i j : ZCCompletedDifferentialModuleIndex C ψ} (hij : i ≤ j)
    (x : zcCompletedDifferentialModuleStageSource C ψ j) :
    zcCompletedDifferentialModuleStageTargetTransition C ψ hij
        (zcCompletedDifferentialModuleStagePsi C ψ j x) =
      zcCompletedDifferentialModuleStagePsi C ψ i
        (zcCompletedDifferentialModuleStageSourceTransition C ψ hij x)

theorem

zcCompletedDifferentialModuleStageScalar_transition

L1246 ↗

FoxDifferential.zcCompletedDifferentialModuleStageScalar_transition

Documentation

The group-algebra transition of a stage scalar equals the scalar of the transitioned source element.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (ψ : G →* H)
omit [IsTopologicalGroup G] in

Lean source · statement

theorem zcCompletedDifferentialModuleStageScalar_transition
    {i j : ZCCompletedDifferentialModuleIndex C ψ} (hij : i ≤ j)
    (x : zcCompletedDifferentialModuleStageSource C ψ j) :
    zcCompletedGroupAlgebraTransition C H hij.2
        (zcCompletedDifferentialModuleStageScalar C ψ j x) =
      zcCompletedDifferentialModuleStageScalar C ψ i
        (zcCompletedDifferentialModuleStageSourceTransition C ψ hij x)

def

zcCompletedDifferentialModulePreStageTransition

L1273 ↗

FoxDifferential.zcCompletedDifferentialModulePreStageTransition

Documentation

Additive transition between the finite pre-modules before quotienting by the crossed-differential relations.

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (ψ : G →* H)

Lean source · statement

def zcCompletedDifferentialModulePreStageTransition
    {i j : ZCCompletedDifferentialModuleIndex C ψ} (hij : i ≤ j) :
    CrossedDifferentialPreModule
        (zcCompletedDifferentialModuleStageRing C ψ j)
        (zcCompletedDifferentialModuleStageSource C ψ j) →+
      CrossedDifferentialPreModule
        (zcCompletedDifferentialModuleStageRing C ψ i)
        (zcCompletedDifferentialModuleStageSource C ψ i)

theorem

zcCompletedDifferentialModulePreStageTransition_single

L1293 ↗

FoxDifferential.zcCompletedDifferentialModulePreStageTransition_single

Documentation

The finite-stage transition sends a singleton basis function to the singleton supported at its image in the coarser quotient.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (ψ : G →* H)
omit [IsTopologicalGroup G] in

Lean source · statement

theorem zcCompletedDifferentialModulePreStageTransition_single
    {i j : ZCCompletedDifferentialModuleIndex C ψ} (hij : i ≤ j)
    (q : zcCompletedDifferentialModuleStageSource C ψ j)
    (a : zcCompletedDifferentialModuleStageRing C ψ j) :
    zcCompletedDifferentialModulePreStageTransition C ψ hij (Finsupp.single q a) =
      Finsupp.single (zcCompletedDifferentialModuleStageSourceTransition C ψ hij q)
        (zcCompletedGroupAlgebraTransition C H hij.2 a)

theorem

zcCompletedDifferentialModulePreStageTransition_preStageMap

L1309 ↗

FoxDifferential.zcCompletedDifferentialModulePreStageTransition_preStageMap

Documentation

Completed-to-pre-stage reduction is compatible with finite-stage transitions.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (ψ : G →* H)
omit [IsTopologicalGroup G] in

Lean source · statement

theorem zcCompletedDifferentialModulePreStageTransition_preStageMap
    {i j : ZCCompletedDifferentialModuleIndex C ψ} (hij : i ≤ j)
    (x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :
    zcCompletedDifferentialModulePreStageTransition C ψ hij
        (zcCompletedDifferentialModulePreStageMap C ψ j x) =
      zcCompletedDifferentialModulePreStageMap C ψ i x

def

zcCompletedDifferentialModuleStageTransitionCrossedHom

L1332 ↗

FoxDifferential.zcCompletedDifferentialModuleStageTransitionCrossedHom

Documentation

The universal differential transported along a finite-stage refinement.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (ψ : G →* H)
omit [IsTopologicalGroup G] in

Lean source · full declaration

def zcCompletedDifferentialModuleStageTransitionCrossedHom
    {i j : ZCCompletedDifferentialModuleIndex C ψ} (hij : i ≤ j) :
    letI : Module (zcCompletedDifferentialModuleStageRing C ψ j)
        (ZCCompletedDifferentialModuleStage C ψ i) :=
      Module.compHom _ (zcCompletedGroupAlgebraTransition C H hij.2)
    ScalarCrossedHom (zcCompletedDifferentialModuleStageScalar C ψ j)
      (ZCCompletedDifferentialModuleStage C ψ i) := by
  letI : Module (zcCompletedDifferentialModuleStageRing C ψ j)
      (ZCCompletedDifferentialModuleStage C ψ i) :=
    Module.compHom _ (zcCompletedGroupAlgebraTransition C H hij.2)
  exact
    { toFun := fun x =>
        universalCrossedDifferential (zcCompletedDifferentialModuleStageScalar C ψ i)
          (zcCompletedDifferentialModuleStageSourceTransition C ψ hij x)
      map_mul' := by
        intro x y
        change
          universalCrossedDifferential (zcCompletedDifferentialModuleStageScalar C ψ i)
              (zcCompletedDifferentialModuleStageSourceTransition C ψ hij (x * y)) =
            universalCrossedDifferential (zcCompletedDifferentialModuleStageScalar C ψ i)
                (zcCompletedDifferentialModuleStageSourceTransition C ψ hij x) +
              zcCompletedDifferentialModuleStageScalar C ψ j x •
                universalCrossedDifferential (zcCompletedDifferentialModuleStageScalar C ψ i)
                  (zcCompletedDifferentialModuleStageSourceTransition C ψ hij y)
        rw [map_mul, universalCrossedDifferential_mul]
        congr 1
        change
          zcCompletedDifferentialModuleStageScalar C ψ i
              (zcCompletedDifferentialModuleStageSourceTransition C ψ hij x) •
              universalCrossedDifferential (zcCompletedDifferentialModuleStageScalar C ψ i)
                (zcCompletedDifferentialModuleStageSourceTransition C ψ hij y) =
            zcCompletedGroupAlgebraTransition C H hij.2
              (zcCompletedDifferentialModuleStageScalar C ψ j x) •
              universalCrossedDifferential (zcCompletedDifferentialModuleStageScalar C ψ i)
                (zcCompletedDifferentialModuleStageSourceTransition C ψ hij y)
        rw [zcCompletedDifferentialModuleStageScalar_transition] }

def

zcCompletedDifferentialModuleStageTransition

L1372 ↗

FoxDifferential.zcCompletedDifferentialModuleStageTransition

Documentation

The additive transition map from a finer completed differential-module stage to a coarser stage.

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (ψ : G →* H)

Lean source · statement

def zcCompletedDifferentialModuleStageTransition
    {i j : ZCCompletedDifferentialModuleIndex C ψ} (hij : i ≤ j) :
    ZCCompletedDifferentialModuleStage C ψ j →+
      ZCCompletedDifferentialModuleStage C ψ i

theorem

zcCompletedDifferentialModuleStageTransition_universal

L1391 ↗

FoxDifferential.zcCompletedDifferentialModuleStageTransition_universal

Documentation

The differential-module stage transition preserves the universal stage differential of each group element.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (ψ : G →* H)
omit [IsTopologicalGroup G] in

Lean source · statement

theorem zcCompletedDifferentialModuleStageTransition_universal
    {i j : ZCCompletedDifferentialModuleIndex C ψ} (hij : i ≤ j) (g : G) :
    zcCompletedDifferentialModuleStageTransition C ψ hij
        (zcCompletedDifferentialModuleStageDifferential C ψ j g) =
      zcCompletedDifferentialModuleStageDifferential C ψ i g

theorem

zcCompletedDifferentialModulePreStageTransition_mkQ

L1425 ↗

FoxDifferential.zcCompletedDifferentialModulePreStageTransition_mkQ

Documentation

The finite pre-module transition descends to the quotient transition between finite differential-module stages.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (ψ : G →* H)
omit [IsTopologicalGroup G] in

Lean source · statement

theorem zcCompletedDifferentialModulePreStageTransition_mkQ
    {i j : ZCCompletedDifferentialModuleIndex C ψ} (hij : i ≤ j)
    (x : CrossedDifferentialPreModule
        (zcCompletedDifferentialModuleStageRing C ψ j)
        (zcCompletedDifferentialModuleStageSource C ψ j)) :
    (crossedDifferentialRelationSubmodule
        (zcCompletedDifferentialModuleStageScalar C ψ i)).mkQ
        (zcCompletedDifferentialModulePreStageTransition C ψ hij x) =
      zcCompletedDifferentialModuleStageTransition C ψ hij
        ((crossedDifferentialRelationSubmodule
          (zcCompletedDifferentialModuleStageScalar C ψ j)).mkQ x)

theorem

zcCompletedDifferentialModulePreStageTransition_mem_relationSubmodule

L1492 ↗

FoxDifferential.zcCompletedDifferentialModulePreStageTransition_mem_relationSubmodule

Documentation

Finite pre-stage transitions preserve the crossed-differential relation submodules.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (ψ : G →* H)
omit [IsTopologicalGroup G] in

Lean source · statement

theorem zcCompletedDifferentialModulePreStageTransition_mem_relationSubmodule
    {i j : ZCCompletedDifferentialModuleIndex C ψ} (hij : i ≤ j)
    {x : CrossedDifferentialPreModule
        (zcCompletedDifferentialModuleStageRing C ψ j)
        (zcCompletedDifferentialModuleStageSource C ψ j)}
    (hx : x ∈ crossedDifferentialRelationSubmodule
        (zcCompletedDifferentialModuleStageScalar C ψ j)) :
    zcCompletedDifferentialModulePreStageTransition C ψ hij x ∈
      crossedDifferentialRelationSubmodule
        (zcCompletedDifferentialModuleStageScalar C ψ i)

theorem

zcCompletedDifferentialModulePreStageTransition_id

L1525 ↗

FoxDifferential.zcCompletedDifferentialModulePreStageTransition_id

Documentation

The pre-stage transition for a reflexive refinement is the identity additive homomorphism.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (ψ : G →* H)
omit [IsTopologicalGroup G] in

Lean source · statement

theorem zcCompletedDifferentialModulePreStageTransition_id
    (i : ZCCompletedDifferentialModuleIndex C ψ) :
    zcCompletedDifferentialModulePreStageTransition C ψ (le_rfl : i ≤ i) =
      AddMonoidHom.id
        (CrossedDifferentialPreModule
          (zcCompletedDifferentialModuleStageRing C ψ i)
          (zcCompletedDifferentialModuleStageSource C ψ i))

theorem

zcCompletedDifferentialModulePreStageTransition_comp

L1557 ↗

FoxDifferential.zcCompletedDifferentialModulePreStageTransition_comp

Documentation

Pre-stage transitions compose according to transitivity of index refinement.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (ψ : G →* H)
omit [IsTopologicalGroup G] in

Lean source · statement

theorem zcCompletedDifferentialModulePreStageTransition_comp
    {i j k : ZCCompletedDifferentialModuleIndex C ψ}
    (hij : i ≤ j) (hjk : j ≤ k) :
    (zcCompletedDifferentialModulePreStageTransition C ψ hij).comp
        (zcCompletedDifferentialModulePreStageTransition C ψ hjk) =
      zcCompletedDifferentialModulePreStageTransition C ψ (hij.trans hjk)

theorem

zcCompletedDifferentialModuleFiniteRelationReductions_finiteStageApproximation

L1592 ↗

FoxDifferential.zcCompletedDifferentialModuleFiniteRelationReductions_finiteStageApproximation

Documentation

If a completed pre-module element has relation-valued reductions at every finite stage, then any finite list of finite stages is matched by a single completed relation.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (ψ : G →* H)
omit [IsTopologicalGroup G] in

Lean source · statement

theorem zcCompletedDifferentialModuleFiniteRelationReductions_finiteStageApproximation
    (hdir : Directed (· ≤ ·)
      (id : ZCCompletedDifferentialModuleIndex C ψ →
        ZCCompletedDifferentialModuleIndex C ψ))
    (s : Finset (ZCCompletedDifferentialModuleIndex C ψ))
    (x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)
    (hx : ∀ i : ZCCompletedDifferentialModuleIndex C ψ,
      zcCompletedDifferentialModulePreStageMap C ψ i x ∈
        crossedDifferentialRelationSubmodule
          (zcCompletedDifferentialModuleStageScalar C ψ i)) :
    ∃ r : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G,
      r ∈ crossedDifferentialRelationSubmodule (zcCompletedGroupAlgebraScalar C ψ) ∧
        ∀ i ∈ s,
          zcCompletedDifferentialModulePreStageMap C ψ i r =
            zcCompletedDifferentialModulePreStageMap C ψ i x

theorem

zcCompletedDifferentialModuleStageTransition_comp_projection

L1628 ↗

FoxDifferential.zcCompletedDifferentialModuleStageTransition_comp_projection

Documentation

Transitioning a projected universal differential gives its projection at the coarser stage.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (ψ : G →* H)
omit [IsTopologicalGroup G] in

Lean source · statement

theorem zcCompletedDifferentialModuleStageTransition_comp_projection
    {i j : ZCCompletedDifferentialModuleIndex C ψ} (hij : i ≤ j) (g : G) :
    zcCompletedDifferentialModuleStageTransition C ψ hij
        (zcCompletedDifferentialModuleStageProjection C ψ j
          (zcUniversalDifferential C ψ g)) =
      zcCompletedDifferentialModuleStageProjection C ψ i
        (zcUniversalDifferential C ψ g)

theorem

zcCompletedDifferentialModuleStageTransition_id

L1644 ↗

FoxDifferential.zcCompletedDifferentialModuleStageTransition_id

Documentation

The differential-module stage transition for a reflexive refinement is the identity additive homomorphism.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (ψ : G →* H)
omit [IsTopologicalGroup G] in

Lean source · statement

theorem zcCompletedDifferentialModuleStageTransition_id
    (i : ZCCompletedDifferentialModuleIndex C ψ) :
    zcCompletedDifferentialModuleStageTransition C ψ (le_rfl : i ≤ i) =
      AddMonoidHom.id (ZCCompletedDifferentialModuleStage C ψ i)

theorem

zcCompletedDifferentialModuleStageTransition_comp

L1674 ↗

FoxDifferential.zcCompletedDifferentialModuleStageTransition_comp

Documentation

Differential-module stage transitions compose according to transitivity of index refinement.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (ψ : G →* H)
omit [IsTopologicalGroup G] in

Lean source · statement

theorem zcCompletedDifferentialModuleStageTransition_comp
    {i j k : ZCCompletedDifferentialModuleIndex C ψ}
    (hij : i ≤ j) (hjk : j ≤ k) :
    (zcCompletedDifferentialModuleStageTransition C ψ hij).comp
        (zcCompletedDifferentialModuleStageTransition C ψ hjk) =
      zcCompletedDifferentialModuleStageTransition C ψ (hij.trans hjk)

Module documentation

Fox differential: completed — continuous — universal — finite stage

Declarations