ProCGroups.FoxDifferential.Discrete.KernelBoundary.Basic

15 Theorems | 12 Definitions | 2 Abbreviations

The principal declarations in this module are:

KernelAbelianizationAdd Additive form of the kernel abelianization map. - kernelBoundary The kernel of \(\psi\) maps multiplicatively into the additive differential module via d. - augmentation_toGroupRing_eq_zero The Crowell boundary map lands in the kernel of the augmentation map. - augmentation_surjective The augmentation map \(\mathbb{Z}[H] \to \mathbb{Z}\) is surjective.

import

ProCGroups.FoxDifferential.Discrete.KernelBoundary.IdentityAugmentation

Imported by

Abbreviation FoxDifferential.KernelAbelianizationAdd

abbrev KernelAbelianizationAdd (ψ : G →* H) : Type _ :=
  Additive (Abelianization ψ.ker)

Additive form of the kernel abelianization map.

Theorem FoxDifferential.augmentation_toGroupRing_eq_zero

omit [DecidableEq H] [DecidableEq G] in
theorem augmentation_toGroupRing_eq_zero (ψ : G →* H) (x : DifferentialModule ψ) :
    augmentation H (toGroupRing ψ x) = 0

The Crowell boundary map lands in the kernel of the augmentation map.

Show Lean proof

Theorem FoxDifferential.augmentation_surjective

omit [DecidableEq H] in
theorem augmentation_surjective : Function.Surjective (augmentation H)

The augmentation map \(\mathbb{Z}[H] \to \mathbb{Z}\) is surjective.

Show Lean proof

Theorem FoxDifferential.exact_toGroupRing_augmentation

omit [DecidableEq H] [DecidableEq G] in
theorem exact_toGroupRing_augmentation (ψ : G →* H) (hψ : Function.Surjective ψ) :
    Function.Exact (fun x => toGroupRing ψ x) (augmentation H)

Tail exactness of the discrete Crowell sequence: \(A_{\psi}\) \(\to\) \(\mathbb{Z}[H]\) \(\to\) \(\mathbb{Z}\) is used when \(\psi\) is surjective.

Show Lean proof

Definition FoxDifferential.kernelBoundary

def kernelBoundary (ψ : G →* H) : ψ.ker →* Multiplicative (DifferentialModule ψ) where
  toFun g := Multiplicative.ofAdd (universalDifferential ψ g.1)
  map_one' := by
    apply congrArg Multiplicative.ofAdd
    simp only [OneMemClass.coe_one, universalDifferential_one]
  map_mul' g₁ g₂ := by
    apply congrArg Multiplicative.ofAdd
    have h := universalDifferential_mul ψ g₁.1 g₂.1
    have hψ : (MonoidAlgebra.of ℤ H (ψ g₁.1) : GroupRing H) = 1 := by
      rw [g₁.2, groupRing_of_one (H := H)]
    rw [hψ, one_smul] at h
    simpa using h

The kernel of \(\psi\) maps multiplicatively into the additive differential module via d.

Definition FoxDifferential.kernelAbelianizationBoundary

def kernelAbelianizationBoundary (ψ : G →* H) :
    Abelianization ψ.ker →* Multiplicative (DifferentialModule ψ) :=
  Abelianization.lift (kernelBoundary ψ)

The kernel boundary factors through the abelianization of \(\ker \psi\).

Definition FoxDifferential.kernelAbelianizationBoundaryAdd

def kernelAbelianizationBoundaryAdd (ψ : G →* H) :
    Additive (Abelianization ψ.ker) →+ DifferentialModule ψ where
  toFun x := Multiplicative.toAdd (kernelAbelianizationBoundary ψ (Additive.toMul x))
  map_zero' := by
    simp only [toMul_zero, map_one, toAdd_one]
  map_add' x y := by
    simp only [toMul_add, map_mul, toAdd_mul]

The additive kernel-boundary map sends a kernel element to its abelianization boundary class.

Theorem FoxDifferential.kernelAbelianizationBoundaryAdd_of

omit [DecidableEq H] [DecidableEq G] in
@[simp 900]
theorem kernelAbelianizationBoundaryAdd_of (ψ : G →* H) (g : ψ.ker) :
    kernelAbelianizationBoundaryAdd ψ (Additive.ofMul (Abelianization.of g)) =
        universalDifferential ψ g.1

The additive kernel-boundary map has the stated value on a kernel element.

Show Lean proof

Definition FoxDifferential.kernelAbelianizationConj

def kernelAbelianizationConj (ψ : G →* H) :
    G →* MulAut (Abelianization ψ.ker) where
  toFun g := (MulAut.conjNormal (H := ψ.ker) g).abelianizationCongr
  map_one' := by
    ext x
    refine QuotientGroup.induction_on x ?_
    intro n
    have hconj : MulAut.conjNormal (H := ψ.ker) (1 : G) = 1 := by
      ext m
      simp only [map_one, MulAut.one_apply]
    rw [hconj]
    rfl
  map_mul' g₁ g₂ := by
    ext x
    refine QuotientGroup.induction_on x ?_
    intro n
    let e₁ : MulAut ψ.ker := MulAut.conjNormal (H := ψ.ker) g₁
    let e₂ : MulAut ψ.ker := MulAut.conjNormal (H := ψ.ker) g₂
    have hconj : MulAut.conjNormal (H := ψ.ker) (g₁ * g₂) = e₁ * e₂ := by
      ext m
      simp only [map_mul, MulAut.mul_apply, MulAut.conjNormal_apply, mul_assoc, e₁, e₂]
    rw [hconj]
    calc
      (e₁ * e₂).abelianizationCongr (Abelianization.of n)
          = Abelianization.of ((e₁ * e₂) n) := by
              exact abelianizationCongr_of (e := e₁ * e₂) n
      _ = e₁.abelianizationCongr (Abelianization.of (e₂ n)) := by
            exact (abelianizationCongr_of (e := e₁) (e₂ n)).symm
      _ = e₁.abelianizationCongr (e₂.abelianizationCongr (Abelianization.of n)) := by
            rw [abelianizationCongr_of (e := e₂) n]
      _ = (e₁.abelianizationCongr * e₂.abelianizationCongr) (Abelianization.of n) := by
            rfl

Conjugation by G on \(\ker \psi\), transported to the abelianization of \(\ker \psi\).

Theorem FoxDifferential.kernelAbelianizationConj_of

omit [DecidableEq H] [DecidableEq G] in
@[simp]
theorem kernelAbelianizationConj_of (ψ : G →* H) (g : G) (n : ψ.ker) :
    kernelAbelianizationConj ψ g (Abelianization.of n) =
      Abelianization.of (MulAut.conjNormal (H := ψ.ker) g n)

The conjugation action on kernel abelianization is computed by the displayed representative formula.

Show Lean proof

Theorem FoxDifferential.kernelAbelianizationConj_eq_one_of_mem_ker

omit [DecidableEq H] [DecidableEq G] in
@[simp]
theorem kernelAbelianizationConj_eq_one_of_mem_ker (ψ : G →* H) (n : ψ.ker) :
    kernelAbelianizationConj ψ n = 1

Conjugation by a kernel element becomes trivial in the kernel abelianization.

Show Lean proof

Theorem FoxDifferential.ker_le_kernelAbelianizationConj_ker

omit [DecidableEq H] [DecidableEq G] in
theorem ker_le_kernelAbelianizationConj_ker (ψ : G →* H) :
    ψ.ker ≤ (kernelAbelianizationConj ψ).ker

Elements in the kernel of \(\psi\) act trivially after passing to the kernel abelianization action.

Show Lean proof

Definition FoxDifferential.quotientKernelAbelianizationConj

def quotientKernelAbelianizationConj (ψ : G →* H) :
    G ⧸ ψ.ker →* MulAut (Abelianization ψ.ker) :=
  QuotientGroup.lift ψ.ker (kernelAbelianizationConj ψ) (ker_le_kernelAbelianizationConj_ker ψ)

The conjugation action on the abelianization of \(\ker \psi\) factors through \(G/\ker \psi\).

Definition FoxDifferential.kernelAbelianizationConjOfSurjective

omit [DecidableEq H] [DecidableEq G] in
def kernelAbelianizationConjOfSurjective
    (ψ : G →* H) (hψ : Function.Surjective ψ) :
    H →* MulAut (Abelianization ψ.ker) :=
  (quotientKernelAbelianizationConj ψ).comp
    (QuotientGroup.quotientKerEquivOfSurjective (φ := ψ) hψ).symm.toMonoidHom

If \(\psi\) is surjective, the conjugation action on the abelianization of \(\ker \psi\) is expressed directly as an action of H.

Theorem FoxDifferential.kernelAbelianizationConjOfSurjective_eq_surjInv

omit [DecidableEq H] [DecidableEq G] in
@[simp 900]
theorem kernelAbelianizationConjOfSurjective_eq_surjInv
    (ψ : G →* H) (hψ : Function.Surjective ψ) (h : H) :
    kernelAbelianizationConjOfSurjective ψ hψ h =
      kernelAbelianizationConj ψ (Function.surjInv hψ h)

For a surjective \(\psi\), the induced action on the kernel abelianization agrees with conjugation by a chosen preimage.

Show Lean proof

Definition FoxDifferential.kernelAbelianizationAddAutOfSurjective

def kernelAbelianizationAddAutOfSurjective
    (ψ : G →* H) (hψ : Function.Surjective ψ) :
    H →* Multiplicative (AddAut (KernelAbelianizationAdd ψ)) :=
  (AddAutAdditive (Abelianization ψ.ker)).symm.toAddMonoidHom.toMultiplicativeRight.comp
    (kernelAbelianizationConjOfSurjective ψ hψ)

For a surjective homomorphism, the conjugation action on the kernel abelianization is rewritten as an additive automorphism action.

Definition FoxDifferential.kernelAbelianizationAddAutToModuleEnd

omit [DecidableEq H] [DecidableEq G] in
def kernelAbelianizationAddAutToModuleEnd (ψ : G →* H) :
    Multiplicative (AddAut (KernelAbelianizationAdd ψ)) →*
      Module.End ℤ (KernelAbelianizationAdd ψ) where
  toFun e := e.toAdd.toIntLinearEquiv.toLinearMap
  map_one' := by
    ext x
    change (0 : AddAut (KernelAbelianizationAdd ψ)) x = x
    rfl
  map_mul' e₁ e₂ := by
    ext x
    change (e₁.toAdd + e₂.toAdd) x = e₁.toAdd (e₂.toAdd x)
    rfl

An additive automorphism of the kernel abelianization determines its underlying \(\mathbb{Z}\)-linear endomorphism.

Definition FoxDifferential.kernelAbelianizationModuleEndOfSurjective

def kernelAbelianizationModuleEndOfSurjective
    (ψ : G →* H) (hψ : Function.Surjective ψ) :
    H →* Module.End ℤ (KernelAbelianizationAdd ψ) where
  toFun h := kernelAbelianizationAddAutToModuleEnd (ψ := ψ)
    (kernelAbelianizationAddAutOfSurjective ψ hψ h)
  map_one' := by
    rw [(kernelAbelianizationAddAutOfSurjective ψ hψ).map_one]
    ext x
    rfl
  map_mul' h₁ h₂ := by
    rw [(kernelAbelianizationAddAutOfSurjective ψ hψ).map_mul]
    ext x
    rfl

The surjective-case action as a hom into \(\mathbb{Z}\)-linear endomorphisms.

Theorem FoxDifferential.kernelAbelianizationModuleEndOfSurjective_apply

omit [DecidableEq H] [DecidableEq G] in
@[simp]
theorem kernelAbelianizationModuleEndOfSurjective_apply
    (ψ : G →* H) (hψ : Function.Surjective ψ) (h : H) (x : KernelAbelianizationAdd ψ) :
    kernelAbelianizationModuleEndOfSurjective ψ hψ h x =
      Additive.ofMul (kernelAbelianizationConjOfSurjective ψ hψ h (Additive.toMul x))

The module endomorphism associated to h acts by the conjugation automorphism obtained from a chosen lift of h.

Show Lean proof

Definition FoxDifferential.kernelAbelianizationActionRingHomOfSurjective

def kernelAbelianizationActionRingHomOfSurjective
    (ψ : G →* H) (hψ : Function.Surjective ψ) :
    GroupRing H →+* Module.End ℤ (KernelAbelianizationAdd ψ) :=
  MonoidAlgebra.liftNCRingHom (Int.castRingHom (Module.End ℤ (KernelAbelianizationAdd ψ)))
    (kernelAbelianizationModuleEndOfSurjective ψ hψ) (by
      intro z h
      ext x
      simp only [eq_intCast, Module.End.mul_apply, kernelAbelianizationModuleEndOfSurjective_apply,
  kernelAbelianizationConjOfSurjective_eq_surjInv, Module.End.intCast_apply, toMul_zsmul,
      toMul_ofMul, map_smul])

The induced \(\mathbb{Z}[H]\)-action on \((\ker \psi)^{\mathrm{ab}}\), written in additive form.

Theorem FoxDifferential.kernelAbelianizationActionRingHomOfSurjective_of

omit [DecidableEq H] [DecidableEq G] in
@[simp]
theorem kernelAbelianizationActionRingHomOfSurjective_of
    (ψ : G →* H) (hψ : Function.Surjective ψ) (h : H) :
    kernelAbelianizationActionRingHomOfSurjective ψ hψ (MonoidAlgebra.of ℤ H h) =
      kernelAbelianizationModuleEndOfSurjective ψ hψ h

The surjective-case group-ring action on kernel abelianization has the displayed value on representatives.

Show Lean proof

Definition FoxDifferential.kernelAbelianizationModuleOfSurjective

@[reducible]
def kernelAbelianizationModuleOfSurjective
    (ψ : G →* H) (hψ : Function.Surjective ψ) :
    Module (GroupRing H) (KernelAbelianizationAdd ψ) :=
  Module.compHom _ (kernelAbelianizationActionRingHomOfSurjective ψ hψ)

The \(\mathbb{Z}[H]\)-module structure on \(\ker(\psi)^{\mathrm{ab}}\) induced by surjective conjugation.

Theorem FoxDifferential.kernelAbelianizationBoundaryAdd_conjOfSurjective

omit [DecidableEq H] [DecidableEq G] in
@[simp]
theorem kernelAbelianizationBoundaryAdd_conjOfSurjective
    (ψ : G →* H) (hψ : Function.Surjective ψ) (h : H) (x : Abelianization ψ.ker) :
    kernelAbelianizationBoundaryAdd ψ
        (Additive.ofMul (kernelAbelianizationConjOfSurjective ψ hψ h x)) =
      (MonoidAlgebra.of ℤ H h : GroupRing H) •
        kernelAbelianizationBoundaryAdd ψ (Additive.ofMul x)

For a surjective \(\psi\), the additive kernel-boundary map intertwines the induced conjugation action with scalar multiplication by the corresponding group-ring basis element.

Show Lean proof

Theorem FoxDifferential.kernelAbelianizationBoundaryAdd_commOfSurjective

omit [DecidableEq H] [DecidableEq G] in
@[simp]
theorem kernelAbelianizationBoundaryAdd_commOfSurjective
    (ψ : G →* H) (hψ : Function.Surjective ψ) (h : H) (x : KernelAbelianizationAdd ψ) :
    letI := kernelAbelianizationModuleOfSurjective ψ hψ
    kernelAbelianizationBoundaryAdd ψ ((MonoidAlgebra.of ℤ H h : GroupRing H) • x) =
      (MonoidAlgebra.of ℤ H h : GroupRing H) • kernelAbelianizationBoundaryAdd ψ x

The kernel-boundary additive map is compatible with the surjective-case group-ring action.

Show Lean proof

Definition FoxDifferential.kernelAbelianizationBoundaryLinearOfSurjective

def kernelAbelianizationBoundaryLinearOfSurjective
    (ψ : G →* H) (hψ : Function.Surjective ψ) :
    letI := kernelAbelianizationModuleOfSurjective ψ hψ
    KernelAbelianizationAdd ψ →ₗ[GroupRing H] DifferentialModule ψ := by
  letI := kernelAbelianizationModuleOfSurjective ψ hψ
  let f : KernelAbelianizationAdd ψ →ₗ[ℤ] DifferentialModule ψ :=
    (kernelAbelianizationBoundaryAdd ψ).toIntLinearMap
  exact MonoidAlgebra.equivariantOfLinearOfComm f
    (fun h x => by
      exact kernelAbelianizationBoundaryAdd_commOfSurjective (ψ := ψ) hψ h x)

The head map of the discrete Crowell sequence, in \(\mathbb{Z}[H]\)-linear form when \(\psi\) is surjective.

Theorem FoxDifferential.kernelAbelianizationBoundaryLinearOfSurjective_of

omit [DecidableEq H] [DecidableEq G] in
@[simp]
theorem kernelAbelianizationBoundaryLinearOfSurjective_of
    (ψ : G →* H) (hψ : Function.Surjective ψ) (n : ψ.ker) :
    kernelAbelianizationBoundaryLinearOfSurjective ψ hψ
        (Additive.ofMul (Abelianization.of n)) = universalDifferential ψ n.1

The linear kernel-boundary map in the surjective case has the stated value on a kernel element.

Show Lean proof

Theorem FoxDifferential.kernelAbelianizationBoundaryLinearOfSurjective_apply

omit [DecidableEq H] [DecidableEq G] in
@[simp]
theorem kernelAbelianizationBoundaryLinearOfSurjective_apply
    (ψ : G →* H) (hψ : Function.Surjective ψ) (x : KernelAbelianizationAdd ψ) :
    kernelAbelianizationBoundaryLinearOfSurjective ψ hψ x =
      kernelAbelianizationBoundaryAdd ψ x

The kernel-abelianization boundary map is evaluated on canonical generators and then extended linearly.

Show Lean proof

Theorem FoxDifferential.toGroupRing_kernelAbelianizationBoundaryLinearOfSurjective

omit [DecidableEq H] [DecidableEq G] in
@[simp]
theorem toGroupRing_kernelAbelianizationBoundaryLinearOfSurjective
    (ψ : G →* H) (hψ : Function.Surjective ψ) (x : KernelAbelianizationAdd ψ) :
    toGroupRing ψ (kernelAbelianizationBoundaryLinearOfSurjective ψ hψ x) = 0

Composing the surjective-case kernel-boundary map with the group-ring map gives the expected group-ring boundary.

Show Lean proof

Abbreviation FoxDifferential.kernelAbelianizationBoundaryRangeOfSurjective

abbrev kernelAbelianizationBoundaryRangeOfSurjective
    (ψ : G →* H) (hψ : Function.Surjective ψ) :
    Submodule (GroupRing H) (DifferentialModule ψ) := by
  letI := kernelAbelianizationModuleOfSurjective ψ hψ
  exact LinearMap.range (kernelAbelianizationBoundaryLinearOfSurjective ψ hψ)

The \(A_{\psi}\)-submodule generated by the head map in the surjective case.

ProCGroups.FoxDifferential.Discrete.KernelBoundary.Basic

Declarations