Module

Semidirect.lean

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

12 declarations indexed from sourceView source ↗

Module documentation

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

The principal declarations in this module are:

foxAlgebraicStagePrimePowerSemidirectTransition

Coefficient reduction between prime-power finite Fox semidirect stages.

foxAlgebraicStagePrimePowerSemidirectSystem

The inverse system of finite Fox semidirect stages over prime-power coefficients.

foxAlgebraicStagePrimePowerSemidirectTransition_left

The left coordinate of the finite-stage semidirect point is the specified derivative component.

foxAlgebraicStagePrimePowerSemidirectTransition_right

The right coordinate of the finite-stage semidirect point is the corresponding quotient component.

Imports1

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

Imported by2

instance

foxAlgebraicStagePrimePowerFactPos

L41 ↗

FoxDifferential.foxAlgebraicStagePrimePowerFactPos

Documentation

Every prime-power modulus \(\ell^a\) used in the finite Fox stage is positive.

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 (ℓ : ℕ) [hℓ : 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 · statement

instance foxAlgebraicStagePrimePowerFactPos (a : ℕ) : Fact (0 < ℓ ^ a)

def

foxAlgebraicStagePrimePowerSemidirectTransition

L45 ↗

FoxDifferential.foxAlgebraicStagePrimePowerSemidirectTransition

Documentation

Coefficient reduction between prime-power finite Fox semidirect 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 (ℓ : ℕ) [hℓ : 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 · statement

def foxAlgebraicStagePrimePowerSemidirectTransition
    (N : Subgroup (FreeGroup X)) [N.Normal] {a b : ℕ} (hab : a ≤ b) :
    FoxAlgebraicStageSemidirect (X := X) N (ℓ ^ b) →*
      FoxAlgebraicStageSemidirect (X := X) N (ℓ ^ a)

theorem

foxAlgebraicStagePrimePowerSemidirectTransition_left

L59 ↗

FoxDifferential.foxAlgebraicStagePrimePowerSemidirectTransition_left

Documentation

The left coordinate of the finite-stage semidirect point is the specified derivative component.

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 (ℓ : ℕ) [hℓ : 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] hℓ in

Lean source · full declaration

theorem foxAlgebraicStagePrimePowerSemidirectTransition_left
    (N : Subgroup (FreeGroup X)) [N.Normal] {a b : ℕ} (hab : a ≤ b)
    (y : FoxAlgebraicStageSemidirect (X := X) N (ℓ ^ b)) :
    (foxAlgebraicStagePrimePowerSemidirectTransition (ℓ := ℓ) (X := X) N hab y).left =
      fun i : X =>
        foxAlgebraicStagePrimePowerTargetTransition (ℓ := ℓ) (X := X) N hab (y.left i) := by
  rfl

theorem

foxAlgebraicStagePrimePowerSemidirectTransition_right

L73 ↗

FoxDifferential.foxAlgebraicStagePrimePowerSemidirectTransition_right

Documentation

The right coordinate of the finite-stage semidirect point is the corresponding quotient component.

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 (ℓ : ℕ) [hℓ : 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] hℓ in

Lean source · statement

theorem foxAlgebraicStagePrimePowerSemidirectTransition_right
    (N : Subgroup (FreeGroup X)) [N.Normal] {a b : ℕ} (hab : a ≤ b)
    (y : FoxAlgebraicStageSemidirect (X := X) N (ℓ ^ b)) :
    (foxAlgebraicStagePrimePowerSemidirectTransition (ℓ := ℓ) (X := X) N hab y).right =
      y.right

theorem

foxAlgebraicStagePrimePowerSemidirectTransition_id

L83 ↗

FoxDifferential.foxAlgebraicStagePrimePowerSemidirectTransition_id

Documentation

The prime-power semidirect transition 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 (ℓ : ℕ) [hℓ : 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] hℓ in

Lean source · statement

theorem foxAlgebraicStagePrimePowerSemidirectTransition_id
    (N : Subgroup (FreeGroup X)) [N.Normal] (a : ℕ) :
    foxAlgebraicStagePrimePowerSemidirectTransition
        (ℓ := ℓ) (X := X) N (le_rfl : a ≤ a) =
      MonoidHom.id (FoxAlgebraicStageSemidirect (X := X) N (ℓ ^ a))

theorem

foxAlgebraicStagePrimePowerSemidirectTransition_comp

L96 ↗

FoxDifferential.foxAlgebraicStagePrimePowerSemidirectTransition_comp

Documentation

Prime-power semidirect transitions compose along the stage order.

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 (ℓ : ℕ) [hℓ : 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] hℓ in

Lean source · statement

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

def

foxAlgebraicStagePrimePowerSemidirectSystem

L112 ↗

FoxDifferential.foxAlgebraicStagePrimePowerSemidirectSystem

Documentation

The inverse system of finite Fox semidirect stages over prime-power coefficients.

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 (ℓ : ℕ) [hℓ : 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 foxAlgebraicStagePrimePowerSemidirectSystem
    (N : Subgroup (FreeGroup X)) [N.Normal] :
    InverseSystem (I := ℕ) where
  X := fun a => FoxAlgebraicStageSemidirect (X := X) N (ℓ ^ a)
  topologicalSpace := fun _ => ⊥
  map := fun {a b} hab =>
    foxAlgebraicStagePrimePowerSemidirectTransition (ℓ := ℓ) (X := X) N hab
  continuous_map := by
    intro a b hab
    let : TopologicalSpace (FoxAlgebraicStageSemidirect (X := X) N (ℓ ^ a)) := ⊥
    let : TopologicalSpace (FoxAlgebraicStageSemidirect (X := X) N (ℓ ^ b)) := ⊥
    let : DiscreteTopology (FoxAlgebraicStageSemidirect (X := X) N (ℓ ^ b)) := ⟨rfl⟩
    exact continuous_of_discreteTopology
  map_id := by
    intro a
    funext y
    exact congrArg (fun f : FoxAlgebraicStageSemidirect (X := X) N (ℓ ^ a) →*
        FoxAlgebraicStageSemidirect (X := X) N (ℓ ^ a) => f y)
      (foxAlgebraicStagePrimePowerSemidirectTransition_id (ℓ := ℓ) (X := X) N a)
  map_comp := by
    intro a b c hab hbc
    funext y
    exact congrArg (fun f : FoxAlgebraicStageSemidirect (X := X) N (ℓ ^ c) →*
        FoxAlgebraicStageSemidirect (X := X) N (ℓ ^ a) => f y)
      (foxAlgebraicStagePrimePowerSemidirectTransition_comp
        (ℓ := ℓ) (X := X) N hab hbc)

instance

instGroupFoxAlgebraicStagePrimePowerSemidirectSystemX

L140 ↗

FoxDifferential.instGroupFoxAlgebraicStagePrimePowerSemidirectSystemX

Documentation

The finite-stage semidirect system carries its group structure.

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 (ℓ : ℕ) [hℓ : 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 · statement

instance instGroupFoxAlgebraicStagePrimePowerSemidirectSystemX
    (N : Subgroup (FreeGroup X)) [N.Normal] (a : ℕ) :
    Group ((foxAlgebraicStagePrimePowerSemidirectSystem (ℓ := ℓ) (X := X) N).X a)

instance

instIsGroupSystemFoxAlgebraicStagePrimePowerSemidirectSystem

L148 ↗

FoxDifferential.instIsGroupSystemFoxAlgebraicStagePrimePowerSemidirectSystem

Documentation

The finite-stage semidirect system is a compatible group system.

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 (ℓ : ℕ) [hℓ : 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

instance instIsGroupSystemFoxAlgebraicStagePrimePowerSemidirectSystem
    (N : Subgroup (FreeGroup X)) [N.Normal] :
    IsGroupSystem (foxAlgebraicStagePrimePowerSemidirectSystem (ℓ := ℓ) (X := X) N) where
  map_one := by
    intro a b hab
    exact map_one (foxAlgebraicStagePrimePowerSemidirectTransition (ℓ := ℓ) (X := X) N hab)
  map_mul := by
    intro a b hab x y
    exact map_mul (foxAlgebraicStagePrimePowerSemidirectTransition (ℓ := ℓ) (X := X) N hab) x y
  map_inv := by
    intro a b hab x
    exact map_inv (foxAlgebraicStagePrimePowerSemidirectTransition (ℓ := ℓ) (X := X) N hab) x

theorem

foxAlgebraicStagePrimePowerSemidirectTransition_lift

L163 ↗

FoxDifferential.foxAlgebraicStagePrimePowerSemidirectTransition_lift

Documentation

Prime-power semidirect transitions carry finite lifts to finite lifts.

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 (ℓ : ℕ) [hℓ : 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 hℓ in

Lean source · statement

theorem foxAlgebraicStagePrimePowerSemidirectTransition_lift
    (N : Subgroup (FreeGroup X)) [N.Normal]
    {a b : ℕ} (hab : a ≤ b) (w : FreeGroup X) :
    foxAlgebraicStagePrimePowerSemidirectTransition (ℓ := ℓ) (X := X) N hab
        (foxAlgebraicStageLift (X := X) N (ℓ ^ b) w) =
      foxAlgebraicStageLift (X := X) N (ℓ ^ a) w

theorem

foxAlgebraicStagePrimePowerSemidirectTransition_kernelWordPoint

L178 ↗

FoxDifferential.foxAlgebraicStagePrimePowerSemidirectTransition_kernelWordPoint

Documentation

Prime-power semidirect transitions carry kernel-word points to kernel-word points.

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 (ℓ : ℕ) [hℓ : 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 hℓ in

Lean source · statement

theorem foxAlgebraicStagePrimePowerSemidirectTransition_kernelWordPoint
    (N : Subgroup (FreeGroup X)) [N.Normal]
    {a b : ℕ} (hab : a ≤ b) (w : FreeGroup X) :
    foxAlgebraicStagePrimePowerSemidirectTransition (ℓ := ℓ) (X := X) N hab
        (foxAlgebraicStageSemidirectKernelWordPoint (X := X) N (ℓ ^ b) w) =
      foxAlgebraicStageSemidirectKernelWordPoint (X := X) N (ℓ ^ a) w

theorem

foxAlgebraicStagePrimePowerSemidirectTransition_mem_boundaryCycleSet

L193 ↗

FoxDifferential.foxAlgebraicStagePrimePowerSemidirectTransition_mem_boundaryCycleSet

Documentation

Prime-power semidirect transitions preserve finite boundary-cycle points.

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 (ℓ : ℕ) [hℓ : 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] hℓ in

Lean source · statement

theorem foxAlgebraicStagePrimePowerSemidirectTransition_mem_boundaryCycleSet
    [Fintype X]
    (N : Subgroup (FreeGroup X)) [N.Normal]
    {a b : ℕ} (hab : a ≤ b)
    {y : FoxAlgebraicStageSemidirect (X := X) N (ℓ ^ b)}
    (hy : y ∈ foxAlgebraicStageSemidirectBoundaryCycleSet (X := X) N (ℓ ^ b)) :
    foxAlgebraicStagePrimePowerSemidirectTransition (ℓ := ℓ) (X := X) N hab y ∈
      foxAlgebraicStageSemidirectBoundaryCycleSet (X := X) N (ℓ ^ a)

Module documentation

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

Declarations