Module

RelationSubmodule.lean

Nyll.ProCGroups.FoxDifferential.Completed.FiniteStage.RelationSubmodule

14 declarations indexed from sourceView source ↗

Module documentation

Fox differential: completed — finite stage — relation submodule

The principal declarations in this module are:

foxAlgebraicStageRelationBoundarySubmodule

The \((\mathbb{Z}/n\mathbb{Z})[F/N]\)-submodule generated by finite-stage relation-boundary vectors.

foxAlgebraicStageRelationBoundaryImageSubmodule

The actual relation-boundary image as a finite group-algebra submodule.

foxAlgebraicStageRelationBoundaryRange_subset_relationBoundarySubmodule

Every actual relation-boundary vector lies in the generated relation-boundary submodule.

foxAlgebraicStageRelationBoundaryAddMonoidHom_mem_relationBoundarySubmodule

A relation boundary of a finite-stage relation lies in the generated submodule.

Imports1

Nyll.ProCGroups.FoxDifferential.Completed.FiniteStage.RelationAction

Imported by4

def

foxAlgebraicStageRelationBoundarySubmodule

L41 ↗

FoxDifferential.foxAlgebraicStageRelationBoundarySubmodule

Documentation

The \((\mathbb{Z}/n\mathbb{Z})[F/N]\)-submodule generated by finite-stage relation-boundary vectors.

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 foxAlgebraicStageRelationBoundarySubmodule :
    Submodule (foxAlgebraicStageTargetGroupAlgebra (X := X) N n)
      (foxAlgebraicStageCoordinateVector (X := X) N n)

theorem

foxAlgebraicStageRelationBoundaryRange_subset_relationBoundarySubmodule

L49 ↗

FoxDifferential.foxAlgebraicStageRelationBoundaryRange_subset_relationBoundarySubmodule

Documentation

Every actual relation-boundary vector lies in the generated relation-boundary submodule.

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_subset_relationBoundarySubmodule :
    (foxAlgebraicStageRelationBoundaryRange (X := X) N n :
      Set (foxAlgebraicStageCoordinateVector (X := X) N n)) ⊆
        foxAlgebraicStageRelationBoundarySubmodule (X := X) N n

theorem

foxAlgebraicStageRelationBoundaryAddMonoidHom_mem_relationBoundarySubmodule

L56 ↗

FoxDifferential.foxAlgebraicStageRelationBoundaryAddMonoidHom_mem_relationBoundarySubmodule

Documentation

A relation boundary of a finite-stage relation lies in the generated submodule.

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_mem_relationBoundarySubmodule
    (q : Additive (foxAlgebraicStageRelationGroup (X := X) N n)) :
    foxAlgebraicStageRelationBoundaryAddMonoidHom (X := X) N n q ∈
      foxAlgebraicStageRelationBoundarySubmodule (X := X) N n

theorem

foxAlgebraicStageRelationBoundaryRange_smul_mem

L65 ↗

FoxDifferential.foxAlgebraicStageRelationBoundaryRange_smul_mem

Documentation

The actual relation-boundary image is stable under arbitrary finite group-algebra scalars.

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_smul_mem
    (a : foxAlgebraicStageTargetGroupAlgebra (X := X) N n)
    {v : foxAlgebraicStageCoordinateVector (X := X) N n}
    (hv : v ∈ foxAlgebraicStageRelationBoundaryRange (X := X) N n) :
    a • v ∈ foxAlgebraicStageRelationBoundaryRange (X := X) N n

def

foxAlgebraicStageRelationBoundaryImageSubmodule

L113 ↗

FoxDifferential.foxAlgebraicStageRelationBoundaryImageSubmodule

Documentation

The actual relation-boundary image as a finite group-algebra submodule.

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 foxAlgebraicStageRelationBoundaryImageSubmodule :
    Submodule (foxAlgebraicStageTargetGroupAlgebra (X := X) N n)
      (foxAlgebraicStageCoordinateVector (X := X) N n) where
  carrier := foxAlgebraicStageRelationBoundaryRange (X := X) N n
  zero_mem' := (foxAlgebraicStageRelationBoundaryRange (X := X) N n).zero_mem
  add_mem' := by
    intro x y hx hy
    exact (foxAlgebraicStageRelationBoundaryRange (X := X) N n).add_mem hx hy
  smul_mem' := by
    intro a v hv
    exact foxAlgebraicStageRelationBoundaryRange_smul_mem (X := X) N n a hv

theorem

foxAlgebraicStageRelationBoundaryImageSubmodule_coe

L130 ↗

FoxDifferential.foxAlgebraicStageRelationBoundaryImageSubmodule_coe

Documentation

The relation-boundary image submodule 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 foxAlgebraicStageRelationBoundaryImageSubmodule_coe :
    ((foxAlgebraicStageRelationBoundaryImageSubmodule (X := X) N n :
        Submodule (foxAlgebraicStageTargetGroupAlgebra (X := X) N n)
          (foxAlgebraicStageCoordinateVector (X := X) N n)) :
          Set (foxAlgebraicStageCoordinateVector (X := X) N n)) =
      foxAlgebraicStageSourceKernelDerivativeSet (X := X) N n

theorem

foxAlgebraicStageRelationBoundarySubmodule_eq_imageSubmodule

L144 ↗

FoxDifferential.foxAlgebraicStageRelationBoundarySubmodule_eq_imageSubmodule

Documentation

The generated relation-boundary submodule is the actual relation-boundary image, because the image is already stable under the finite target group algebra.

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 foxAlgebraicStageRelationBoundarySubmodule_eq_imageSubmodule :
    foxAlgebraicStageRelationBoundarySubmodule (X := X) N n =
      foxAlgebraicStageRelationBoundaryImageSubmodule (X := X) N n

theorem

foxAlgebraicStageRelationBoundarySubmodule_le_boundaryCycleSubmodule

L156 ↗

FoxDifferential.foxAlgebraicStageRelationBoundarySubmodule_le_boundaryCycleSubmodule

Documentation

The relation-boundary submodule is contained in the 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 foxAlgebraicStageRelationBoundarySubmodule_le_boundaryCycleSubmodule
    [Fintype X] :
    foxAlgebraicStageRelationBoundarySubmodule (X := X) N n ≤
      foxAlgebraicStageBoundaryCycleSubmodule (X := X) N n

def

foxAlgebraicStageRelationBoundaryModuleExact

L168 ↗

FoxDifferential.foxAlgebraicStageRelationBoundaryModuleExact

Documentation

Module-level finite-stage exactness at the coordinate module: \(\ker\partial\) is contained in the submodule generated by finite relation boundaries.

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 foxAlgebraicStageRelationBoundaryModuleExact [Fintype X] : Prop

theorem

foxAlgebraicStageRelationBoundaryModuleExact_of_relationBoundaryExact

L173 ↗

FoxDifferential.foxAlgebraicStageRelationBoundaryModuleExact_of_relationBoundaryExact

Documentation

Function-level relation-boundary exactness implies the module-level finite exactness target.

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 foxAlgebraicStageRelationBoundaryModuleExact_of_relationBoundaryExact
    [Fintype X]
    (hexact : foxAlgebraicStageRelationBoundaryExact (X := X) N n) :
    foxAlgebraicStageRelationBoundaryModuleExact (X := X) N n

theorem

foxAlgebraicStageRelationBoundaryModuleExact_of_boundaryCyclesCoveredBySourceKernel

L190 ↗

FoxDifferential.foxAlgebraicStageRelationBoundaryModuleExact_of_boundaryCyclesCoveredBySourceKernel

Documentation

The set-level finite coverage target implies the module-level finite exactness target.

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 foxAlgebraicStageRelationBoundaryModuleExact_of_boundaryCyclesCoveredBySourceKernel
    [Fintype X]
    (hcovered : foxAlgebraicStageBoundaryCyclesCoveredBySourceKernel (X := X) N n) :
    foxAlgebraicStageRelationBoundaryModuleExact (X := X) N n

theorem

foxAlgebraicStageBoundaryCyclesCoveredBySourceKernel_of_relationBoundaryModuleExact

L206 ↗

FoxDifferential.foxAlgebraicStageBoundaryCyclesCoveredBySourceKernel_of_relationBoundaryModuleExact

Documentation

Module-level finite exactness is strong enough to recover the set-level source-kernel coverage, because the relation-boundary image is already a finite group-algebra submodule.

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_relationBoundaryModuleExact
    [Fintype X]
    (hexact : foxAlgebraicStageRelationBoundaryModuleExact (X := X) N n) :
    foxAlgebraicStageBoundaryCyclesCoveredBySourceKernel (X := X) N n

theorem

foxAlgebraicStageRelationBoundaryModuleExact_iff_submodule_eq_boundaryCycleSubmodule

L220 ↗

FoxDifferential.foxAlgebraicStageRelationBoundaryModuleExact_iff_submodule_eq_boundaryCycleSubmodule

Documentation

Module exactness is equivalent to equality between \(\ker \partial\) and the generated relation-boundary submodule.

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 foxAlgebraicStageRelationBoundaryModuleExact_iff_submodule_eq_boundaryCycleSubmodule
    {N : Subgroup (FreeGroup X)} [N.Normal] {n : ℕ} [Fintype X] :
    foxAlgebraicStageRelationBoundaryModuleExact (X := X) N n ↔
      foxAlgebraicStageRelationBoundarySubmodule (X := X) N n =
        foxAlgebraicStageBoundaryCycleSubmodule (X := X) N n

theorem

relationBoundarySubmodule_eq_boundaryCycleSubmodule_of_relExact

L238 ↗

FoxDifferential.relationBoundarySubmodule_eq_boundaryCycleSubmodule_of_relExact

Documentation

Function-level finite exactness identifies \(\ker \partial\) with the generated relation-boundary submodule.

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 relationBoundarySubmodule_eq_boundaryCycleSubmodule_of_relExact
    [Fintype X]
    (hexact : foxAlgebraicStageRelationBoundaryExact (X := X) N n) :
    foxAlgebraicStageRelationBoundarySubmodule (X := X) N n =
      foxAlgebraicStageBoundaryCycleSubmodule (X := X) N n

Module documentation

Fox differential: completed — finite stage — relation submodule

Declarations