FoxDifferential.Completed.Continuous.Universal.FiniteStage

58 Theorem | 16 Definition | 4 Abbreviation | 1 Structure | 7 Instance

This module proves the universal-property part of the construction. It packages finite-stage data into completed maps and shows the required extension and uniqueness statements.

Open this file on GitHub

import

Imported by

Structure FoxDifferential.ZCCompletedDifferentialModuleIndex GitHub

structure ZCCompletedDifferentialModuleIndex (ψ : G →* H) where
  source : OpenNormalSubgroupInClass C G
  target : ZCCompletedGroupAlgebraIndex C H
  compatible :
    (source.1 : Subgroup G) ≤
      ((OrderDual.ofDual target.2).1 : Subgroup H).comap ψ

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

Instance FoxDifferential.ZCCompletedDifferentialModuleIndex.instLE GitHub

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

The completed Fox-differential object carries the bundled structure determined by its finite-stage data.

Instance FoxDifferential.ZCCompletedDifferentialModuleIndex.instPreorder GitHub

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⟩

The completed Fox-differential object carries the bundled structure determined by its finite-stage data.

Theorem FoxDifferential.ZCCompletedDifferentialModuleIndex.le_def GitHub

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

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

Show proof

Definition FoxDifferential.zcCompletedDifferentialModuleComapIndex GitHub

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

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

Theorem FoxDifferential.nonempty_zcCompletedDifferentialModuleIndex GitHub

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

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

Show proof

Theorem FoxDifferential.directed_zcCompletedDifferentialModuleIndex GitHub

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)

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.

Show proof

Abbreviation FoxDifferential.zcCompletedDifferentialModuleStageSource GitHub

abbrev zcCompletedDifferentialModuleStageSource
    (i : ZCCompletedDifferentialModuleIndex C ψ) : Type u :=
  G ⧸ (i.source.1 : Subgroup G)

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

Abbreviation FoxDifferential.zcCompletedDifferentialModuleStageTarget GitHub

abbrev zcCompletedDifferentialModuleStageTarget
    (i : ZCCompletedDifferentialModuleIndex C ψ) : Type u :=
  CompletedGroupAlgebraQuotientInClass H C i.target.2

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

Abbreviation FoxDifferential.zcCompletedDifferentialModuleStageRing GitHub

abbrev zcCompletedDifferentialModuleStageRing
    (i : ZCCompletedDifferentialModuleIndex C ψ) : Type u :=
  ZCCompletedGroupAlgebraStage C H i.target

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

Definition FoxDifferential.zcCompletedDifferentialModuleStagePsi GitHub

def zcCompletedDifferentialModuleStagePsi
    (i : ZCCompletedDifferentialModuleIndex C ψ) :
    zcCompletedDifferentialModuleStageSource C ψ i →*
      zcCompletedDifferentialModuleStageTarget C ψ i :=
  QuotientGroup.map
    (N := (i.source.1 : Subgroup G))
    (M := ((OrderDual.ofDual i.target.2).1 : Subgroup H))
    ψ i.compatible

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

Definition FoxDifferential.zcCompletedDifferentialModuleStageScalar GitHub

def zcCompletedDifferentialModuleStageScalar
    (i : ZCCompletedDifferentialModuleIndex C ψ) :
    zcCompletedDifferentialModuleStageSource C ψ i →*
      zcCompletedDifferentialModuleStageRing C ψ i :=
  (MonoidAlgebra.of (ModNCompletedCoeff i.target.1.modulus)
    (zcCompletedDifferentialModuleStageTarget C ψ i)).comp
      (zcCompletedDifferentialModuleStagePsi C ψ i)

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

Abbreviation FoxDifferential.ZCCompletedDifferentialModuleStage GitHub

abbrev ZCCompletedDifferentialModuleStage
    (i : ZCCompletedDifferentialModuleIndex C ψ) : Type u :=
  CrossedDifferentialModule (zcCompletedDifferentialModuleStageScalar C ψ i)

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

Instance FoxDifferential.instTopologicalSpaceZCCompletedDifferentialModuleStage GitHub

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

Finite completed differential-module stages carry the discrete topology.

Instance FoxDifferential.instDiscreteTopologyZCCompletedDifferentialModuleStage GitHub

instance instDiscreteTopologyZCCompletedDifferentialModuleStage
    (i : ZCCompletedDifferentialModuleIndex C ψ) :
    DiscreteTopology (ZCCompletedDifferentialModuleStage C ψ i) :=
  ⟨rfl⟩

Finite completed differential-module stages carry the discrete topology.

Instance FoxDifferential.instT2SpaceZCCompletedDifferentialModuleStage GitHub

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

Finite completed differential-module stages are Hausdorff.

Instance FoxDifferential.instIsTopologicalAddGroupZCCompletedDifferentialModuleStage GitHub

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

Finite completed differential-module stages are topological additive groups.

Instance FoxDifferential.instModuleZCCompletedGroupAlgebraZCCompletedDifferentialModuleStage GitHub

instance instModuleZCCompletedGroupAlgebraZCCompletedDifferentialModuleStage
    (i : ZCCompletedDifferentialModuleIndex C ψ) :
    Module (ZCCompletedGroupAlgebra C H) (ZCCompletedDifferentialModuleStage C ψ i) :=
  Module.compHom _ (zcCompletedGroupAlgebraProjectionRingHom C H i.target)

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

Definition FoxDifferential.zcCompletedDifferentialModuleStageSourceProj GitHub

def zcCompletedDifferentialModuleStageSourceProj
    (i : ZCCompletedDifferentialModuleIndex C ψ) :
    G →* zcCompletedDifferentialModuleStageSource C ψ i :=
  QuotientGroup.mk' (i.source.1 : Subgroup G)

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

Theorem FoxDifferential.zcCompletedDifferentialModuleStageSourceProj_apply GitHub

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

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

Show proof

Theorem FoxDifferential.zcCompletedDifferentialModuleStagePsi_mk GitHub

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)

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

Show proof

Theorem FoxDifferential.zcCompletedDifferentialModuleStageScalar_mk GitHub

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

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

Show proof

Theorem FoxDifferential.zcCompletedDifferentialModuleStagePsi_coe GitHub

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

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

Show proof

Theorem FoxDifferential.zcCompletedDifferentialModuleStageScalar_coe GitHub

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)

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

Show proof

Theorem FoxDifferential.zcCompletedDifferentialModuleStagePsi_sourceProj GitHub

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)

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

Show proof

Theorem FoxDifferential.zcCompletedDifferentialModuleStageScalar_sourceProj GitHub

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

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

Show proof

Definition FoxDifferential.zcCompletedDifferentialModuleIdentitySourceIndex GitHub

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

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.

Theorem FoxDifferential.zcCompletedDifferentialModuleIdentitySourceIndex_source GitHub

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

The identity-source stage of the \(\mathbb{Z}_C\)-completed differential module is identified with its finite source and target coordinates.

Show proof

Theorem FoxDifferential.zcCompletedDifferentialModuleIdentitySourceIndex_target_fst GitHub

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

The identity-source stage of the \(\mathbb{Z}_C\)-completed differential module is identified with its finite source and target coordinates.

Show proof

Theorem FoxDifferential.zcCompletedDifferentialModuleStageSourceProj_identitySourceIndex GitHub

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

The identity-source stage of the \(\mathbb{Z}_C\)-completed differential module is identified with its finite source and target coordinates.

Show proof

Theorem FoxDifferential.zcCompletedDifferentialModuleStagePsi_identitySourceIndex_sourceProj GitHub

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

The identity-source stage of the \(\mathbb{Z}_C\)-completed differential module is identified with its finite source and target coordinates.

Show proof

Theorem FoxDifferential.zcCompletedDifferentialModuleStageScalar_identitySourceIndex_sourceProj GitHub

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)

The identity-source stage of the \(\mathbb{Z}_C\)-completed differential module is identified with its finite source and target coordinates.

Show proof

Definition FoxDifferential.zcCompletedDifferentialModuleIdentitySourceStageRingHom GitHub

def zcCompletedDifferentialModuleIdentitySourceStageRingHom
    (i : ZCCompletedDifferentialModuleIndex C ψ) :
    RingHom
      (zcCompletedDifferentialModuleStageRing C (MonoidHom.id G)
        (zcCompletedDifferentialModuleIdentitySourceIndex C ψ i))
      (zcCompletedDifferentialModuleStageRing C ψ i) :=
  MonoidAlgebra.mapDomainRingHom (ModNCompletedCoeff i.target.1.modulus)
    (zcCompletedDifferentialModuleStagePsi C ψ i)

@[simp]

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

Theorem FoxDifferential.zcCompletedDifferentialModuleIdentitySourceStageRingHom_stageScalar GitHub

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

The identity-source stage of the \(\mathbb{Z}_C\)-completed differential module is identified with its finite source and target coordinates.

Show proof

Theorem FoxDifferential.zcCompletedDifferentialModuleIdentitySourceStageToStage_isCrossedDifferential GitHub

theorem zcCompletedDifferentialModuleIdentitySourceStageToStage_isCrossedDifferential
    (i : ZCCompletedDifferentialModuleIndex C ψ) :
    letI : Module
        (zcCompletedDifferentialModuleStageRing C (MonoidHom.id G)
          (zcCompletedDifferentialModuleIdentitySourceIndex C ψ i))
        (ZCCompletedDifferentialModuleStage C ψ i)

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

Show proof

Definition FoxDifferential.zcCompletedDifferentialModuleIdentitySourceStageToStage GitHub

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 crossedDifferentialModuleLift
    (A := ZCCompletedDifferentialModuleStage C ψ i)
    (zcCompletedDifferentialModuleStageScalar C (MonoidHom.id G)
      (zcCompletedDifferentialModuleIdentitySourceIndex C ψ i))
    (fun q : zcCompletedDifferentialModuleStageSource C (MonoidHom.id G)
        (zcCompletedDifferentialModuleIdentitySourceIndex C ψ i) =>
      universalCrossedDifferential (zcCompletedDifferentialModuleStageScalar C ψ i) q)
    (zcCompletedDifferentialModuleIdentitySourceStageToStage_isCrossedDifferential C ψ i)

@[simp]

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

Theorem FoxDifferential.zcCompletedDifferentialModuleIdentitySourceStageToStage_universal GitHub

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

The identity-source stage of the \(\mathbb{Z}_C\)-completed differential module is identified with its finite source and target coordinates.

Show proof

Definition FoxDifferential.zcCompletedDifferentialModuleStageDifferential GitHub

def zcCompletedDifferentialModuleStageDifferential
    (i : ZCCompletedDifferentialModuleIndex C ψ) (g : G) :
    ZCCompletedDifferentialModuleStage C ψ i :=
  universalCrossedDifferential (zcCompletedDifferentialModuleStageScalar C ψ i)
    (zcCompletedDifferentialModuleStageSourceProj C ψ i g)

The finite-stage universal differential applied to an element of the original source.

Theorem FoxDifferential.zcCompletedDifferentialModuleStageDifferential_one GitHub

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

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

Show proof

Theorem FoxDifferential.zcCompletedDifferentialModuleStageBoundary_isCrossedDifferential GitHub

theorem zcCompletedDifferentialModuleStageBoundary_isCrossedDifferential
    (i : ZCCompletedDifferentialModuleIndex C ψ) :
    IsCrossedDifferential (zcCompletedDifferentialModuleStageScalar C ψ i)
      (fun q : zcCompletedDifferentialModuleStageSource C ψ i =>
        zcCompletedDifferentialModuleStageScalar C ψ i q - 1)

The finite-stage boundary \(q \mapsto [q]-1\) is a crossed differential.

Show proof

Definition FoxDifferential.zcCompletedDifferentialModuleStageBoundary GitHub

def zcCompletedDifferentialModuleStageBoundary
    (i : ZCCompletedDifferentialModuleIndex C ψ) :
    ZCCompletedDifferentialModuleStage C ψ i →ₗ[zcCompletedDifferentialModuleStageRing C ψ i]
      zcCompletedDifferentialModuleStageRing C ψ i :=
  crossedDifferentialModuleLift
    (A := zcCompletedDifferentialModuleStageRing C ψ i)
    (zcCompletedDifferentialModuleStageScalar C ψ i)
    (fun q : zcCompletedDifferentialModuleStageSource C ψ i =>
      zcCompletedDifferentialModuleStageScalar C ψ i q - 1)
    (zcCompletedDifferentialModuleStageBoundary_isCrossedDifferential C ψ i)

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

Theorem FoxDifferential.zcCompletedDifferentialModuleStageBoundary_differential GitHub

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

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

Show proof

Definition FoxDifferential.zcCompletedDifferentialModuleStageBoundaryCompletedLinearMap GitHub

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

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

Theorem FoxDifferential.zcCompletedDifferentialModuleStageBoundaryCompletedLinearMap_apply GitHub

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

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

Show proof

Theorem FoxDifferential.zcCompletedDifferentialModuleStage_completed_smul GitHub

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

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

Show proof

Theorem FoxDifferential.zcCompletedDifferentialModuleStage_completed_groupLike_smul GitHub

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

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

Show proof

Theorem FoxDifferential.zcCompletedDifferentialModuleStageDifferential_isCrossedDifferential GitHub

theorem zcCompletedDifferentialModuleStageDifferential_isCrossedDifferential
    (i : ZCCompletedDifferentialModuleIndex C ψ) :
    IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ)
      (zcCompletedDifferentialModuleStageDifferential C ψ i)

The finite-stage differential is a crossed differential after restricting scalars from the completed group algebra to the finite stage ring.

Show proof

Definition FoxDifferential.zcCompletedDifferentialModuleStageProjection GitHub

def zcCompletedDifferentialModuleStageProjection
    (i : ZCCompletedDifferentialModuleIndex C ψ) :
    ZCCompletedDifferentialModule C ψ →ₗ[ZCCompletedGroupAlgebra C H]
      ZCCompletedDifferentialModuleStage C ψ i :=
  zcCompletedDifferentialModuleLift (A := ZCCompletedDifferentialModuleStage C ψ i)
    C ψ (zcCompletedDifferentialModuleStageDifferential C ψ i)
    (zcCompletedDifferentialModuleStageDifferential_isCrossedDifferential C ψ i)

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

Theorem FoxDifferential.zcCompletedDifferentialModuleStageProjection_universal GitHub

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

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

Show proof

Theorem FoxDifferential.zcDiffModuleIdentitySourceStageToStage_stageProj_universal GitHub

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)

The identity-source stage of the \(\mathbb{Z}_C\)-completed differential module is identified with its finite source and target coordinates.

Show proof

Theorem FoxDifferential.zcCompletedDifferentialModuleStageProjection_mkQ GitHub

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

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

Show proof

Definition FoxDifferential.zcCompletedDifferentialModulePreStageMap GitHub

def zcCompletedDifferentialModulePreStageMap
    (i : ZCCompletedDifferentialModuleIndex C ψ) :
    CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G →ₗ[ZCCompletedGroupAlgebra C H]
      CrossedDifferentialPreModule
        (zcCompletedDifferentialModuleStageRing C ψ i)
        (zcCompletedDifferentialModuleStageSource C ψ i) :=
  (Finsupp.lmapDomain
      (zcCompletedDifferentialModuleStageRing C ψ i)
      (ZCCompletedGroupAlgebra C H)
      (zcCompletedDifferentialModuleStageSourceProj C ψ i)).comp
    (Finsupp.mapRange.linearMap
      (α := G) (zcCompletedGroupAlgebraProjectionLinearMap C H i.target))

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

Theorem FoxDifferential.zcCompletedDifferentialModulePreStageMap_single GitHub

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)

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

Show proof

Theorem FoxDifferential.zcCompletedDifferentialModulePreStageMap_relationElement GitHub

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)

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

Show proof

Theorem FoxDifferential.zcCompletedDifferentialModulePreStageMap_relationSubmodule_surjective GitHub

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

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

Show proof

Theorem FoxDifferential.zcCompletedDifferentialModulePreStageMap_mkQ GitHub

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

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.

Show proof

Theorem FoxDifferential.zcDiffModuleStageBoundaryCompletedLinearMap_comp_stageProj GitHub

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

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.

Show proof

Theorem FoxDifferential.zcDiffModuleIdentitySourceStageProj_eq_zero_of_boundary_eq_zero GitHub

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

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

Show proof

Theorem FoxDifferential.zcDiffModuleIdentitySourceStageProj_eq_zero_of_zcTo_eq_zero GitHub

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

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

Show proof

Definition FoxDifferential.zcCompletedDifferentialModuleStageSourceTransition GitHub

def zcCompletedDifferentialModuleStageSourceTransition
    {i j : ZCCompletedDifferentialModuleIndex C ψ} (hij : i ≤ j) :
    zcCompletedDifferentialModuleStageSource C ψ j →*
      zcCompletedDifferentialModuleStageSource C ψ i :=
  OpenNormalSubgroupInClass.map (C := C) (G := G) hij.1

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

Theorem FoxDifferential.zcCompletedDifferentialModuleStageSourceTransition_coe GitHub

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)

The finite-stage transition maps compose compatibly along chains of quotient refinements.

Show proof

Theorem FoxDifferential.zcCompletedDifferentialModuleStageSourceTransition_mk GitHub

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

The finite-stage transition maps compose compatibly along chains of quotient refinements.

Show proof

Theorem FoxDifferential.zcCompletedDifferentialModuleStageSourceTransition_sourceProj GitHub

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

The finite-stage transition maps compose compatibly along chains of quotient refinements.

Show proof

Theorem FoxDifferential.zcCompletedDifferentialModuleStageSourceTransition_id GitHub

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

The finite-stage transition maps compose compatibly along chains of quotient refinements.

Show proof

Theorem FoxDifferential.zcCompletedDifferentialModuleStageSourceTransition_comp GitHub

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

The finite-stage transition maps compose compatibly along chains of quotient refinements.

Show proof

Definition FoxDifferential.zcCompletedDifferentialModuleStageTargetTransition GitHub

def zcCompletedDifferentialModuleStageTargetTransition
    {i j : ZCCompletedDifferentialModuleIndex C ψ} (hij : i ≤ j) :
    zcCompletedDifferentialModuleStageTarget C ψ j →*
      zcCompletedDifferentialModuleStageTarget C ψ i :=
  OpenNormalSubgroupInClass.map (C := C) (G := H)
    (U := OrderDual.ofDual i.target.2) (V := OrderDual.ofDual j.target.2) hij.2.2

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

Theorem FoxDifferential.zcCompletedDifferentialModuleStageTargetTransition_coe GitHub

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)

The finite-stage transition maps compose compatibly along chains of quotient refinements.

Show proof

Theorem FoxDifferential.zcCompletedDifferentialModuleStageTargetTransition_mk GitHub

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

The finite-stage transition maps compose compatibly along chains of quotient refinements.

Show proof

Theorem FoxDifferential.zcCompletedDifferentialModuleStageTargetTransition_id GitHub

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

The finite-stage transition maps compose compatibly along chains of quotient refinements.

Show proof

Theorem FoxDifferential.zcCompletedDifferentialModuleStageTargetTransition_comp GitHub

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

The finite-stage transition maps compose compatibly along chains of quotient refinements.

Show proof

Theorem FoxDifferential.zcCompletedDifferentialModuleStagePsi_transition GitHub

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)

The finite-stage transition maps compose compatibly along chains of quotient refinements.

Show proof

Theorem FoxDifferential.zcCompletedDifferentialModuleStageScalar_transition GitHub

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)

The finite-stage transition maps compose compatibly along chains of quotient refinements.

Show proof

Definition FoxDifferential.zcCompletedDifferentialModulePreStageTransition GitHub

def zcCompletedDifferentialModulePreStageTransition
    {i j : ZCCompletedDifferentialModuleIndex C ψ} (hij : i ≤ j) :
    CrossedDifferentialPreModule
        (zcCompletedDifferentialModuleStageRing C ψ j)
        (zcCompletedDifferentialModuleStageSource C ψ j) →+
      CrossedDifferentialPreModule
        (zcCompletedDifferentialModuleStageRing C ψ i)
        (zcCompletedDifferentialModuleStageSource C ψ i) :=
  (Finsupp.lmapDomain
      (zcCompletedDifferentialModuleStageRing C ψ i) ℤ
      (zcCompletedDifferentialModuleStageSourceTransition C ψ hij)).toAddMonoidHom.comp
    (Finsupp.mapRange.addMonoidHom
      (zcCompletedGroupAlgebraTransition C H hij.2).toAddMonoidHom)

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

Theorem FoxDifferential.zcCompletedDifferentialModulePreStageTransition_single GitHub

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)

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

Show proof

Theorem FoxDifferential.zcCompletedDifferentialModulePreStageTransition_preStageMap GitHub

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

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

Show proof

Theorem FoxDifferential.zcCompletedDifferentialModuleStageTransition_delta_isCrossedDifferential GitHub

theorem zcCompletedDifferentialModuleStageTransition_delta_isCrossedDifferential
    {i j : ZCCompletedDifferentialModuleIndex C ψ} (hij : i ≤ j) :
    letI : Module (zcCompletedDifferentialModuleStageRing C ψ j)
        (ZCCompletedDifferentialModuleStage C ψ i)

The finite-stage transition maps compose compatibly along chains of quotient refinements.

Show proof

Definition FoxDifferential.zcCompletedDifferentialModuleStageTransition GitHub

def zcCompletedDifferentialModuleStageTransition
    {i j : ZCCompletedDifferentialModuleIndex C ψ} (hij : i ≤ j) :
    ZCCompletedDifferentialModuleStage C ψ j →+
      ZCCompletedDifferentialModuleStage C ψ i := by
  letI : Module (zcCompletedDifferentialModuleStageRing C ψ j)
      (ZCCompletedDifferentialModuleStage C ψ i) :=
    Module.compHom _ (zcCompletedGroupAlgebraTransition C H hij.2)
  exact
    (crossedDifferentialModuleLift
      (A := ZCCompletedDifferentialModuleStage C ψ i)
      (zcCompletedDifferentialModuleStageScalar C ψ j)
      (fun x : zcCompletedDifferentialModuleStageSource C ψ j =>
        universalCrossedDifferential (zcCompletedDifferentialModuleStageScalar C ψ i)
          (zcCompletedDifferentialModuleStageSourceTransition C ψ hij x))
      (zcCompletedDifferentialModuleStageTransition_delta_isCrossedDifferential
        C ψ hij)).toAddMonoidHom

Transition maps compose compatibly along refinements of finite quotients.

Theorem FoxDifferential.zcCompletedDifferentialModuleStageTransition_universal GitHub

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

The finite-stage transition maps compose compatibly along chains of quotient refinements.

Show proof

Theorem FoxDifferential.zcCompletedDifferentialModulePreStageTransition_mkQ GitHub

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)

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

Show proof

Theorem FoxDifferential.zcCompletedDifferentialModulePreStageTransition_mem_relationSubmodule GitHub

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)

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

Show proof

Theorem FoxDifferential.zcCompletedDifferentialModulePreStageTransition_id GitHub

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

The finite-stage transition maps compose compatibly along chains of quotient refinements.

Show proof

Theorem FoxDifferential.zcCompletedDifferentialModulePreStageTransition_comp GitHub

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)

The finite-stage transition maps compose compatibly along chains of quotient refinements.

Show proof

Theorem FoxDifferential.zcCompletedDifferentialModuleFiniteRelationReductions_finiteStageApproximation GitHub

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

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.

Show proof

Theorem FoxDifferential.zcCompletedDifferentialModuleStageTransition_comp_projection GitHub

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)

The finite-stage transition maps compose compatibly along chains of quotient refinements.

Show proof

Theorem FoxDifferential.zcCompletedDifferentialModuleStageTransition_id GitHub

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

The finite-stage transition maps compose compatibly along chains of quotient refinements.

Show proof

Theorem FoxDifferential.zcCompletedDifferentialModuleStageTransition_comp GitHub

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)

The finite-stage transition maps compose compatibly along chains of quotient refinements.

Show proof

FoxDifferential.Completed.Continuous.Universal.FiniteStage

Declarations