NYLL
Module

BoundaryCycles.lean

Nyll.ProCGroups.FoxDifferential.Completed.FiniteStage.CoeffMap.BoundaryCycles
7 declarations indexed from sourceView source ↗

Module documentation

Fox differential: completed — finite stage — coeff map — boundary cycles

The principal declarations in this module are:

  • foxAlgebraicStageSemidirectCoeffMap_left

The left component of finite-stage semidirect coefficient reduction is obtained by reducing each coordinate coefficient.

  • foxAlgebraicStageSemidirectCoeffMap_right

The right component of finite-stage semidirect coefficient reduction is unchanged.

  • foxAlgebraicStageSemidirectCoeffMap_rfl

Coefficient reduction is the identity on finite-stage semidirect targets when the modulus is unchanged.

  • foxAlgebraicStageSemidirectCoeffMap_comp

Coefficient reductions compose on finite-stage semidirect targets.

Imports3
Imported by3

Declarations

theorem

foxAlgebraicStageSemidirectCoeffMap_left

L52 ↗
FoxDifferential.foxAlgebraicStageSemidirectCoeffMap_left
Documentation

The left component of finite-stage semidirect coefficient reduction is obtained by reducing each coordinate coefficient.

Source context 12 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 : ℕ)
variable {n₀ m₀ : ℕ} [Fact (0 < n₀)] [Fact (0 < m₀)]
omit [DecidableEq X] [Fact (0 < n₀)] [Fact (0 < m₀)] in
Lean source · full declaration
theorem foxAlgebraicStageSemidirectCoeffMap_left
    (N : Subgroup (FreeGroup X)) [N.Normal] (hnm : n₀ ∣ m₀)
    (y : FoxAlgebraicStageSemidirect (X := X) N m₀) :
    (foxAlgebraicStageSemidirectCoeffMap (X := X) N hnm y).left =
      fun i : X => foxAlgebraicStageTargetGroupAlgebraCoeffMap (X := X) N hnm (y.left i) :=
  rfl
theorem

foxAlgebraicStageSemidirectCoeffMap_right

L62 ↗
FoxDifferential.foxAlgebraicStageSemidirectCoeffMap_right
Documentation

The right component of finite-stage semidirect coefficient reduction is unchanged.

Source context 12 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 : ℕ)
variable {n₀ m₀ : ℕ} [Fact (0 < n₀)] [Fact (0 < m₀)]
omit [DecidableEq X] [Fact (0 < n₀)] [Fact (0 < m₀)] in
Lean source · statement
theorem foxAlgebraicStageSemidirectCoeffMap_right
    (N : Subgroup (FreeGroup X)) [N.Normal] (hnm : n₀ ∣ m₀)
    (y : FoxAlgebraicStageSemidirect (X := X) N m₀) :
    (foxAlgebraicStageSemidirectCoeffMap (X := X) N hnm y).right = y.right
theorem

foxAlgebraicStageSemidirectCoeffMap_rfl

L74 ↗
FoxDifferential.foxAlgebraicStageSemidirectCoeffMap_rfl
Documentation

Coefficient reduction is the identity on finite-stage semidirect targets when the modulus is unchanged.

Source context 12 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 : ℕ)
variable {n₀ m₀ : ℕ} [Fact (0 < n₀)] [Fact (0 < m₀)]
omit [Fact (0 < m₀)] [DecidableEq X] [Fact (0 < n₀)] in
Lean source · statement
theorem foxAlgebraicStageSemidirectCoeffMap_rfl
    (N : Subgroup (FreeGroup X)) [N.Normal] :
    foxAlgebraicStageSemidirectCoeffMap
        (X := X) (n₀ := n₀) (m₀ := n₀) N dvd_rfl =
      MonoidHom.id (FoxAlgebraicStageSemidirect (X := X) N n₀)
theorem

foxAlgebraicStageSemidirectCoeffMap_comp

L92 ↗
FoxDifferential.foxAlgebraicStageSemidirectCoeffMap_comp
Documentation

Coefficient reductions compose on finite-stage semidirect targets.

Source context 12 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 : ℕ)
variable {n₀ m₀ : ℕ} [Fact (0 < n₀)] [Fact (0 < m₀)]
omit [DecidableEq X] [Fact (0 < n₀)] [Fact (0 < m₀)] in
Lean source · statement
theorem foxAlgebraicStageSemidirectCoeffMap_comp
    {k₀ : ℕ}
    (N : Subgroup (FreeGroup X)) [N.Normal]
    (hnm : n₀ ∣ m₀) (hmk : m₀ ∣ k₀) :
    (foxAlgebraicStageSemidirectCoeffMap (X := X) N hnm).comp
        (foxAlgebraicStageSemidirectCoeffMap (X := X) N hmk) =
      foxAlgebraicStageSemidirectCoeffMap (X := X) N (dvd_trans hnm hmk)
theorem

foxAlgebraicStageSemidirectCoeffMap_mem_boundaryCycleSet

L117 ↗
FoxDifferential.foxAlgebraicStageSemidirectCoeffMap_mem_boundaryCycleSet
Documentation

Coefficient reduction carries finite semidirect boundary cycles to finite semidirect boundary cycles.

Source context 12 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 : ℕ)
variable {n₀ m₀ : ℕ} [Fact (0 < n₀)] [Fact (0 < m₀)]
omit [DecidableEq X] [Fact (0 < n₀)] [Fact (0 < m₀)] in
Lean source · statement
theorem foxAlgebraicStageSemidirectCoeffMap_mem_boundaryCycleSet
    [Fintype X]
    (N : Subgroup (FreeGroup X)) [N.Normal] (hnm : n₀ ∣ m₀)
    {y : FoxAlgebraicStageSemidirect (X := X) N m₀}
    (hy : y ∈ foxAlgebraicStageSemidirectBoundaryCycleSet (X := X) N m₀) :
    foxAlgebraicStageSemidirectCoeffMap (X := X) N hnm y ∈
      foxAlgebraicStageSemidirectBoundaryCycleSet (X := X) N n₀
theorem

foxAlgebraicStageSemidirectCoeffMap_kernelWordPoint

L136 ↗
FoxDifferential.foxAlgebraicStageSemidirectCoeffMap_kernelWordPoint
Documentation

Coefficient reduction sends the finite semidirect kernel-word point at modulus \(m\) to the corresponding point at modulus \(n\).

Source context 12 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 : ℕ)
variable {n₀ m₀ : ℕ} [Fact (0 < n₀)] [Fact (0 < m₀)]
omit [Fact (0 < n₀)] [Fact (0 < m₀)] in
Lean source · statement
theorem foxAlgebraicStageSemidirectCoeffMap_kernelWordPoint
    (N : Subgroup (FreeGroup X)) [N.Normal] (hnm : n₀ ∣ m₀)
    (w : FreeGroup X) :
    foxAlgebraicStageSemidirectCoeffMap (X := X) N hnm
        (foxAlgebraicStageSemidirectKernelWordPoint (X := X) N m₀ w) =
      foxAlgebraicStageSemidirectKernelWordPoint (X := X) N n₀ w
theorem

foxAlgebraicStageSemidirectCoeffMap_kernelWordDerivativeSet_subset

L155 ↗
FoxDifferential.foxAlgebraicStageSemidirectCoeffMap_kernelWordDerivativeSet_subset
Documentation

Coefficient reduction sends the finite semidirect kernel-word derivative set at modulus \(m\) into the corresponding set at modulus \(n\).

Source context 12 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 : ℕ)
variable {n₀ m₀ : ℕ} [Fact (0 < n₀)] [Fact (0 < m₀)]
omit [Fact (0 < n₀)] [Fact (0 < m₀)] in
Lean source · full declaration
theorem foxAlgebraicStageSemidirectCoeffMap_kernelWordDerivativeSet_subset
    (N : Subgroup (FreeGroup X)) [N.Normal] (hnm : n₀ ∣ m₀) :
    (fun y : FoxAlgebraicStageSemidirect (X := X) N m₀ =>
        foxAlgebraicStageSemidirectCoeffMap (X := X) N hnm y) ''
      foxAlgebraicStageSemidirectKernelWordDerivativeSet (X := X) N m₀ ⊆
        foxAlgebraicStageSemidirectKernelWordDerivativeSet (X := X) N n₀ := by
  intro y hy
  rcases hy with ⟨z, hz, rfl⟩
  rcases hz with ⟨w, hwN, hzw⟩
  refine ⟨w, hwN, ?_⟩
  rw [← hzw]
  exact (foxAlgebraicStageSemidirectCoeffMap_kernelWordPoint (X := X) N hnm w).symm

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.