NYLL
Module

MagnusQuotient.lean

Nyll.ProCGroups.FoxDifferential.Completed.FiniteStage.MagnusQuotient
15 declarations indexed from sourceView source ↗

Module documentation

Fox differential: completed — finite stage — magnus quotient

The principal declarations in this module are:

  • foxAlgebraicStageSemidirectReindexHom

Reindex the finite-stage Fox semidirect target along an equivalence of free bases.

  • foxAlgebraicStageSemidirectReindexHom_lift

The reindexing hom carries the finite-stage lift to the finite-stage lift.

  • foxAlgebraicStageDerivativeVector_reindex

Finite-stage Fox derivative vectors reindex along an equivalence of free bases.

  • foxAlgebraicStageDerivativeVector_eq_zero_reindex

Zero of a finite-stage Fox derivative vector is invariant under reindexing the free basis.

Imports2
Imported by2

Declarations

def

foxAlgebraicStageSemidirectReindexHom

L41 ↗
FoxDifferential.foxAlgebraicStageSemidirectReindexHom
Documentation

Reindex the finite-stage Fox semidirect target along an equivalence of free bases.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped commutatorElement
universe u v
variable {X : Type u}
section Reindex
variable {Y : Type v}
variable [DecidableEq X] [DecidableEq Y]
Lean source · statement
def foxAlgebraicStageSemidirectReindexHom
    (e : X ≃ Y)
    (N : Subgroup (FreeGroup X)) [N.Normal]
    (M : Subgroup (FreeGroup Y)) [M.Normal]
    (hM : N.map (FreeGroup.freeGroupCongr e).toMonoidHom = M)
    (n : ℕ) :
    FoxAlgebraicStageSemidirect (X := X) N n →*
      FoxAlgebraicStageSemidirect (X := Y) M n
theorem

foxAlgebraicStageSemidirectReindexHom_lift

L100 ↗
FoxDifferential.foxAlgebraicStageSemidirectReindexHom_lift
Documentation

The reindexing hom carries the finite-stage lift to the finite-stage lift.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped commutatorElement
universe u v
variable {X : Type u}
section Reindex
variable {Y : Type v}
variable [DecidableEq X] [DecidableEq Y]
Lean source · statement
theorem foxAlgebraicStageSemidirectReindexHom_lift
    (e : X ≃ Y)
    (N : Subgroup (FreeGroup X)) [N.Normal]
    (M : Subgroup (FreeGroup Y)) [M.Normal]
    (hM : N.map (FreeGroup.freeGroupCongr e).toMonoidHom = M)
    (n : ℕ) (w : FreeGroup X) :
    foxAlgebraicStageSemidirectReindexHom (X := X) (Y := Y) e N M hM n
        (foxAlgebraicStageLift (X := X) N n w) =
      foxAlgebraicStageLift (X := Y) M n ((FreeGroup.freeGroupCongr e) w)
theorem

foxAlgebraicStageDerivativeVector_reindex

L154 ↗
FoxDifferential.foxAlgebraicStageDerivativeVector_reindex
Documentation

Finite-stage Fox derivative vectors reindex along an equivalence of free bases.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped commutatorElement
universe u v
variable {X : Type u}
section Reindex
variable {Y : Type v}
variable [DecidableEq X] [DecidableEq Y]
Lean source · full declaration
theorem foxAlgebraicStageDerivativeVector_reindex
    (e : X ≃ Y)
    (N : Subgroup (FreeGroup X)) [N.Normal]
    (M : Subgroup (FreeGroup Y)) [M.Normal]
    (hM : N.map (FreeGroup.freeGroupCongr e).toMonoidHom = M)
    (n : ℕ) (w : FreeGroup X) :
    foxAlgebraicStageDerivativeVector (X := Y) M n ((FreeGroup.freeGroupCongr e) w) =
      fun y =>
        MonoidAlgebra.mapDomainRingHom (ModNCompletedCoeff n)
          (QuotientGroup.congr N M (FreeGroup.freeGroupCongr e) hM).toMonoidHom
          (foxAlgebraicStageDerivativeVector (X := X) N n w (e.symm y)) := by
  have h :=
    congrArg FoxAlgebraicStageSemidirect.left
      (foxAlgebraicStageSemidirectReindexHom_lift
        (X := X) (Y := Y) e N M hM n w)
  simpa [foxAlgebraicStageDerivativeVector, foxAlgebraicStageSemidirectReindexHom] using h.symm
theorem

foxAlgebraicStageDerivativeVector_eq_zero_reindex

L172 ↗
FoxDifferential.foxAlgebraicStageDerivativeVector_eq_zero_reindex
Documentation

Zero of a finite-stage Fox derivative vector is invariant under reindexing the free basis.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped commutatorElement
universe u v
variable {X : Type u}
section Reindex
variable {Y : Type v}
variable [DecidableEq X] [DecidableEq Y]
Lean source · statement
theorem foxAlgebraicStageDerivativeVector_eq_zero_reindex
    (e : X ≃ Y)
    (N : Subgroup (FreeGroup X)) [N.Normal]
    (M : Subgroup (FreeGroup Y)) [M.Normal]
    (hM : N.map (FreeGroup.freeGroupCongr e).toMonoidHom = M)
    (n : ℕ) {w : FreeGroup X}
    (hw : foxAlgebraicStageDerivativeVector (X := X) N n w = 0) :
    foxAlgebraicStageDerivativeVector (X := Y) M n ((FreeGroup.freeGroupCongr e) w) = 0
theorem

commutator_subtype_le_foxCommutatorPowerSubgroup

L198 ↗
FoxDifferential.commutator_subtype_le_foxCommutatorPowerSubgroup
Documentation

The ordinary commutator subgroup of \(N\), mapped back to the ambient group, is contained in the finite Fox commutator-power subgroup.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped commutatorElement
universe u v
variable {X : Type u}
variable {Q H : Type u}
variable [Group Q] [Group H]
section CommutatorPowerSubgroup
variable {F : Type u} [Group F]
Lean source · statement
theorem commutator_subtype_le_foxCommutatorPowerSubgroup
    (N : Subgroup F) (n : ℕ) :
    (commutator N).map N.subtype ≤ foxCommutatorPowerSubgroup (F := F) N n
theorem

pow_mem_foxCommutatorPowerSubgroup

L208 ↗
FoxDifferential.pow_mem_foxCommutatorPowerSubgroup
Documentation

Nth powers from N are defining relators for the finite Fox commutator-power subgroup.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped commutatorElement
universe u v
variable {X : Type u}
variable {Q H : Type u}
variable [Group Q] [Group H]
section CommutatorPowerSubgroup
variable {F : Type u} [Group F]
Lean source · statement
theorem pow_mem_foxCommutatorPowerSubgroup
    (N : Subgroup F) (n : ℕ) {a : F} (ha : a ∈ N) :
    a ^ n ∈ foxCommutatorPowerSubgroup (F := F) N n
theorem

mem_foxCommutatorPowerSubgroup_of_abelianization_eq_pow

L217 ↗
FoxDifferential.mem_foxCommutatorPowerSubgroup_of_abelianization_eq_pow
Documentation

If the abelianization class of a kernel element is an \(n\)-th power, then the element lies in \([N,N]N^n\).

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped commutatorElement
universe u v
variable {X : Type u}
variable {Q H : Type u}
variable [Group Q] [Group H]
section CommutatorPowerSubgroup
variable {F : Type u} [Group F]
Lean source · statement
theorem mem_foxCommutatorPowerSubgroup_of_abelianization_eq_pow
    (N : Subgroup F) (n : ℕ) {w : F} (hw : w ∈ N) (a : N)
    (hclass :
      Abelianization.of ⟨w, hw⟩ = (Abelianization.of a) ^ n) :
    w ∈ foxCommutatorPowerSubgroup (F := F) N n
theorem

ker_foxAlgebraicStageLift_le_foxCommutatorPowerSubgroup_iff_residue

L253 ↗
FoxDifferential.ker_foxAlgebraicStageLift_le_foxCommutatorPowerSubgroup_iff_residue
Documentation

Residue-Fox form of the finite-stage Magnus reverse inclusion. The finite-stage derivative is not a separate Fox theory: it is the residue free Fox derivative for the quotient map \(\mathrm{FreeGroup}(X) \to F/N\). This is the residue form of the finite Magnus reverse inclusion, expressed through the finite-stage derivative.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped commutatorElement
universe u v
variable {X : Type u}
variable {Q H : Type u}
variable [Group Q] [Group H]
Lean source · statement
theorem ker_foxAlgebraicStageLift_le_foxCommutatorPowerSubgroup_iff_residue
    [DecidableEq X]
    (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ) :
    (foxAlgebraicStageLift (X := X) N n).ker ≤
        foxCommutatorPowerSubgroup (F := FreeGroup X) N n ↔
      ∀ w : FreeGroup X,
        w ∈ N →
        residueFreeGroupFoxDerivativeVector n (QuotientGroup.mk' N) w = 0 →
          w ∈ foxCommutatorPowerSubgroup (F := FreeGroup X) N n
theorem

ker_foxAlgebraicStageLift_le_foxCommutatorPowerSubgroup_iff_residueUniversal

L278 ↗
FoxDifferential.ker_foxAlgebraicStageLift_le_foxCommutatorPowerSubgroup_iff_residueUniversal
Documentation

Residue-universal form of the finite-stage Magnus reverse inclusion. With a finite free basis, the finite-stage coordinate vector is equivalent to the residue universal differential, so the remaining theorem is a kernel statement in the residue universal module.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped commutatorElement
universe u v
variable {X : Type u}
variable {Q H : Type u}
variable [Group Q] [Group H]
Lean source · statement
theorem ker_foxAlgebraicStageLift_le_foxCommutatorPowerSubgroup_iff_residueUniversal
    [DecidableEq X] [Finite X]
    (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ) :
    (foxAlgebraicStageLift (X := X) N n).ker ≤
        foxCommutatorPowerSubgroup (F := FreeGroup X) N n ↔
      ∀ w : FreeGroup X,
        w ∈ N →
        residueUniversalDifferential n (QuotientGroup.mk' N) w = 0 →
          w ∈ foxCommutatorPowerSubgroup (F := FreeGroup X) N n
theorem

mem_commutator_ker_of_mem_foxCommutatorPowerSubgroup_of_pow_eq_one

L307 ↗
FoxDifferential.mem_commutator_ker_of_mem_foxCommutatorPowerSubgroup_of_pow_eq_one
Documentation

The finite commutator-power subgroup maps into the ordinary commutator subgroup of a target kernel whenever the chosen exponent kills that kernel. This is the mathematical quotient bookkeeping needed after the finite-stage Magnus kernel theorem: the commutator relators map to commutators in kernel \(\beta\), while the power relators map to \(1\) by the given exponent-killing hypothesis.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped commutatorElement
universe u v
variable {X : Type u}
variable {Q H : Type u}
variable [Group Q] [Group H]
Lean source · full declaration
theorem mem_commutator_ker_of_mem_foxCommutatorPowerSubgroup_of_pow_eq_one
    (α : FreeGroup X →* Q) (β : Q →* H) (n : ℕ)
    (hpow : ∀ k : β.ker, k ^ n = 1)
    {w : FreeGroup X}
    (hwker : w ∈ (β.comp α).ker)
    (hw :
      w ∈ foxCommutatorPowerSubgroup
        (F := FreeGroup X) (β.comp α).ker n) :
    (⟨α w, by
      change β (α w) = 1
      simpa [MonoidHom.mem_ker, MonoidHom.comp_apply] using hwker⟩ : β.ker) ∈
      commutator β.ker := by
  let K : Subgroup Q := β.ker
  let S : Subgroup (FreeGroup X) := (⁅K, K⁆).comap α
  have hSnormal : S.Normal := by
    dsimp [S, K]
    infer_instance
  have hrel_le :
      foxCommutatorPowerSubgroup (F := FreeGroup X) (β.comp α).ker n ≤ S := by
    refine Subgroup.normalClosure_le_normal ?_
    intro g hg
    rcases hg with ⟨a, ha, b, hb, rfl⟩ | ⟨a, ha, rfl⟩
    · change α ⁅a, b⁆ ∈ ⁅K, K⁆
      rw [map_commutatorElement]
      have haK : α a ∈ K := by
        change β (α a) = 1
        simpa [MonoidHom.mem_ker, MonoidHom.comp_apply] using ha
      have hbK : α b ∈ K := by
        change β (α b) = 1
        simpa [MonoidHom.mem_ker, MonoidHom.comp_apply] using hb
      exact Subgroup.commutator_mem_commutator haK hbK
    · change α (a ^ n) ∈ ⁅K, K⁆
      rw [map_pow]
      have haK : α a ∈ β.ker := by
        change β (α a) = 1
        simpa [MonoidHom.mem_ker, MonoidHom.comp_apply] using ha
      have hpowQ : (α a) ^ n = 1 := by
        simpa using congrArg Subtype.val (hpow ⟨α a, haK⟩)
      rw [hpowQ]
      exact (⁅K, K⁆).one_mem
  have hQ : α w ∈ ⁅K, K⁆ := hrel_le hw
  have hQmap : α w ∈ (commutator β.ker).map β.ker.subtype := by
    simpa [K, Subgroup.map_subtype_commutator] using hQ
  rcases hQmap with ⟨c, hc, hcval⟩
  have hc_eq :
      c =
        (⟨α w, by
          change β (α w) = 1
          simpa [MonoidHom.mem_ker, MonoidHom.comp_apply] using hwker⟩ : β.ker) := by
    apply Subtype.ext
    exact hcval
  simpa [hc_eq] using hc
theorem

mem_commutator_ker_of_mem_foxCommutatorPowerSubgroup_card

L361 ↗
FoxDifferential.mem_commutator_ker_of_mem_foxCommutatorPowerSubgroup_card
Documentation

The finite-kernel cardinality version of the quotient bookkeeping lemma.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped commutatorElement
universe u v
variable {X : Type u}
variable {Q H : Type u}
variable [Group Q] [Group H]
Lean source · full declaration
theorem mem_commutator_ker_of_mem_foxCommutatorPowerSubgroup_card
    (α : FreeGroup X →* Q) (β : Q →* H)
    {w : FreeGroup X}
    (hwker : w ∈ (β.comp α).ker)
    (hw :
      w ∈ foxCommutatorPowerSubgroup
        (F := FreeGroup X) (β.comp α).ker (Nat.card β.ker)) :
    (⟨α w, by
      change β (α w) = 1
      simpa [MonoidHom.mem_ker, MonoidHom.comp_apply] using hwker⟩ : β.ker) ∈
      commutator β.ker := by
  exact
    mem_commutator_ker_of_mem_foxCommutatorPowerSubgroup_of_pow_eq_one
      (X := X) α β (Nat.card β.ker) (fun _ => pow_card_eq_one') hwker hw
theorem

mem_commutator_ker_of_foxAlgebraicStageDerivativeVector_eq_zero_of_ker_le

L381 ↗
FoxDifferential.mem_commutator_ker_of_foxAlgebraicStageDerivativeVector_eq_zero_of_ker_le
Documentation

Finite quotient commutator conclusion from the finite-stage Magnus reverse inclusion. Once the kernel of the finite-stage lift has been identified with \([N,N]N^m\), a zero finite-stage derivative for a representative word gives the ordinary commutator conclusion in kernel \beta.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped commutatorElement
universe u v
variable {X : Type u}
variable {Q H : Type u}
variable [Group Q] [Group H]
Lean source · full declaration
theorem mem_commutator_ker_of_foxAlgebraicStageDerivativeVector_eq_zero_of_ker_le
    [DecidableEq X]
    (α : FreeGroup X →* Q) (β : Q →* H) (n : ℕ)
    (hpow : ∀ k : β.ker, k ^ n = 1)
    (hmag :
      (foxAlgebraicStageLift (X := X) (β.comp α).ker n).ker ≤
        foxCommutatorPowerSubgroup (F := FreeGroup X) (β.comp α).ker n)
    {w : FreeGroup X}
    (hwker : w ∈ (β.comp α).ker)
    (hder :
      foxAlgebraicStageDerivativeVector (X := X) (β.comp α).ker n w = 0) :
    (⟨α w, by
      change β (α w) = 1
      simpa [MonoidHom.mem_ker, MonoidHom.comp_apply] using hwker⟩ : β.ker) ∈
      commutator β.ker := by
  have hwrel :
      w ∈ foxCommutatorPowerSubgroup (F := FreeGroup X) (β.comp α).ker n :=
    hmag
      ((mem_ker_foxAlgebraicStageLift_iff
        (X := X) (N := (β.comp α).ker) (n := n)).2
        ⟨hwker, hder⟩)
  exact
    mem_commutator_ker_of_mem_foxCommutatorPowerSubgroup_of_pow_eq_one
      (X := X) α β n hpow hwker hwrel
theorem

mem_commutator_ker_of_residueUniversalDifferential_eq_zero_of_kernel_le

L409 ↗
FoxDifferential.mem_commutator_ker_of_residueUniversalDifferential_eq_zero_of_kernel_le
Documentation

Finite quotient commutator conclusion from the residue-universal finite Magnus kernel statement.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped commutatorElement
universe u v
variable {X : Type u}
variable {Q H : Type u}
variable [Group Q] [Group H]
Lean source · full declaration
theorem mem_commutator_ker_of_residueUniversalDifferential_eq_zero_of_kernel_le
    (α : FreeGroup X →* Q) (β : Q →* H) (n : ℕ)
    (hpow : ∀ k : β.ker, k ^ n = 1)
    (hmag :
      ∀ w : FreeGroup X,
        w ∈ (β.comp α).ker →
        residueUniversalDifferential n (QuotientGroup.mk' (β.comp α).ker) w = 0 →
          w ∈ foxCommutatorPowerSubgroup
            (F := FreeGroup X) (β.comp α).ker n)
    {w : FreeGroup X}
    (hwker : w ∈ (β.comp α).ker)
    (hder :
      residueUniversalDifferential n (QuotientGroup.mk' (β.comp α).ker) w = 0) :
    (⟨α w, by
      change β (α w) = 1
      simpa [MonoidHom.mem_ker, MonoidHom.comp_apply] using hwker⟩ : β.ker) ∈
      commutator β.ker := by
  exact
    mem_commutator_ker_of_mem_foxCommutatorPowerSubgroup_of_pow_eq_one
      (X := X) α β n hpow hwker (hmag w hwker hder)
theorem

mem_commutator_ker_of_foxAlgebraicStageDerivativeVector_eq_zero_of_ker_le_card

L434 ↗
FoxDifferential.mem_commutator_ker_of_foxAlgebraicStageDerivativeVector_eq_zero_of_ker_le_card
Documentation

The cardinality-specialized finite quotient commutator conclusion from the finite-stage Magnus reverse inclusion.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped commutatorElement
universe u v
variable {X : Type u}
variable {Q H : Type u}
variable [Group Q] [Group H]
Lean source · full declaration
theorem mem_commutator_ker_of_foxAlgebraicStageDerivativeVector_eq_zero_of_ker_le_card
    [DecidableEq X]
    (α : FreeGroup X →* Q) (β : Q →* H)
    (hmag :
      (foxAlgebraicStageLift (X := X) (β.comp α).ker (Nat.card β.ker)).ker ≤
        foxCommutatorPowerSubgroup
          (F := FreeGroup X) (β.comp α).ker (Nat.card β.ker))
    {w : FreeGroup X}
    (hwker : w ∈ (β.comp α).ker)
    (hder :
      foxAlgebraicStageDerivativeVector (X := X) (β.comp α).ker (Nat.card β.ker) w = 0) :
    (⟨α w, by
      change β (α w) = 1
      simpa [MonoidHom.mem_ker, MonoidHom.comp_apply] using hwker⟩ : β.ker) ∈
      commutator β.ker := by
  exact
    mem_commutator_ker_of_foxAlgebraicStageDerivativeVector_eq_zero_of_ker_le
      (X := X) α β (Nat.card β.ker) (fun _ => pow_card_eq_one') hmag hwker hder
theorem

mem_commutator_ker_of_residueUniversalDifferential_eq_zero_of_kernel_le_card

L457 ↗
FoxDifferential.mem_commutator_ker_of_residueUniversalDifferential_eq_zero_of_kernel_le_card
Documentation

The cardinality-specialized finite quotient commutator conclusion from the residue-universal finite Magnus kernel statement.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped commutatorElement
universe u v
variable {X : Type u}
variable {Q H : Type u}
variable [Group Q] [Group H]
Lean source · full declaration
theorem mem_commutator_ker_of_residueUniversalDifferential_eq_zero_of_kernel_le_card
    (α : FreeGroup X →* Q) (β : Q →* H)
    (hmag :
      ∀ w : FreeGroup X,
        w ∈ (β.comp α).ker →
        residueUniversalDifferential (Nat.card β.ker)
            (QuotientGroup.mk' (β.comp α).ker) w = 0 →
          w ∈ foxCommutatorPowerSubgroup
            (F := FreeGroup X) (β.comp α).ker (Nat.card β.ker))
    {w : FreeGroup X}
    (hwker : w ∈ (β.comp α).ker)
    (hder :
      residueUniversalDifferential (Nat.card β.ker)
          (QuotientGroup.mk' (β.comp α).ker) w = 0) :
    (⟨α w, by
      change β (α w) = 1
      simpa [MonoidHom.mem_ker, MonoidHom.comp_apply] using hwker⟩ : β.ker) ∈
      commutator β.ker := by
  exact
    mem_commutator_ker_of_residueUniversalDifferential_eq_zero_of_kernel_le
      (X := X) α β (Nat.card β.ker) (fun _ => pow_card_eq_one') hmag hwker hder

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