Module

MagnusKernel.lean

Nyll.ProCGroups.FoxDifferential.Discrete.KernelBoundary.MagnusKernel

2 declarations indexed from sourceView source ↗

Module documentation

Fox differential: discrete — kernel boundary — magnus kernel

The principal declarations in this module are:

kernelAbelianizationBoundaryLinearOfSurjective_injective

The surjective-case linear kernel-boundary map is injective in the Magnus-kernel comparison.

mem_commutator_ker_of_d_eq_zero_of_surjective

Discrete Magnus-kernel form of the injectivity theorem: for a surjective \(\psi\), if the Crowell/Fox differential of a kernel element vanishes, then that element already lies in the ordinary commutator subgroup of \(\ker \psi\).

Imports1

Nyll.ProCGroups.FoxDifferential.Discrete.KernelBoundary.Homology

Imported by3

theorem

kernelAbelianizationBoundaryLinearOfSurjective_injective

L34 ↗

FoxDifferential.KernelAugmentation.kernelAbelianizationBoundaryLinearOfSurjective_injective

Documentation

The surjective-case linear kernel-boundary map is injective in the Magnus-kernel comparison.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
namespace KernelAugmentation
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
variable {ψ : G →* H}
omit [DecidableEq H] in
omit [DecidableEq H] [DecidableEq G] in

Lean source · full declaration

theorem kernelAbelianizationBoundaryLinearOfSurjective_injective
    (hψ : Function.Surjective ψ) :
    letI := kernelAbelianizationModuleOfSurjective ψ hψ
    Function.Injective (kernelAbelianizationBoundaryLinearOfSurjective ψ hψ) := by
  let := kernelAbelianizationModuleOfSurjective ψ hψ
  let := kernelAugmentationIdealCoinvariantsModuleOfSurjective (ψ := ψ) hψ
  intro x y hxy
  have hcoinv :
      kernelAbelianizationToCoinvariantsLinear (ψ := ψ) x =
        kernelAbelianizationToCoinvariantsLinear (ψ := ψ) y := by
    calc
      kernelAbelianizationToCoinvariantsLinear (ψ := ψ) x =
          differentialToKernelAugmentationIdealCoinvariantsLinearOfSurjective (ψ := ψ) hψ
            (kernelAbelianizationBoundaryLinearOfSurjective ψ hψ x) := by
              symm
              exact differentialToKernelAugmentationIdealCoinvariantsLinearOfSurjective_boundary
                (ψ := ψ) hψ x
      _ =
          differentialToKernelAugmentationIdealCoinvariantsLinearOfSurjective (ψ := ψ) hψ
            (kernelAbelianizationBoundaryLinearOfSurjective ψ hψ y) := by
              simp only [hxy, kernelAbelianizationBoundaryLinearOfSurjective_apply]
      _ = kernelAbelianizationToCoinvariantsLinear (ψ := ψ) y := by
            exact differentialToKernelAugmentationIdealCoinvariantsLinearOfSurjective_boundary
              (ψ := ψ) hψ y
  exact (kernelAbelianizationToCoinvariantsLinear_injective (H := H) (ψ := ψ) hψ) hcoinv

theorem

mem_commutator_ker_of_d_eq_zero_of_surjective

L66 ↗

FoxDifferential.KernelAugmentation.mem_commutator_ker_of_d_eq_zero_of_surjective

Documentation

Source context 6 commands

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

namespace FoxDifferential
noncomputable section
namespace KernelAugmentation
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
variable {ψ : G →* H}
omit [DecidableEq H] [DecidableEq G] in

Lean source · statement

theorem mem_commutator_ker_of_d_eq_zero_of_surjective
    (hψ : Function.Surjective ψ) (n : ψ.ker) (hn : universalDifferential ψ n.1 = 0) :
    n ∈ commutator ψ.ker

Module documentation

Fox differential: discrete — kernel boundary — magnus kernel

Declarations

kernelAbelianizationBoundaryLinearOfSurjective_injective

mem_commutator_ker_of_d_eq_zero_of_surjective