Module

Basic.lean

Nyll.ProCGroups.FoxDifferential.Completed.FiniteStage.PrimePower.System.Basic

18 declarations indexed from sourceView source ↗

Module documentation

Fox differential: finite stage — prime power — system — basic

The principal declarations in this module are:

foxAlgebraicStagePrimePowerSourceGroupAlgebra

Source group algebra at the \(\ell^a\) finite Fox stage.

foxAlgebraicStagePrimePowerTargetGroupAlgebra

Target group algebra at the \(\ell^a\) finite Fox stage.

foxAlgebraicStagePrimePowerFreeGroupAlgebraTransition_of

Coefficient reduction sends a group-like free-group element to the same group-like element at the lower prime-power stage.

foxAlgebraicStagePrimePowerSourceProjection_of

Evaluation of the source projection on a group-like free-group algebra element.

Imports1

Nyll.ProCGroups.FoxDifferential.Completed.FiniteStage.CoeffMap.BoundaryCycles

Imported by3

abbrev

foxAlgebraicStagePrimePowerSourceGroupAlgebra

L45 ↗

FoxDifferential.foxAlgebraicStagePrimePowerSourceGroupAlgebra

Documentation

Source group algebra at the \(\ell^a\) finite Fox stage.

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 [Fact (0 < ℓ)] in

Lean source · statement

abbrev foxAlgebraicStagePrimePowerSourceGroupAlgebra
    (N : Subgroup (FreeGroup X)) (a : ℕ) : Type u

abbrev

foxAlgebraicStagePrimePowerTargetGroupAlgebra

L52 ↗

FoxDifferential.foxAlgebraicStagePrimePowerTargetGroupAlgebra

Documentation

Target group algebra at the \(\ell^a\) finite Fox stage.

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 [Fact (0 < ℓ)] in

Lean source · statement

abbrev foxAlgebraicStagePrimePowerTargetGroupAlgebra
    (N : Subgroup (FreeGroup X)) (a : ℕ) : Type u

abbrev

foxAlgebraicStagePrimePowerFreeGroupAlgebra

L58 ↗

FoxDifferential.foxAlgebraicStagePrimePowerFreeGroupAlgebra

Documentation

The free-group algebra with coefficients modulo \(\ell^a\).

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 [Fact (0 < ℓ)] in

Lean source · statement

abbrev foxAlgebraicStagePrimePowerFreeGroupAlgebra (a : ℕ) : Type u

def

foxAlgebraicStagePrimePowerFreeGroupAlgebraTransition

L63 ↗

FoxDifferential.foxAlgebraicStagePrimePowerFreeGroupAlgebraTransition

Documentation

Coefficient reduction on free-group algebras between prime-power stages.

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 [Fact (0 < ℓ)] in

Lean source · statement

def foxAlgebraicStagePrimePowerFreeGroupAlgebraTransition
    {a b : ℕ} (hab : a ≤ b) :
    foxAlgebraicStagePrimePowerFreeGroupAlgebra (ℓ := ℓ) (X := X) b →+*
      foxAlgebraicStagePrimePowerFreeGroupAlgebra (ℓ := ℓ) (X := X) a

theorem

foxAlgebraicStagePrimePowerFreeGroupAlgebraTransition_of

L76 ↗

FoxDifferential.foxAlgebraicStagePrimePowerFreeGroupAlgebraTransition_of

Documentation

Coefficient reduction sends a group-like free-group element to the same group-like element at the lower prime-power stage.

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] [Fact (0 < ℓ)] in

Lean source · statement

theorem foxAlgebraicStagePrimePowerFreeGroupAlgebraTransition_of
    {a b : ℕ} (hab : a ≤ b) (w : FreeGroup X) :
    foxAlgebraicStagePrimePowerFreeGroupAlgebraTransition (ℓ := ℓ) (X := X) hab
        (MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ b)) (FreeGroup X) w) =
      MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ a)) (FreeGroup X) w

def

foxAlgebraicStagePrimePowerSourceProjection

L89 ↗

FoxDifferential.foxAlgebraicStagePrimePowerSourceProjection

Documentation

The projection from the free-group algebra to the finite Fox source quotient at a prime-power stage.

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 [Fact (0 < ℓ)] in

Lean source · statement

def foxAlgebraicStagePrimePowerSourceProjection
    (N : Subgroup (FreeGroup X)) (a : ℕ) :
    foxAlgebraicStagePrimePowerFreeGroupAlgebra (ℓ := ℓ) (X := X) a →+*
      foxAlgebraicStagePrimePowerSourceGroupAlgebra (ℓ := ℓ) (X := X) N a

theorem

foxAlgebraicStagePrimePowerSourceProjection_of

L100 ↗

FoxDifferential.foxAlgebraicStagePrimePowerSourceProjection_of

Documentation

Evaluation of the source projection on a group-like free-group algebra element.

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] [Fact (0 < ℓ)] in

Lean source · statement

theorem foxAlgebraicStagePrimePowerSourceProjection_of
    (N : Subgroup (FreeGroup X)) (a : ℕ) (w : FreeGroup X) :
    foxAlgebraicStagePrimePowerSourceProjection (ℓ := ℓ) (X := X) N a
        (MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ a)) (FreeGroup X) w) =
      MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ a))
        (FreeGroup X ⧸
          foxCommutatorPowerSubgroup (F := FreeGroup X) N (ℓ ^ a))
        (QuotientGroup.mk'
          (foxCommutatorPowerSubgroup (F := FreeGroup X) N (ℓ ^ a)) w)

def

foxAlgebraicStagePrimePowerSourceTransition

L121 ↗

FoxDifferential.foxAlgebraicStagePrimePowerSourceTransition

Documentation

Transition map for the finite Fox source quotient group algebras along prime-power stages.

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 [Fact (0 < ℓ)] in

Lean source · statement

def foxAlgebraicStagePrimePowerSourceTransition
    (N : Subgroup (FreeGroup X)) {a b : ℕ} (hab : a ≤ b) :
    foxAlgebraicStagePrimePowerSourceGroupAlgebra (ℓ := ℓ) (X := X) N b →+*
      foxAlgebraicStagePrimePowerSourceGroupAlgebra (ℓ := ℓ) (X := X) N a

theorem

foxAlgebraicStagePrimePowerSourceTransition_of

L131 ↗

FoxDifferential.foxAlgebraicStagePrimePowerSourceTransition_of

Documentation

Evaluation of a source transition map on a group-like quotient element.

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] [Fact (0 < ℓ)] in

Lean source · statement

theorem foxAlgebraicStagePrimePowerSourceTransition_of
    (N : Subgroup (FreeGroup X)) {a b : ℕ} (hab : a ≤ b) (w : FreeGroup X) :
    foxAlgebraicStagePrimePowerSourceTransition (ℓ := ℓ) (X := X) N hab
        (MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ b))
          (FreeGroup X ⧸
            foxCommutatorPowerSubgroup (F := FreeGroup X) N (ℓ ^ b))
          (QuotientGroup.mk'
            (foxCommutatorPowerSubgroup (F := FreeGroup X) N (ℓ ^ b)) w)) =
      MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ a))
        (FreeGroup X ⧸
          foxCommutatorPowerSubgroup (F := FreeGroup X) N (ℓ ^ a))
        (QuotientGroup.mk'
          (foxCommutatorPowerSubgroup (F := FreeGroup X) N (ℓ ^ a)) w)

theorem

foxAlgebraicStagePrimePowerSourceTransition_id

L150 ↗

FoxDifferential.foxAlgebraicStagePrimePowerSourceTransition_id

Documentation

The source transition map from a stage to itself is the identity.

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] [Fact (0 < ℓ)] in

Lean source · statement

theorem foxAlgebraicStagePrimePowerSourceTransition_id
    (N : Subgroup (FreeGroup X)) (a : ℕ) :
    foxAlgebraicStagePrimePowerSourceTransition (ℓ := ℓ) (X := X) N
        (le_rfl : a ≤ a) =
      RingHom.id _

theorem

foxAlgebraicStagePrimePowerSourceTransition_comp

L161 ↗

FoxDifferential.foxAlgebraicStagePrimePowerSourceTransition_comp

Documentation

Source transition maps compose along the order on prime-power stages.

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] [Fact (0 < ℓ)] in

Lean source · statement

theorem foxAlgebraicStagePrimePowerSourceTransition_comp
    (N : Subgroup (FreeGroup X)) {a b c : ℕ} (hab : a ≤ b) (hbc : b ≤ c) :
    (foxAlgebraicStagePrimePowerSourceTransition (ℓ := ℓ) (X := X) N hab).comp
        (foxAlgebraicStagePrimePowerSourceTransition (ℓ := ℓ) (X := X) N hbc) =
      foxAlgebraicStagePrimePowerSourceTransition (ℓ := ℓ) (X := X) N (hab.trans hbc)

theorem

foxAlgebraicStagePrimePowerSourceProjection_transition

L171 ↗

FoxDifferential.foxAlgebraicStagePrimePowerSourceProjection_transition

Documentation

Source projection commutes with coefficient reduction and the source transition map.

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] [Fact (0 < ℓ)] in

Lean source · statement

theorem foxAlgebraicStagePrimePowerSourceProjection_transition
    (N : Subgroup (FreeGroup X)) {a b : ℕ} (hab : a ≤ b) :
    (foxAlgebraicStagePrimePowerSourceTransition (ℓ := ℓ) (X := X) N hab).comp
        (foxAlgebraicStagePrimePowerSourceProjection (ℓ := ℓ) (X := X) N b) =
      (foxAlgebraicStagePrimePowerSourceProjection (ℓ := ℓ) (X := X) N a).comp
        (foxAlgebraicStagePrimePowerFreeGroupAlgebraTransition (ℓ := ℓ) (X := X) hab)

def

foxAlgebraicStagePrimePowerTargetTransition

L208 ↗

FoxDifferential.foxAlgebraicStagePrimePowerTargetTransition

Documentation

Transition map for the finite Fox target group algebras along prime-power stages.

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 [Fact (0 < ℓ)] in

Lean source · statement

def foxAlgebraicStagePrimePowerTargetTransition
    (N : Subgroup (FreeGroup X)) [N.Normal] {a b : ℕ} (hab : a ≤ b) :
    foxAlgebraicStagePrimePowerTargetGroupAlgebra (ℓ := ℓ) (X := X) N b →+*
      foxAlgebraicStagePrimePowerTargetGroupAlgebra (ℓ := ℓ) (X := X) N a

theorem

foxAlgebraicStagePrimePowerTargetTransition_of

L218 ↗

FoxDifferential.foxAlgebraicStagePrimePowerTargetTransition_of

Documentation

Evaluation of a target transition map on a group-like target quotient element.

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] [Fact (0 < ℓ)] in

Lean source · statement

theorem foxAlgebraicStagePrimePowerTargetTransition_of
    (N : Subgroup (FreeGroup X)) [N.Normal] {a b : ℕ} (hab : a ≤ b) (w : FreeGroup X) :
    foxAlgebraicStagePrimePowerTargetTransition (ℓ := ℓ) (X := X) N hab
        (MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ b))
          (foxAlgebraicStageTargetQuotient (X := X) N)
          (QuotientGroup.mk' N w)) =
      MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ a))
        (foxAlgebraicStageTargetQuotient (X := X) N)
        (QuotientGroup.mk' N w)

theorem

foxAlgebraicStagePrimePowerTargetTransition_id

L233 ↗

FoxDifferential.foxAlgebraicStagePrimePowerTargetTransition_id

Documentation

The target transition map from a stage to itself is the identity.

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] [Fact (0 < ℓ)] in

Lean source · statement

theorem foxAlgebraicStagePrimePowerTargetTransition_id
    (N : Subgroup (FreeGroup X)) [N.Normal] (a : ℕ) :
    foxAlgebraicStagePrimePowerTargetTransition (ℓ := ℓ) (X := X) N
        (le_rfl : a ≤ a) =
      RingHom.id _

theorem

foxAlgebraicStagePrimePowerTargetTransition_comp

L244 ↗

FoxDifferential.foxAlgebraicStagePrimePowerTargetTransition_comp

Documentation

Target transition maps compose along the order on prime-power stages.

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] [Fact (0 < ℓ)] in

Lean source · statement

theorem foxAlgebraicStagePrimePowerTargetTransition_comp
    (N : Subgroup (FreeGroup X)) [N.Normal] {a b c : ℕ} (hab : a ≤ b) (hbc : b ≤ c) :
    (foxAlgebraicStagePrimePowerTargetTransition (ℓ := ℓ) (X := X) N hab).comp
        (foxAlgebraicStagePrimePowerTargetTransition (ℓ := ℓ) (X := X) N hbc) =
      foxAlgebraicStagePrimePowerTargetTransition (ℓ := ℓ) (X := X) N (hab.trans hbc)

def

foxAlgebraicStagePrimePowerSourceSystem

L253 ↗

FoxDifferential.foxAlgebraicStagePrimePowerSourceSystem

Documentation

The inverse system of finite Fox source quotient group algebras over prime-power stages.

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 : ℕ)

Lean source · full declaration

def foxAlgebraicStagePrimePowerSourceSystem
    (N : Subgroup (FreeGroup X)) :
    InverseSystem (I := ℕ) where
  X := foxAlgebraicStagePrimePowerSourceGroupAlgebra (ℓ := ℓ) (X := X) N
  topologicalSpace := fun _ => ⊥
  map := fun {a b} hab => foxAlgebraicStagePrimePowerSourceTransition (ℓ := ℓ) (X := X) N hab
  continuous_map := by
    intro a b hab
    let : TopologicalSpace
        (foxAlgebraicStagePrimePowerSourceGroupAlgebra (ℓ := ℓ) (X := X) N a) := ⊥
    let : TopologicalSpace
        (foxAlgebraicStagePrimePowerSourceGroupAlgebra (ℓ := ℓ) (X := X) N b) := ⊥
    let : DiscreteTopology
        (foxAlgebraicStagePrimePowerSourceGroupAlgebra (ℓ := ℓ) (X := X) N b) := ⟨rfl⟩
    exact continuous_of_discreteTopology
  map_id := by
    intro a
    funext x
    exact congrFun
      (congrArg DFunLike.coe
        (foxAlgebraicStagePrimePowerSourceTransition_id (ℓ := ℓ) (X := X) N a)) x
  map_comp := by
    intro a b c hab hbc
    funext x
    exact congrFun
      (congrArg DFunLike.coe
        (foxAlgebraicStagePrimePowerSourceTransition_comp
          (ℓ := ℓ) (X := X) N hab hbc)) x

def

foxAlgebraicStagePrimePowerTargetSystem

L283 ↗

FoxDifferential.foxAlgebraicStagePrimePowerTargetSystem

Documentation

The inverse system of finite Fox target group algebras over prime-power stages.

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 : ℕ)

Lean source · full declaration

def foxAlgebraicStagePrimePowerTargetSystem
    (N : Subgroup (FreeGroup X)) [N.Normal] :
    InverseSystem (I := ℕ) where
  X := foxAlgebraicStagePrimePowerTargetGroupAlgebra (ℓ := ℓ) (X := X) N
  topologicalSpace := fun _ => ⊥
  map := fun {a b} hab => foxAlgebraicStagePrimePowerTargetTransition (ℓ := ℓ) (X := X) N hab
  continuous_map := by
    intro a b hab
    let : TopologicalSpace
        (foxAlgebraicStagePrimePowerTargetGroupAlgebra (ℓ := ℓ) (X := X) N a) := ⊥
    let : TopologicalSpace
        (foxAlgebraicStagePrimePowerTargetGroupAlgebra (ℓ := ℓ) (X := X) N b) := ⊥
    let : DiscreteTopology
        (foxAlgebraicStagePrimePowerTargetGroupAlgebra (ℓ := ℓ) (X := X) N b) := ⟨rfl⟩
    exact continuous_of_discreteTopology
  map_id := by
    intro a
    funext x
    exact congrFun
      (congrArg DFunLike.coe
        (foxAlgebraicStagePrimePowerTargetTransition_id (ℓ := ℓ) (X := X) N a)) x
  map_comp := by
    intro a b c hab hbc
    funext x
    exact congrFun
      (congrArg DFunLike.coe
      (foxAlgebraicStagePrimePowerTargetTransition_comp
          (ℓ := ℓ) (X := X) N hab hbc)) x

Module documentation

Fox differential: finite stage — prime power — system — basic

Declarations