Module

RelationIdeal.lean

Nyll.ProCGroups.FoxDifferential.Completed.FiniteStage.RelationIdeal

13 declarations indexed from sourceView source ↗

Module documentation

Fox differential: completed — finite stage — relation ideal

The principal declarations in this module are:

foxAlgebraicStageRelationAugmentationGenerator

The augmentation generator \(q-1\) attached to a finite-stage relation \(q \in \ker(F/[N,N]N^n \to F/N)\).

foxAlgebraicStageRelationAugmentationIdeal

The source group-algebra ideal generated by finite-stage relation augmentation generators.

foxAlgebraicStageRelationAugmentationGenerator_mem_relationAugmentationIdeal

A finite-stage relation augmentation generator belongs to the relation augmentation ideal.

foxAlgebraicStageRelationAugmentationGenerator_mem_groupAlgebraMapKernel

A relation augmentation generator maps to zero in the target group algebra.

Imports2

Imported by2

def

foxAlgebraicStageRelationAugmentationGenerator

L42 ↗

FoxDifferential.foxAlgebraicStageRelationAugmentationGenerator

Documentation

The augmentation generator \(q-1\) attached to a finite-stage relation \(q \in \ker(F/[N,N]N^n \to F/N)\).

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 foxAlgebraicStageRelationAugmentationGenerator
    (q : foxAlgebraicStageRelationGroup (X := X) N n) :
    foxAlgebraicStageSourceGroupAlgebra (X := X) N n

def

foxAlgebraicStageRelationAugmentationIdeal

L49 ↗

FoxDifferential.foxAlgebraicStageRelationAugmentationIdeal

Documentation

The source group-algebra ideal generated by finite-stage relation augmentation generators.

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 foxAlgebraicStageRelationAugmentationIdeal :
    Ideal (foxAlgebraicStageSourceGroupAlgebra (X := X) N n)

theorem

foxAlgebraicStageRelationAugmentationGenerator_mem_relationAugmentationIdeal

L56 ↗

FoxDifferential.foxAlgebraicStageRelationAugmentationGenerator_mem_relationAugmentationIdeal

Documentation

A finite-stage relation augmentation generator belongs to the relation augmentation ideal.

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 foxAlgebraicStageRelationAugmentationGenerator_mem_relationAugmentationIdeal
    (q : foxAlgebraicStageRelationGroup (X := X) N n) :
    foxAlgebraicStageRelationAugmentationGenerator (X := X) N n q ∈
      foxAlgebraicStageRelationAugmentationIdeal (X := X) N n

theorem

foxAlgebraicStageRelationAugmentationGenerator_mem_groupAlgebraMapKernel

L64 ↗

FoxDifferential.foxAlgebraicStageRelationAugmentationGenerator_mem_groupAlgebraMapKernel

Documentation

A relation augmentation generator maps to zero in the target group algebra.

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 foxAlgebraicStageRelationAugmentationGenerator_mem_groupAlgebraMapKernel
    (q : foxAlgebraicStageRelationGroup (X := X) N n) :
    foxAlgebraicStageRelationAugmentationGenerator (X := X) N n q ∈
      foxAlgebraicStageGroupAlgebraMapKernelIdeal (X := X) N n

theorem

foxAlgebraicStageRelationAugmentationIdeal_le_groupAlgebraMapKernel

L81 ↗

FoxDifferential.foxAlgebraicStageRelationAugmentationIdeal_le_groupAlgebraMapKernel

Documentation

The generated relation augmentation ideal is contained in the kernel of the source-to-target finite group-algebra map.

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 foxAlgebraicStageRelationAugmentationIdeal_le_groupAlgebraMapKernel :
    foxAlgebraicStageRelationAugmentationIdeal (X := X) N n ≤
      foxAlgebraicStageGroupAlgebraMapKernelIdeal (X := X) N n

def

foxAlgebraicStageTargetGroupAlgebraSection

L93 ↗

FoxDifferential.foxAlgebraicStageTargetGroupAlgebraSection

Documentation

A section of the source-to-target finite group-algebra map, obtained by choosing a source quotient lift for each target quotient basis element. This is only a \(\mathbb{Z}/n\mathbb{Z}\)-linear section; no multiplicativity is asserted.

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 foxAlgebraicStageTargetGroupAlgebraSection :
    foxAlgebraicStageTargetGroupAlgebra (X := X) N n →ₗ[ModNCompletedCoeff n]
      foxAlgebraicStageSourceGroupAlgebra (X := X) N n

theorem

foxAlgebraicStageTargetGroupAlgebraSection_of

L109 ↗

FoxDifferential.foxAlgebraicStageTargetGroupAlgebraSection_of

Documentation

The finite-stage target group-algebra section sends a group-like quotient element to the chosen lifted group-like element.

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 foxAlgebraicStageTargetGroupAlgebraSection_of
    (h : foxAlgebraicStageTargetQuotient (X := X) N) :
    foxAlgebraicStageTargetGroupAlgebraSection (X := X) N n
      (MonoidAlgebra.of (ModNCompletedCoeff n)
        (foxAlgebraicStageTargetQuotient (X := X) N) h) =
      MonoidAlgebra.of (ModNCompletedCoeff n)
        (FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n)
        (foxAlgebraicStageTargetQuotientLiftToSource (X := X) N n h)

theorem

foxCommutatorPowerGroupAlgebraMap_section

L128 ↗

FoxDifferential.foxCommutatorPowerGroupAlgebraMap_section

Documentation

The chosen group-algebra section is a right inverse to the finite source-to-target map.

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 foxCommutatorPowerGroupAlgebraMap_section
    (y : foxAlgebraicStageTargetGroupAlgebra (X := X) N n) :
    foxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n
        (foxAlgebraicStageTargetGroupAlgebraSection (X := X) N n y) = y

theorem

foxCommutatorPowerGroupAlgebraMap_surjective

L150 ↗

FoxDifferential.foxCommutatorPowerGroupAlgebraMap_surjective

Documentation

The finite source-to-target group-algebra map is surjective.

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 foxCommutatorPowerGroupAlgebraMap_surjective :
    Function.Surjective (foxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n)

theorem

foxAlgebraicStage_sourceBasis_sub_section_mem_relationAugmentationIdeal

L161 ↗

FoxDifferential.foxAlgebraicStage_sourceBasis_sub_section_mem_relationAugmentationIdeal

Documentation

A source basis element minus the chosen lift of its target image lies in the finite-stage relation augmentation ideal.

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 foxAlgebraicStage_sourceBasis_sub_section_mem_relationAugmentationIdeal
    (s : FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n) :
    MonoidAlgebra.of (ModNCompletedCoeff n)
        (FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n) s -
      foxAlgebraicStageTargetGroupAlgebraSection (X := X) N n
        (foxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n
          (MonoidAlgebra.of (ModNCompletedCoeff n)
            (FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n) s)) ∈
      foxAlgebraicStageRelationAugmentationIdeal (X := X) N n

theorem

foxAlgebraicStage_sub_section_map_mem_relationAugmentationIdeal

L214 ↗

FoxDifferential.foxAlgebraicStage_sub_section_map_mem_relationAugmentationIdeal

Documentation

Every finite-stage source group-algebra element minus the chosen lift of its target image lies in the relation augmentation ideal.

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 foxAlgebraicStage_sub_section_map_mem_relationAugmentationIdeal
    (x : foxAlgebraicStageSourceGroupAlgebra (X := X) N n) :
    x - foxAlgebraicStageTargetGroupAlgebraSection (X := X) N n
        (foxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n x) ∈
      foxAlgebraicStageRelationAugmentationIdeal (X := X) N n

theorem

foxAlgebraicStageGroupAlgebraMapKernelIdeal_eq_relationAugmentationIdeal

L256 ↗

FoxDifferential.foxAlgebraicStageGroupAlgebraMapKernelIdeal_eq_relationAugmentationIdeal

Documentation

The kernel ideal of the finite source-to-target group-algebra map is exactly the ideal spanned by relation augmentation generators.

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 foxAlgebraicStageGroupAlgebraMapKernelIdeal_eq_relationAugmentationIdeal :
    foxAlgebraicStageGroupAlgebraMapKernelIdeal (X := X) N n =
      foxAlgebraicStageRelationAugmentationIdeal (X := X) N n

theorem

foxAlgebraicStage_mem_groupAlgebraMapKernelIdeal_iff_relationAugmentationIdeal

L275 ↗

FoxDifferential.foxAlgebraicStage_mem_groupAlgebraMapKernelIdeal_iff_relationAugmentationIdeal

Documentation

At a finite Fox stage, membership in the source-to-target group-algebra map kernel ideal is equivalent to membership in the relation augmentation ideal.

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 foxAlgebraicStage_mem_groupAlgebraMapKernelIdeal_iff_relationAugmentationIdeal
    {N : Subgroup (FreeGroup X)} [N.Normal] {n : ℕ}
    {x : foxAlgebraicStageSourceGroupAlgebra (X := X) N n} :
    x ∈ foxAlgebraicStageGroupAlgebraMapKernelIdeal (X := X) N n ↔
      x ∈ foxAlgebraicStageRelationAugmentationIdeal (X := X) N n

Module documentation

Fox differential: completed — finite stage — relation ideal

Declarations