Yamaguchi Lean 4 Library
FoxDifferential.Completed.FiniteStage
FoxDifferential/Completed/FiniteStage

FoxDifferential.Completed.FiniteStage

22 sections | 77 files | 567 declarations

This module develops Fox differentials and completed Fox coordinates for free, profinite, and pro-\(C\) group constructions.

Basic

1 files | 17 declarations | 10 Theorem | 6 Definition | 1 Instance
The finite-stage completed group-algebra projection preserves coefficient algebra maps.

Bifiltered

4 files | 29 declarations | 18 Theorem | 8 Definition | 1 Abbreviation | 2 Instance
Finite quotient stages are used to compare completed Fox boundaries, derivatives, and relation modules with explicit finite group-algebra calculations.

BoundaryCycleHom

1 files | 8 declarations | 5 Theorem | 2 Definition | 1 Abbreviation
The kernel of the finite source-to-target quotient \(F/[N,N]N^n \to F/N\).

BoundaryCycles

1 files | 15 declarations | 9 Theorem | 6 Definition
The finite-stage Fox boundary-cycle submodule \(\ker \partial\).

BoundaryQuotient

1 files | 6 declarations | 4 Theorem | 1 Definition | 1 Abbreviation
Finite coordinate vectors modulo the submodule generated by finite relation boundaries.

BoundarySubgroups

1 files | 7 declarations | 5 Theorem | 2 Definition
Finite semidirect boundary cycles form a subgroup.

CoeffMap

7 files | 32 declarations | 27 Theorem | 5 Definition
Fox Differential / Completed / Finite Stage / Coefficient Map.

MagnusQuotient

1 files | 15 declarations | 14 Theorem | 1 Definition
Reindex the finite-stage Fox semidirect target along an equivalence of free bases.

PrimePower

31 files | 164 declarations | 109 Theorem | 28 Definition | 6 Abbreviation | 21 Instance
Wrapper for the `FoxDifferential.Completed.FiniteStage.PrimePower` folder.

RelationAction

1 files | 8 declarations | 6 Theorem | 2 Definition
Conjugating a finite-stage relation by an arbitrary source-quotient element gives another finite-stage relation.

RelationIdeal

1 files | 13 declarations | 10 Theorem | 3 Definition
The augmentation generator \(q-1\) attached to a finite-stage relation \(q \in \ker(F/[N,N]N^n \to F/N)\).

RelationIdealDerivative

1 files | 16 declarations | 15 Theorem | 1 Definition
The vector of target-valued finite Fox derivatives of a source group-algebra element.

RelationIdealPrimitive

1 files | 20 declarations | 15 Theorem | 5 Definition
An element of the source finite group algebra has a relation-compatible source Fox primitive if it is the source boundary of a vector whose target projection lies in the finite ...

RelationModule

1 files | 14 declarations | 10 Theorem | 3 Definition | 1 Abbreviation
The finite-stage relation group \(\ker(F/[N,N]N^n \to F/N)\). Its elements are exactly finite-stage kernel relations.

RelationRealization

1 files | 5 declarations | 5 Theorem
The additive source-kernel derivative set is closed under integer multiples.

RelationSubmodule

1 files | 14 declarations | 11 Theorem | 3 Definition
The \((\mathbb{Z}/n\mathbb{Z})[F/N]\)-submodule generated by finite-stage relation-boundary vectors.

SemidirectCycles

1 files | 16 declarations | 10 Theorem | 6 Definition
The finite semidirect point \((Dq,1)\) attached to a source-quotient element.

SourceBoundary

1 files | 15 declarations | 11 Theorem | 3 Definition | 1 Abbreviation
Source-valued coordinate vectors over \((\mathbb{Z}/n\mathbb{Z})[F/([N,N]N^n)]\).

SourceCycleReduction

1 files | 9 declarations | 6 Theorem | 3 Definition
Source boundary cycles in the source coordinate module.

SourceDerivativeVector

1 files | 9 declarations | 7 Theorem | 2 Definition
Source-valued derivative vector of a source quotient element.

Stage

17 files | 126 declarations | 92 Theorem | 25 Definition | 4 Abbreviation | 1 Structure | 4 Instance
Finite quotient stages are used to compare completed Fox boundaries, derivatives, and relation modules with explicit finite group-algebra calculations.

TargetMap

1 files | 9 declarations | 9 Theorem
The left coordinate of the finite-stage semidirect point is the specified derivative component.