ModuleLift.lean
Nyll.ProCGroups.FoxDifferential.Completed.FiniteStage.Stage.Derivative.Lift
6 declarations indexed from sourceView source ↗ Module documentation
Fox differential: finite stage — stage — derivative — lift
The principal declarations in this module are:
Semidirect-product lift defining the finite-stage Fox derivative.
foxAlgebraicStageDerivativeVector
Finite-stage Fox derivative vector of a free-group word.
foxAlgebraicStageLift_right
The right component of the finite-stage lift is the quotient class in \(F/N\).
foxAlgebraicStageCoefficient_apply
The finite Fox-stage coefficient map is evaluated by applying the selected coefficient projection.
Declarations
FoxDifferential.foxAlgebraicStageLift
DocumentationSemidirect-product lift defining the finite-stage Fox derivative.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
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]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)
FoxDifferential.foxAlgebraicStageLift_right
DocumentationThe right component of the finite-stage lift is the quotient class in \(F/N\).
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
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]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)
FoxDifferential.foxAlgebraicStageDerivativeVector
DocumentationFinite-stage Fox derivative vector of a free-group word.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
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]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)
FoxDifferential.foxAlgebraicStageDerivative
DocumentationA coordinate of the finite-stage Fox derivative vector.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
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]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)
FoxDifferential.foxAlgebraicStageCoefficient
DocumentationThe coefficient map for the finite-stage Fox crossed differential.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
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]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)
FoxDifferential.foxAlgebraicStageCoefficient_apply
DocumentationThe finite Fox-stage coefficient map is evaluated by applying the selected coefficient projection.
Source context 11 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
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]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)
omit [DecidableEq X] in