Module

RelationModule.lean

Nyll.ProCGroups.FoxDifferential.Completed.FiniteStage.RelationModule

14 declarations indexed from sourceView source ↗

Module documentation

Fox differential: completed — finite stage — relation module

The principal declarations in this module are:

foxAlgebraicStageRelationGroup

The finite-stage relation group \(\ker(F/[N,N]N^n \to F/N)\). Its elements are exactly finite-stage kernel relations.

foxAlgebraicStageRelationBoundaryAddMonoidHom

The finite-stage relation boundary, written additively: \(N/[N,N]N^n \to ((\mathbb{Z}/n\mathbb{Z})[F/N])^X\).

foxAlgebraicStageRelationGroup_target_eq_one

Every finite-stage relation group element maps to \(1\) in the target normal quotient.

foxAlgebraicStageQuotientCoefficient_relation_eq_one

Every finite-stage relation group element has quotient coefficient equal to \(1\).

Imports1

Nyll.ProCGroups.FoxDifferential.Completed.FiniteStage.BoundaryCycles

Imported by2

abbrev

foxAlgebraicStageRelationGroup

L42 ↗

FoxDifferential.foxAlgebraicStageRelationGroup

Documentation

The finite-stage relation group \(\ker(F/[N,N]N^n \to F/N)\). Its elements are exactly finite-stage kernel relations.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)

Lean source · statement

abbrev foxAlgebraicStageRelationGroup : Type u

theorem

foxAlgebraicStageRelationGroup_target_eq_one

L49 ↗

FoxDifferential.foxAlgebraicStageRelationGroup_target_eq_one

Documentation

Every finite-stage relation group element maps to \(1\) in the target normal quotient.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)
omit [DecidableEq X] in

Lean source · statement

theorem foxAlgebraicStageRelationGroup_target_eq_one
    (q : foxAlgebraicStageRelationGroup (X := X) N n) :
    foxCommutatorPowerQuotientMapToNormalQuotient
      (F := FreeGroup X) N n q.1 = 1

theorem

foxAlgebraicStageQuotientCoefficient_relation_eq_one

L58 ↗

FoxDifferential.foxAlgebraicStageQuotientCoefficient_relation_eq_one

Documentation

Every finite-stage relation group element has quotient coefficient equal to \(1\).

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)
omit [DecidableEq X] in

Lean source · statement

theorem foxAlgebraicStageQuotientCoefficient_relation_eq_one
    (q : foxAlgebraicStageRelationGroup (X := X) N n) :
    foxAlgebraicStageQuotientCoefficient (X := X) N n q.1 = 1

def

foxAlgebraicStageRelationBoundaryAddMonoidHom

L67 ↗

FoxDifferential.foxAlgebraicStageRelationBoundaryAddMonoidHom

Documentation

The finite-stage relation boundary, written additively: \(N/[N,N]N^n \to ((\mathbb{Z}/n\mathbb{Z})[F/N])^X\).

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)

Lean source · full declaration

def foxAlgebraicStageRelationBoundaryAddMonoidHom :
    Additive (foxAlgebraicStageRelationGroup (X := X) N n) →+
      foxAlgebraicStageCoordinateVector (X := X) N n where
  toFun q := foxAlgebraicStageQuotientDerivativeVector (X := X) N n
    (Additive.toMul q).1
  map_zero' := by
    change foxAlgebraicStageQuotientDerivativeVector (X := X) N n 1 = 0
    exact ScalarCrossedHom.map_one
      (foxAlgebraicStageQuotientDerivativeVector (X := X) N n)
  map_add' := by
    intro q r
    change foxAlgebraicStageQuotientDerivativeVector (X := X) N n
        ((Additive.toMul q).1 * (Additive.toMul r).1) =
      foxAlgebraicStageQuotientDerivativeVector (X := X) N n (Additive.toMul q).1 +
        foxAlgebraicStageQuotientDerivativeVector (X := X) N n (Additive.toMul r).1
    rw [ScalarCrossedHom.map_mul
      (foxAlgebraicStageQuotientDerivativeVector (X := X) N n),
      foxAlgebraicStageQuotientCoefficient_relation_eq_one]
    simp only [one_smul]

theorem

foxAlgebraicStageRelationBoundaryAddMonoidHom_of

L92 ↗

FoxDifferential.foxAlgebraicStageRelationBoundaryAddMonoidHom_of

Documentation

The relation-boundary add monoid homomorphism is evaluated on a finite-stage relation by the defining boundary formula.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)

Lean source · statement

theorem foxAlgebraicStageRelationBoundaryAddMonoidHom_of
    (q : foxAlgebraicStageRelationGroup (X := X) N n) :
    foxAlgebraicStageRelationBoundaryAddMonoidHom (X := X) N n (Additive.ofMul q) =
      foxAlgebraicStageQuotientDerivativeVector (X := X) N n q.1

def

foxAlgebraicStageRelationBoundaryRange

L99 ↗

FoxDifferential.foxAlgebraicStageRelationBoundaryRange

Documentation

The relation-boundary image, as an additive subgroup of the finite coordinate module.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)

Lean source · statement

def foxAlgebraicStageRelationBoundaryRange :
    AddSubgroup (foxAlgebraicStageCoordinateVector (X := X) N n)

theorem

foxAlgebraicStageRelationBoundaryRange_coe

L108 ↗

FoxDifferential.foxAlgebraicStageRelationBoundaryRange_coe

Documentation

The relation-boundary range has the finite-stage source-kernel derivative set as its underlying set.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)

Lean source · statement

theorem foxAlgebraicStageRelationBoundaryRange_coe :
    ((foxAlgebraicStageRelationBoundaryRange (X := X) N n :
        AddSubgroup (foxAlgebraicStageCoordinateVector (X := X) N n)) :
          Set (foxAlgebraicStageCoordinateVector (X := X) N n)) =
      foxAlgebraicStageSourceKernelDerivativeSet (X := X) N n

theorem

mem_foxAlgebraicStageRelationBoundaryRange_iff

L119 ↗

FoxDifferential.mem_foxAlgebraicStageRelationBoundaryRange_iff

Documentation

Membership in the finite-stage relation-boundary range is equivalent to the displayed coordinate condition.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)

Lean source · statement

theorem mem_foxAlgebraicStageRelationBoundaryRange_iff
    {N : Subgroup (FreeGroup X)} [N.Normal] {n : ℕ}
    {v : foxAlgebraicStageCoordinateVector (X := X) N n} :
    v ∈ foxAlgebraicStageRelationBoundaryRange (X := X) N n ↔
      ∃ q : Additive (foxAlgebraicStageRelationGroup (X := X) N n),
        foxAlgebraicStageRelationBoundaryAddMonoidHom (X := X) N n q = v

theorem

foxAlgebraicStageFoxBoundary_relationBoundary_eq_zero

L140 ↗

FoxDifferential.foxAlgebraicStageFoxBoundary_relationBoundary_eq_zero

Documentation

The finite-stage relation boundary lands in finite Fox boundary cycles.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)

Lean source · statement

theorem foxAlgebraicStageFoxBoundary_relationBoundary_eq_zero
    [Fintype X] (q : Additive (foxAlgebraicStageRelationGroup (X := X) N n)) :
    foxAlgebraicStageFoxBoundary (X := X) N n
      (foxAlgebraicStageRelationBoundaryAddMonoidHom (X := X) N n q) = 0

theorem

foxAlgebraicStageRelationBoundary_range_le_boundaryCycleSubmodule

L153 ↗

FoxDifferential.foxAlgebraicStageRelationBoundary_range_le_boundaryCycleSubmodule

Documentation

The relation-boundary range is contained in \(\ker \partial\).

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)

Lean source · statement

theorem foxAlgebraicStageRelationBoundary_range_le_boundaryCycleSubmodule
    [Fintype X] :
    foxAlgebraicStageRelationBoundaryRange (X := X) N n ≤
      (foxAlgebraicStageBoundaryCycleSubmodule (X := X) N n).toAddSubgroup

def

foxAlgebraicStageRelationBoundaryExact

L164 ↗

FoxDifferential.foxAlgebraicStageRelationBoundaryExact

Documentation

Finite-stage exactness at the coordinate module.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)

Lean source · statement

def foxAlgebraicStageRelationBoundaryExact [Fintype X] : Prop

theorem

foxAlgebraicStageRelationBoundaryExact_iff_boundaryCyclesCoveredBySourceKernel

L173 ↗

FoxDifferential.foxAlgebraicStageRelationBoundaryExact_iff_boundaryCyclesCoveredBySourceKernel

Documentation

Finite-stage exactness is equivalent to the coverage statement formulated at the level of finite-stage boundary cycles.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)

Lean source · statement

theorem foxAlgebraicStageRelationBoundaryExact_iff_boundaryCyclesCoveredBySourceKernel
    {N : Subgroup (FreeGroup X)} [N.Normal] {n : ℕ} [Fintype X] :
    foxAlgebraicStageRelationBoundaryExact (X := X) N n ↔
      foxAlgebraicStageBoundaryCyclesCoveredBySourceKernel (X := X) N n

theorem

foxAlgebraicStageRelationBoundaryExact_of_boundaryCyclesCoveredBySourceKernel

L205 ↗

FoxDifferential.foxAlgebraicStageRelationBoundaryExact_of_boundaryCyclesCoveredBySourceKernel

Documentation

Coverage of finite boundary cycles gives finite-stage exactness in the usual function-level form.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)

Lean source · statement

theorem foxAlgebraicStageRelationBoundaryExact_of_boundaryCyclesCoveredBySourceKernel
    [Fintype X]
    (hcovered : foxAlgebraicStageBoundaryCyclesCoveredBySourceKernel (X := X) N n) :
    foxAlgebraicStageRelationBoundaryExact (X := X) N n

theorem

foxAlgebraicStageBoundaryCyclesCoveredBySourceKernel_of_relationBoundaryExact

L213 ↗

FoxDifferential.foxAlgebraicStageBoundaryCyclesCoveredBySourceKernel_of_relationBoundaryExact

Documentation

Function-level finite-stage exactness gives the set-level coverage used by the density step.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)

Lean source · statement

theorem foxAlgebraicStageBoundaryCyclesCoveredBySourceKernel_of_relationBoundaryExact
    [Fintype X]
    (hexact : foxAlgebraicStageRelationBoundaryExact (X := X) N n) :
    foxAlgebraicStageBoundaryCyclesCoveredBySourceKernel (X := X) N n

Module documentation

Fox differential: completed — finite stage — relation module

Declarations