ModuleSurjective.lean
Nyll.ProCGroups.FoxDifferential.Completed.DifferentialModule.TargetQuotient.Surjective
4 declarations indexed from sourceView source ↗ Module documentation
Fox differential: completed — differential module — target quotient — surjective
The principal declarations in this module are:
primePowerCompletedGroupAlgebraMap_targetQuotient_lift
A noncomputable lift of a completed target group-algebra coefficient to the source completed group algebra. The defining equation is \(\mathrm{primePowerCompletedGroupAlgebraMap\_targetQuotient\_lift\_spec}\).
foxAlgebraicStageTargetQuotientContinuousMonoidHom_surjective
The quotient homomorphism \(\mathrm{FreeGroup}(X) \to \mathrm{FreeGroup}(X)/N\) is surjective. This specialized form is used to lift coefficients from \(\mathbb{Z}_{\ell}\llbracket F/N\rrbracket\) to \(\mathbb{Z}_{\ell}\llbracket F\rrbracket\) in the completed Fox derivative.
primePowerCompletedGroupAlgebraMap_targetQuotient_surjective
The completed group-algebra map attached to \(\mathrm{FreeGroup}(X) \to \mathrm{FreeGroup}(X)/N\) is surjective. This is the coefficient-lifting input for the surjectivity half of \(K/KI \to L\).
primePowerCompletedGroupAlgebraMap_targetQuotient_lift_spec
The chosen coefficient lift maps back to the prescribed completed target coefficient.
Declarations
FoxDifferential.foxAlgebraicStageTargetQuotientContinuousMonoidHom_surjective
DocumentationThe quotient homomorphism \(\mathrm{FreeGroup}(X) \to \mathrm{FreeGroup}(X)/N\) is surjective. This specialized form is used to lift coefficients from \(\mathbb{Z}_{\ell}\llbracket F/N\rrbracket\) to \(\mathbb{Z}_{\ell}\llbracket F\rrbracket\) in the completed Fox derivative.
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.primePowerCompletedGroupAlgebraMap_targetQuotient_surjective
DocumentationThe completed group-algebra map attached to \(\mathrm{FreeGroup}(X) \to \mathrm{FreeGroup}(X)/N\) is surjective. This is the coefficient-lifting input for the surjectivity half of \(K/KI \to L\).
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.primePowerCompletedGroupAlgebraMap_targetQuotient_lift
DocumentationA noncomputable lift of a completed target group-algebra coefficient to the source completed group algebra. The defining equation is \(\mathrm{primePowerCompletedGroupAlgebraMap\_targetQuotient\_lift\_spec}\).
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.primePowerCompletedGroupAlgebraMap_targetQuotient_lift_spec
DocumentationThe chosen coefficient lift maps back to the prescribed completed target coefficient.
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