ModuleBasic.lean
Nyll.ProCGroups.FoxDifferential.Completed.DifferentialModule.TargetQuotient.Basic
3 declarations indexed from sourceView source ↗ Module documentation
Fox differential: completed — differential module — target quotient — basic
The principal declarations in this module are:
foxAlgebraicStageTargetQuotientContinuousMonoidHom
The completed Fox-differential map is continuous with respect to the inverse-limit topology on the completed coefficient modules.
foxAlgebraicStageTargetQuotientContinuousMonoidHom_apply
The finite-stage target quotient homomorphism sends a word to its quotient class modulo \(N\).
foxAlgebraicStagePrimePowerSourceCompletedIndex_le_targetQuotientComap
The completed free derivative source finite stage \([N,N]N^{ell^a}\) refines every finite stage pulled back from the target quotient \(F/N\). This order comparison lets the completed group-algebra projection for \(\pi: \mathbb{Z}_{\ell}\llbracket F\rrbracket \to \mathbb{Z}_{\ell}\llbracket F/N\rrbracket\) be computed from the completed free derivative source projection.
Declarations
FoxDifferential.foxAlgebraicStageTargetQuotientContinuousMonoidHom
DocumentationThe completed Fox-differential map is continuous with respect to the inverse-limit topology on the completed coefficient modules.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups
open ProCGroups.ProC
universe u v
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {X : Type u} [DecidableEq X]
FoxDifferential.foxAlgebraicStageTargetQuotientContinuousMonoidHom_apply
DocumentationThe finite-stage target quotient homomorphism sends a word to its quotient class modulo \(N\).
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups
open ProCGroups.ProC
universe u v
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {X : Type u} [DecidableEq X]
omit [DecidableEq X] in
FoxDifferential.foxAlgebraicStagePrimePowerSourceCompletedIndex_le_targetQuotientComap
DocumentationThe completed free derivative source finite stage \([N,N]N^{ell^a}\) refines every finite stage pulled back from the target quotient \(F/N\). This order comparison lets the completed group-algebra projection for \(\pi: \mathbb{Z}_{\ell}\llbracket F\rrbracket \to \mathbb{Z}_{\ell}\llbracket F/N\rrbracket\) be computed from the completed free derivative source projection.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups
open ProCGroups.ProC
universe u v
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {X : Type u} [DecidableEq X]
omit [DecidableEq X] [Fact (0 < ℓ)] in