ProCGroups.FoxDifferential.Discrete.KernelBoundary.Homology

26 Theorems | 22 Definitions | 7 Abbreviations | 1 Instance

The principal declarations in this module are:

kernelGroupRingRep The left-multiplication representation of \(\ker \psi\) on \(\mathbb{Z}[G]\). - kernelSplitEquiv A section-based decomposition G \(\simeq\) \(\ker \psi\) \(\times\) H. - kernelSplitEquiv_smul The kernel-splitting equivalence is equivariant for the left action of \(\ker\psi\): acting by \(n\) before applying the equivalence is the same as acting by \(n\) afterward. - indBottomKernelUnderlyingEquiv_mk The bottom-kernel induced-module equivalence sends the representative indexed by \(g\in\ker\psi\) and \(a\in \mathbb{Z}[H]\) to the tensor of the singleton at \(g\) with \(a\).

imports

Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence
ProCGroups.FoxDifferential.Discrete.KernelBoundary.Basic

Imported by

Instance FoxDifferential.instMulActionKernelCodomainTrivial

instance instMulActionKernelCodomainTrivial : MulAction ↥(ψ.ker) H where
  smul _ h := h
  one_smul _ := rfl
  mul_smul _ _ _ := rfl

The kernel-boundary codomain carries the trivial multiplication action.

Abbreviation FoxDifferential.kernelGroupRingRep

abbrev kernelGroupRingRep : Rep ℤ ↥(ψ.ker) :=
  Rep.ofMulAction ℤ ↥(ψ.ker) G

The left-multiplication representation of \(\ker \psi\) on \(\mathbb{Z}[G]\).

Definition FoxDifferential.kernelSplitEquiv

def kernelSplitEquiv : G ≃ ↥(ψ.ker) × H where
  toFun g :=
    (⟨g * (Function.surjInv hψ (ψ g))⁻¹, by
        simp only [MonoidHom.mem_ker, map_mul, map_inv, Function.surjInv_eq hψ (ψ g),
            mul_inv_cancel]⟩, ψ g)
  invFun x := x.1.1 * Function.surjInv hψ x.2
  left_inv g := by
    simp only [mul_assoc, inv_mul_cancel, mul_one]
  right_inv x := by
    rcases x with ⟨n, h⟩
    apply Prod.ext
    · apply Subtype.ext
      change
        n.1 * Function.surjInv hψ h *
            (Function.surjInv hψ (ψ (n.1 * Function.surjInv hψ h)))⁻¹ = n.1
      rw [map_mul, n.2, Function.surjInv_eq hψ h]
      simp only [one_mul, mul_assoc, mul_inv_cancel, mul_one]
    · change ψ (n.1 * Function.surjInv hψ h) = h
      rw [map_mul, n.2, one_mul, Function.surjInv_eq hψ h]

A section-based decomposition G \(\simeq\) \(\ker \psi\) \(\times\) H.

Theorem FoxDifferential.kernelSplitEquiv_smul

omit [DecidableEq H] [DecidableEq G] in
@[simp]
theorem kernelSplitEquiv_smul (n : ↥(ψ.ker)) (g : G) :
    kernelSplitEquiv ψ hψ (n • g) = n • kernelSplitEquiv ψ hψ g

The kernel-splitting equivalence is equivariant for the left action of \(\ker\psi\): acting by \(n\) before applying the equivalence is the same as acting by \(n\) afterward.

Show Lean proof

Abbreviation FoxDifferential.kernelRightTensorRep

abbrev kernelRightTensorRep : Rep ℤ ↥(ψ.ker) :=
  rightRegularRep ↥(ψ.ker) ⊗ Rep.trivial ℤ ↥(ψ.ker) (H →₀ ℤ)

The \(\ker \psi\)-representation on \(\mathbb{Z}[\ker \psi\] \otimes \mathbb{Z}[H]\) whose first factor is right-regular and whose second factor is trivial.

Definition FoxDifferential.kernelGroupRingRepIsoRightTensor

def kernelGroupRingRepIsoRightTensor :
    kernelGroupRingRep (ψ := ψ) ≅ kernelRightTensorRep (H := H) (ψ := ψ) := by
  let e₁ :
      GroupRing G ≃ₗ[ℤ] ((↥(ψ.ker) × H) →₀ ℤ) :=
    (MonoidAlgebra.coeffLinearEquiv ℤ).trans
      (Finsupp.domLCongr (kernelSplitEquiv ψ hψ))
  let e₂ :
      ((↥(ψ.ker) × H) →₀ ℤ) ≃ₗ[ℤ] (GroupRing ↥(ψ.ker)) ⊗[ℤ] (H →₀ ℤ) :=
    (finsuppTensorFinsupp' ℤ ↥(ψ.ker) H).symm.trans
      (TensorProduct.congr
        ((Finsupp.domLCongr (Equiv.inv ↥(ψ.ker))).trans
          (MonoidAlgebra.coeffLinearEquiv ℤ).symm)
        (LinearEquiv.refl ℤ (H →₀ ℤ)))
  refine Rep.mkIso (Representation.Equiv.mk (e₁.trans e₂) ?_)
  intro n
  apply LinearMap.toAddMonoidHom_injective
  apply MonoidAlgebra.addMonoidHom_ext
  intro g r
  have hcalc :
      e₂ (Finsupp.single (n • kernelSplitEquiv ψ hψ g) r) =
        ((kernelRightTensorRep (ψ := ψ) (H := H)).ρ n)
          (e₂ (Finsupp.single (kernelSplitEquiv ψ hψ g) r)) := by
    change e₂ (Finsupp.single (n • kernelSplitEquiv ψ hψ g) r) =
      TensorProduct.map ((rightRegularRepresentation ↥(ψ.ker)) n) LinearMap.id
        (e₂ (Finsupp.single (kernelSplitEquiv ψ hψ g) r))
    cases hkg : kernelSplitEquiv ψ hψ g with
    | mk m h =>
        simp only [e₂, LinearEquiv.trans_apply,
          finsuppTensorFinsupp'_symm_single_eq_single_one_tmul, TensorProduct.congr_tmul,
          TensorProduct.map_tmul, LinearEquiv.refl_apply]
        have hnm :
            (((Finsupp.domLCongr (Equiv.inv ↥(ψ.ker))).trans
                (MonoidAlgebra.coeffLinearEquiv ℤ).symm)
              (Finsupp.single (n * m) (1 : ℤ))) =
              MonoidAlgebra.single ((n * m)⁻¹) (1 : ℤ) := by
          ext x
          simp only [LinearEquiv.trans_apply, Finsupp.domLCongr_apply, Finsupp.domCongr_apply,
            Finsupp.equivMapDomain_single, Equiv.inv_apply, mul_inv_rev,
            MonoidAlgebra.coeffLinearEquiv_symm_apply, MonoidAlgebra.coeff_single]
        have hm :
            (((Finsupp.domLCongr (Equiv.inv ↥(ψ.ker))).trans
                (MonoidAlgebra.coeffLinearEquiv ℤ).symm)
              (Finsupp.single m (1 : ℤ))) =
              MonoidAlgebra.single m⁻¹ (1 : ℤ) := by
          ext x
          simp only [LinearEquiv.trans_apply, Finsupp.domLCongr_apply, Finsupp.domCongr_apply,
            Finsupp.equivMapDomain_single, Equiv.inv_apply,
            MonoidAlgebra.coeffLinearEquiv_symm_apply, MonoidAlgebra.coeff_single]
        change
          (((Finsupp.domLCongr (Equiv.inv ↥(ψ.ker))).trans
              (MonoidAlgebra.coeffLinearEquiv ℤ).symm)
            (Finsupp.single (n * m) (1 : ℤ))) ⊗ₜ[ℤ] Finsupp.single h r =
            ((rightRegularRepresentation ↥(ψ.ker)) n)
              ((((Finsupp.domLCongr (Equiv.inv ↥(ψ.ker))).trans
                  (MonoidAlgebra.coeffLinearEquiv ℤ).symm)
                (Finsupp.single m (1 : ℤ)))) ⊗ₜ[ℤ] Finsupp.single h r
        rw [hnm, hm]
        simp only [mul_inv_rev, rightRegularRepresentation_apply_single]
  change
    e₂
        (e₁
          (((kernelGroupRingRep (ψ := ψ)).ρ n) (MonoidAlgebra.single g r))) =
      ((kernelRightTensorRep (ψ := ψ) (H := H)).ρ n)
        (e₂ (e₁ (MonoidAlgebra.single g r)))
  simpa [kernelGroupRingRep, kernelRightTensorRep, e₁,
    LinearEquiv.trans_apply, kernelSplitEquiv_smul, MonoidAlgebra.coeffLinearEquiv_apply,
    Representation.ofMulAction_single, Rep.tensor_ρ] using hcalc

The section decomposition, rewritten as a representation isomorphism to a right-regular tensor model.

Definition FoxDifferential.indBottomKernelUnderlyingEquiv

def indBottomKernelUnderlyingEquiv :
    Representation.IndV (⊥ : Subgroup ↥(ψ.ker)).subtype
      (Rep.trivial ℤ (⊥ : Subgroup ↥(ψ.ker)) (H →₀ ℤ)).ρ
      ≃ₗ[ℤ] (GroupRing ↥(ψ.ker)) ⊗[ℤ] (H →₀ ℤ) := by
  let ρt :
      Representation ℤ (⊥ : Subgroup ↥(ψ.ker))
        (TensorProduct ℤ (GroupRing ↥(ψ.ker)) (H →₀ ℤ)) :=
    Representation.tprod
      (((Rep.leftRegular ℤ ↥(ψ.ker)).ρ.comp (⊥ : Subgroup ↥(ψ.ker)).subtype))
      (Rep.trivial ℤ (⊥ : Subgroup ↥(ψ.ker)) (H →₀ ℤ)).ρ
  exact coinvariantsLEquivOfSubsingleton ρt

The trivial representation of the trivial subgroup of \(\ker \psi\) on the free \(\mathbb{Z}\)-module \(\mathbb{Z}[H]\).

Theorem FoxDifferential.indBottomKernelUnderlyingEquiv_mk

omit [DecidableEq H] [DecidableEq G] in
@[simp 900]
theorem indBottomKernelUnderlyingEquiv_mk (g : ↥(ψ.ker)) (a : H →₀ ℤ) :
    indBottomKernelUnderlyingEquiv (H := H) (ψ := ψ)
      (Representation.IndV.mk (⊥ : Subgroup ↥(ψ.ker)).subtype
        (Rep.trivial ℤ (⊥ : Subgroup ↥(ψ.ker)) (H →₀ ℤ)).ρ g a) =
        MonoidAlgebra.single g 1 ⊗ₜ[ℤ] a

The bottom-kernel induced-module equivalence sends the representative indexed by \(g\in\ker\psi\) and \(a\in \mathbb{Z}[H]\) to the tensor of the singleton at \(g\) with \(a\).

Show Lean proof

Definition FoxDifferential.indBottomKernelIsoRightTensor

def indBottomKernelIsoRightTensor :
    Rep.ind (⊥ : Subgroup ↥(ψ.ker)).subtype
        (Rep.trivial ℤ (⊥ : Subgroup ↥(ψ.ker)) (H →₀ ℤ)) ≅
      kernelRightTensorRep (ψ := ψ) (H := H) := by
  refine Rep.mkIso (Representation.Equiv.mk
    (indBottomKernelUnderlyingEquiv (H := H) (ψ := ψ)) ?_)
  intro g
  apply Representation.IndV.hom_ext (φ := (⊥ : Subgroup ↥(ψ.ker)).subtype)
    (ρ := (Rep.trivial ℤ (⊥ : Subgroup ↥(ψ.ker)) (H →₀ ℤ)).ρ)
  · intro h
    apply LinearMap.ext
    intro a
    change
      indBottomKernelUnderlyingEquiv (H := H) (ψ := ψ)
        (((Rep.ind (⊥ : Subgroup ↥(ψ.ker)).subtype
            (Rep.trivial ℤ (⊥ : Subgroup ↥(ψ.ker)) (H →₀ ℤ))).ρ g)
          ((Representation.IndV.mk (⊥ : Subgroup ↥(ψ.ker)).subtype
            (Rep.trivial ℤ (⊥ : Subgroup ↥(ψ.ker)) (H →₀ ℤ)).ρ h) a)) =
        ((kernelRightTensorRep (ψ := ψ) (H := H)).ρ g)
          (indBottomKernelUnderlyingEquiv (H := H) (ψ := ψ)
            ((Representation.IndV.mk (⊥ : Subgroup ↥(ψ.ker)).subtype
              (Rep.trivial ℤ (⊥ : Subgroup ↥(ψ.ker)) (H →₀ ℤ)).ρ h) a))
    have hind :
        (((Rep.ind (⊥ : Subgroup ↥(ψ.ker)).subtype
            (Rep.trivial ℤ (⊥ : Subgroup ↥(ψ.ker)) (H →₀ ℤ))).ρ g)
          ((Representation.IndV.mk (⊥ : Subgroup ↥(ψ.ker)).subtype
            (Rep.trivial ℤ (⊥ : Subgroup ↥(ψ.ker)) (H →₀ ℤ)).ρ h) a)) =
        (Representation.IndV.mk (⊥ : Subgroup ↥(ψ.ker)).subtype
          (Rep.trivial ℤ (⊥ : Subgroup ↥(ψ.ker)) (H →₀ ℤ)).ρ (h * g⁻¹)) a := by
      exact Representation.ind_mk
        (φ := (⊥ : Subgroup ↥(ψ.ker)).subtype)
        (ρ := (Rep.trivial ℤ (⊥ : Subgroup ↥(ψ.ker)) (H →₀ ℤ)).ρ) g h a
    rw [hind, indBottomKernelUnderlyingEquiv_mk, indBottomKernelUnderlyingEquiv_mk]
    change MonoidAlgebra.single (h * g⁻¹) 1 ⊗ₜ[ℤ] a =
      TensorProduct.map ((rightRegularRepresentation ↥(ψ.ker)) g) LinearMap.id
        (MonoidAlgebra.single h 1 ⊗ₜ[ℤ] a)
    simp only [map_tmul, rightRegularRepresentation_apply_single, LinearMap.id_coe, id_eq]

\(\operatorname{Ind}_{1}^{\ker \psi}(\mathbb{Z}[H])\) is the right-regular tensor model.

Abbreviation FoxDifferential.groupRingRep

abbrev groupRingRep : Rep ℤ G :=
  Rep.ofMulAction ℤ G G

The left-regular representation of \(G\) on \(\mathbb{Z}[G]\).

Theorem FoxDifferential.groupRingRep_apply_single

omit [DecidableEq G] in
@[simp]
theorem groupRingRep_apply_single (g h : G) (m : ℤ) :
    ((groupRingRep (G := G)).ρ g) (MonoidAlgebra.single h m) =
      MonoidAlgebra.single (g * h) m

The group-ring representation sends a singleton basis element to the singleton at the product.

Show Lean proof

Theorem FoxDifferential.kernelGroupRingRep_apply_single

omit [DecidableEq H] [DecidableEq G] in
@[simp]
theorem kernelGroupRingRep_apply_single (n : ψ.ker) (g : G) (m : ℤ) :
    ((kernelGroupRingRep (ψ := ψ)).ρ n) (MonoidAlgebra.single g m) =
      MonoidAlgebra.single (n • g) m

The kernel group-ring representation sends a singleton basis element to the singleton at the product.

Show Lean proof

Theorem FoxDifferential.augmentation_kernelGroupRingRep

omit [DecidableEq H] [DecidableEq G] in
theorem augmentation_kernelGroupRingRep
    (n : ψ.ker) (x : GroupRing G) :
    augmentation G (((kernelGroupRingRep (ψ := ψ)).ρ n) x) = augmentation G x

The left-regular group-ring representation preserves the augmentation-kernel condition.

Show Lean proof

Theorem FoxDifferential.augmentation_groupRingRep

omit [DecidableEq G] in
theorem augmentation_groupRingRep
    (g : G) (x : GroupRing G) :
    augmentation G (((groupRingRep (G := G)).ρ g) x) = augmentation G x

Left multiplication by \(g : G\) preserves the group-ring augmentation.

Show Lean proof

Abbreviation FoxDifferential.groupAugmentationIdealRep

abbrev groupAugmentationIdealRep : Rep ℤ G :=
  Rep.of (X := augmentationIdeal G)
    { toFun := fun g =>
        { toFun := fun x =>
            ⟨((groupRingRep (G := G)).ρ g) x.1, by
              rw [mem_augmentationIdeal_iff]
              rw [augmentation_groupRingRep (G := G) g x.1]
              exact (mem_augmentationIdeal_iff (H := G) (x := x.1)).1 x.2⟩
          map_add' := by
            intro x y
            apply Subtype.ext
            exact map_add ((groupRingRep (G := G)).ρ g) x.1 y.1
          map_smul' := by
            intro m x
            apply Subtype.ext
            exact map_smul ((groupRingRep (G := G)).ρ g) m x.1 }
      map_one' := by
        ext x h
        simp only [groupRingRep, map_one, Module.End.one_apply, Subtype.coe_eta,
          LinearMap.coe_mk, AddHom.coe_mk]
      map_mul' := by
        intro g₁ g₂
        ext x h
        simp only [groupRingRep, map_mul, Module.End.mul_apply, LinearMap.coe_mk,
          AddHom.coe_mk]}

The left-regular G-action preserves the augmentation ideal \(I(\mathbb{Z}[G])\).

Abbreviation FoxDifferential.kernelAugmentationIdealRep

abbrev kernelAugmentationIdealRep : Rep ℤ ↥(ψ.ker) :=
  Rep.of (X := augmentationIdeal G)
    { toFun := fun n =>
        { toFun := fun x =>
            ⟨((kernelGroupRingRep (ψ := ψ)).ρ n) x.1, by
              rw [mem_augmentationIdeal_iff]
              rw [augmentation_kernelGroupRingRep (ψ := ψ) n x.1]
              exact (mem_augmentationIdeal_iff (H := G) (x := x.1)).1 x.2⟩
          map_add' := by
            intro x y
            apply Subtype.ext
            exact map_add ((kernelGroupRingRep (ψ := ψ)).ρ n) x.1 y.1
          map_smul' := by
            intro m x
            apply Subtype.ext
            exact map_smul ((kernelGroupRingRep (ψ := ψ)).ρ n) m x.1 }
      map_one' := by
        ext x g
        simp only [kernelGroupRingRep, map_one, Module.End.one_apply, Subtype.coe_eta,
          LinearMap.coe_mk, AddHom.coe_mk]
      map_mul' := by
        intro n₁ n₂
        ext x g
        simp only [kernelGroupRingRep, map_mul, Module.End.mul_apply, LinearMap.coe_mk,
          AddHom.coe_mk]}

The kernel-restricted action of \(\ker \psi\) on the augmentation ideal \(I(\mathbb{Z}[G])\).

Definition FoxDifferential.kernelAugmentationIdealInclusion

def kernelAugmentationIdealInclusion :
    kernelAugmentationIdealRep (ψ := ψ) ⟶ kernelGroupRingRep (ψ := ψ) :=
  Rep.ofHom <| Representation.IntertwiningMap.mk
    ((augmentationIdeal G).subtype.restrictScalars ℤ) fun _ => rfl

The inclusion \(I(\mathbb{Z}[G])\hookrightarrow \mathbb{Z}[G]\) as a morphism of \(\ker \psi\)-representations.

Definition FoxDifferential.kernelGroupRingAugmentation

def kernelGroupRingAugmentation :
    kernelGroupRingRep (ψ := ψ) ⟶ Rep.trivial ℤ ↥(ψ.ker) ℤ :=
  Rep.ofHom <| Representation.IntertwiningMap.mk
    ((augmentation G).toAddMonoidHom.toIntLinearMap) fun n => by
      apply LinearMap.toAddMonoidHom_injective
      apply MonoidAlgebra.addMonoidHom_ext
      intro g m
      change augmentation G (((kernelGroupRingRep (ψ := ψ)).ρ n)
          (MonoidAlgebra.single g m)) =
        ((Rep.trivial ℤ ↥(ψ.ker) ℤ).ρ n) (augmentation G (MonoidAlgebra.single g m))
      rw [kernelGroupRingRep_apply_single]
      simp only [augmentation, augmentationAlgHom,
        AlgHom.toRingHom_eq_coe, RingHom.coe_coe, MonoidAlgebra.lift_single,
        MonoidHom.one_apply, Int.zsmul_eq_mul, mul_one, isTrivial_def, LinearMap.id_coe, id_eq]

The augmentation map \(\mathbb{Z}[G] \to \mathbb{Z}\) as a morphism of \(\ker \psi\)-representations.

Definition FoxDifferential.kernelAugmentationShortComplex

def kernelAugmentationShortComplex :
    CategoryTheory.ShortComplex (Rep ℤ ↥(ψ.ker)) :=
  CategoryTheory.ShortComplex.mk
    (kernelAugmentationIdealInclusion (ψ := ψ))
    (kernelGroupRingAugmentation (ψ := ψ))
    (by
      ext x
      exact x.2)

The augmentation ideal \(I(\mathbb{Z}[G])\), the group ring \(\mathbb{Z}[G]\), and the augmentation \(\mathbb{Z}[G]\to\mathbb{Z}\) form the short complex \(0\to I(\mathbb{Z}[G])\to\mathbb{Z}[G]\to\mathbb{Z}\to 0\) of \(\ker \psi\)-representations.

Theorem FoxDifferential.kernelAugmentationShortComplex_exact

omit [DecidableEq H] [DecidableEq G] in
theorem kernelAugmentationShortComplex_exact :
    (kernelAugmentationShortComplex (ψ := ψ)).Exact

The kernel-augmentation short complex is exact: the augmentation ideal maps onto the kernel of the group-ring augmentation.

Show Lean proof

Theorem FoxDifferential.kernelAugmentationShortExact

omit [DecidableEq H] [DecidableEq G] in
theorem kernelAugmentationShortExact :
    (kernelAugmentationShortComplex (ψ := ψ)).ShortExact

The canonical augmentation sequence with augmentation ideal as kernel is short exact: the inclusion is injective, its image is the kernel of augmentation, and the augmentation is surjective.

Show Lean proof

Abbreviation FoxDifferential.kernelTrivialIntRep

abbrev kernelTrivialIntRep : Rep ℤ ↥(ψ.ker) :=
  Rep.trivial ℤ ↥(ψ.ker) ℤ

The trivial integral representation of \(\ker\psi\).

Definition FoxDifferential.kernelAugmentationConnecting

def kernelAugmentationConnecting :
    groupHomology (kernelTrivialIntRep (ψ := ψ)) 1 ⟶
      groupHomology (kernelAugmentationIdealRep (ψ := ψ)) 0 :=
  groupHomology.δ
    (X := kernelAugmentationShortComplex (ψ := ψ))
    (kernelAugmentationShortExact (ψ := ψ))
    1 0 rfl

The connecting homomorphism \(H_1(\ker \psi, \mathbb{Z})\) \(\to\) \(H_0(\ker \psi, I(\mathbb{Z}[G]))\) attached to the short exact sequence 0 \(\to\) \(I(\mathbb{Z}[G])\) \(\to\) \(\mathbb{Z}[G]\) \(\to\) \(\mathbb{Z}\) \(\to\) 0 of \(\ker \psi\)-representations.

Definition FoxDifferential.kernelTrivialH1AddEquivAbelianization

def kernelTrivialH1AddEquivAbelianization :
    groupHomology (kernelTrivialIntRep (ψ := ψ)) 1 ≃+
      Additive (Abelianization ψ.ker) :=
  (groupHomology.H1AddEquivOfIsTrivial (kernelTrivialIntRep (ψ := ψ))).trans
    (TensorProduct.rid ℤ (Additive (Abelianization ψ.ker))).toAddEquiv

The standard low-degree identification \(H_1(\ker \psi, \mathbb{Z}) \simeq (\ker \psi)^{\mathrm{ab}}\).

Theorem FoxDifferential.kernelTrivialH1AddEquivAbelianization_symm_of

omit [DecidableEq H] [DecidableEq G] in
@[simp]
theorem kernelTrivialH1AddEquivAbelianization_symm_of (n : ψ.ker) :
    (kernelTrivialH1AddEquivAbelianization (ψ := ψ)).symm
        (Additive.ofMul (Abelianization.of n)) =
      groupHomology.H1π (kernelTrivialIntRep (ψ := ψ))
        ((groupHomology.cycles₁IsoOfIsTrivial (kernelTrivialIntRep (ψ := ψ))).inv
          (Finsupp.single n 1))

The inverse of the \(H_1\)-abelianization equivalence sends the abelianization class of \(n\in\ker\psi\) to the degree-one homology class represented by the singleton cycle at \(n\).

Show Lean proof

Theorem FoxDifferential.kernelAugmentationConnecting_boundaryCycle_of

omit [DecidableEq H] [DecidableEq G] in
theorem kernelAugmentationConnecting_boundaryCycle_of (n : ψ.ker) :
    Finsupp.mapRange.linearMap (kernelAugmentationShortComplex (ψ := ψ)).g.hom.toLinearMap
      (Finsupp.single n (MonoidAlgebra.single n.1 (1 : ℤ))) =
    ((groupHomology.cycles₁IsoOfIsTrivial (kernelTrivialIntRep (ψ := ψ))).inv
      (Finsupp.single n 1)).1

The connecting morphism sends a boundary cycle to the corresponding augmentation-coinvariant class.

Show Lean proof

Theorem FoxDifferential.kernelAugmentationConnecting_boundaryElement_of

omit [DecidableEq H] [DecidableEq G] in
theorem kernelAugmentationConnecting_boundaryElement_of (n : ψ.ker) :
    (kernelAugmentationShortComplex (ψ := ψ)).f.hom
      (-(augmentationGeneratorSubtype (H := G) n.1)) =
    groupHomology.d₁₀ (kernelGroupRingRep (ψ := ψ))
      (Finsupp.single n (MonoidAlgebra.single n.1 (1 : ℤ)))

The connecting morphism has the displayed representative on a boundary element.

Show Lean proof

Theorem FoxDifferential.kernelAugmentationConnecting_H0Iso_of

omit [DecidableEq H] [DecidableEq G] in
theorem kernelAugmentationConnecting_H0Iso_of (n : ψ.ker) :
    (groupHomology.H0Iso (kernelAugmentationIdealRep (ψ := ψ))).hom.hom
      ((kernelAugmentationConnecting (ψ := ψ)).hom
        ((kernelTrivialH1AddEquivAbelianization (ψ := ψ)).symm
          (Additive.ofMul (Abelianization.of n)))) =
      -Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
          (augmentationGeneratorSubtype (H := G) n.1)

The connecting morphism matches the corresponding degree-zero coinvariant class.

Show Lean proof

Theorem FoxDifferential.kernelAugmentationConnecting_injective

omit [DecidableEq H] [DecidableEq G] in
theorem kernelAugmentationConnecting_injective
    (hψ : Function.Surjective ψ) :
    Function.Injective (kernelAugmentationConnecting (ψ := ψ)).hom

The kernel-augmentation connecting map is injective.

Show Lean proof

Abbreviation FoxDifferential.KernelAugmentationIdealCoinvariants

abbrev KernelAugmentationIdealCoinvariants (ψ : G →* H) : Type _ :=
  Representation.Coinvariants ((kernelAugmentationIdealRep (ψ := ψ)).ρ)

The coinvariants of the kernel augmentation ideal are formed from the ordinary group-ring augmentation ideal.

Theorem FoxDifferential.kernelAugmentationIdealRep_rho_eq_groupAugmentationIdealRep_rho

omit [DecidableEq H] [DecidableEq G] in
@[simp 900]
theorem kernelAugmentationIdealRep_rho_eq_groupAugmentationIdealRep_rho
    (n : ψ.ker) :
    (kernelAugmentationIdealRep (ψ := ψ)).ρ n =
      (groupAugmentationIdealRep (G := G)).ρ n.1

The kernel augmentation-ideal representative agrees with the corresponding group augmentation-ideal representative.

Show Lean proof

Definition FoxDifferential.kernelAugmentationIdealCoinvariantsEndOfSurjective

def kernelAugmentationIdealCoinvariantsEndOfSurjective
    (hψ : Function.Surjective ψ) (h : H) :
    KernelAugmentationIdealCoinvariants (ψ := ψ) →ₗ[ℤ]
      KernelAugmentationIdealCoinvariants (ψ := ψ) :=
  Representation.Coinvariants.lift ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
    ((Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)).comp
      ((groupAugmentationIdealRep (G := G)).ρ (Function.surjInv hψ h)))
    (by
      intro n
      ext x
      let s : G := Function.surjInv hψ h
      have hs : ψ s = h := by
        simpa [s] using Function.surjInv_eq hψ h
      let n' : ψ.ker := ⟨s * n.1 * s⁻¹, by
        change ψ (s * n.1 * s⁻¹) = 1
        rw [map_mul, map_mul, n.2, map_inv, hs]
        simp only [mul_one, mul_inv_cancel]⟩
      have hs_mul :
          ((groupAugmentationIdealRep (G := G)).ρ s)
              (((groupAugmentationIdealRep (G := G)).ρ n.1) x) =
            ((groupAugmentationIdealRep (G := G)).ρ (s * n.1)) x := by
        exact congrArg
          (fun f : augmentationIdeal G →ₗ[ℤ] augmentationIdeal G => f x)
          (((groupAugmentationIdealRep (G := G)).ρ).map_mul s n.1).symm
      have hs'_mul :
          ((groupAugmentationIdealRep (G := G)).ρ n'.1)
              (((groupAugmentationIdealRep (G := G)).ρ s) x) =
            ((groupAugmentationIdealRep (G := G)).ρ (n'.1 * s)) x := by
        exact congrArg
          (fun f : augmentationIdeal G →ₗ[ℤ] augmentationIdeal G => f x)
          (((groupAugmentationIdealRep (G := G)).ρ).map_mul n'.1 s).symm
      calc
        Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
            (((groupAugmentationIdealRep (G := G)).ρ s)
              (((kernelAugmentationIdealRep (ψ := ψ)).ρ n) x))
            = Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
                (((groupAugmentationIdealRep (G := G)).ρ s)
                  (((groupAugmentationIdealRep (G := G)).ρ n.1) x)) := by
                    rw [kernelAugmentationIdealRep_rho_eq_groupAugmentationIdealRep_rho
                      (ψ := ψ) n]
        _ = Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
              (((groupAugmentationIdealRep (G := G)).ρ (s * n.1)) x) := by
                rw [hs_mul]
        _ = Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
              (((groupAugmentationIdealRep (G := G)).ρ (n'.1 * s)) x) := by
                congr 1
                simp only [MonoidHom.coe_mk, OneHom.coe_mk, map_mul, Module.End.mul_apply,
                    LinearMap.coe_mk,
  AddHom.coe_mk, mul_assoc, inv_mul_cancel, mul_one, s, n']
        _ = Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
              (((groupAugmentationIdealRep (G := G)).ρ n'.1)
                (((groupAugmentationIdealRep (G := G)).ρ s) x)) := by
                  rw [hs'_mul]
        _ = Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
              (((kernelAugmentationIdealRep (ψ := ψ)).ρ n')
                (((groupAugmentationIdealRep (G := G)).ρ s) x)) := by
                  rw [kernelAugmentationIdealRep_rho_eq_groupAugmentationIdealRep_rho
                    (ψ := ψ) n']
        _ = Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
              (((groupAugmentationIdealRep (G := G)).ρ s) x) := by
                exact Representation.Coinvariants.mk_self_apply
                  ((kernelAugmentationIdealRep (ψ := ψ)).ρ) n'
                  (((groupAugmentationIdealRep (G := G)).ρ s) x))

The \(H\)-action on \(H_0(\ker \psi, I(\mathbb{Z}[G]))\), built from a surjective section.

Theorem FoxDifferential.kernelAugmentationIdealCoinvariantsEndOfSurjective_mk

omit [DecidableEq H] [DecidableEq G] in
@[simp 900]
theorem kernelAugmentationIdealCoinvariantsEndOfSurjective_mk
    (hψ : Function.Surjective ψ) (h : H) (x : augmentationIdeal G) :
    kernelAugmentationIdealCoinvariantsEndOfSurjective (ψ := ψ) hψ h
        (Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ) x) =
      Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
        (((groupAugmentationIdealRep (G := G)).ρ (Function.surjInv hψ h)) x)

The surjective-case endomorphism of kernel augmentation coinvariants is evaluated on representatives.

Show Lean proof

Definition FoxDifferential.kernelAugmentationIdealCoinvariantsModuleEndOfSurjective

def kernelAugmentationIdealCoinvariantsModuleEndOfSurjective
    (hψ : Function.Surjective ψ) :
    H →* Module.End ℤ (KernelAugmentationIdealCoinvariants (ψ := ψ)) where
  toFun h := kernelAugmentationIdealCoinvariantsEndOfSurjective (ψ := ψ) hψ h
  map_one' := by
    apply Representation.Coinvariants.hom_ext
    ext x
    rw [LinearMap.comp_apply]
    rw [kernelAugmentationIdealCoinvariantsEndOfSurjective_mk (ψ := ψ) hψ]
    let n : ψ.ker := ⟨Function.surjInv hψ (1 : H), by
      simpa using Function.surjInv_eq hψ (1 : H)⟩
    rw [← kernelAugmentationIdealRep_rho_eq_groupAugmentationIdealRep_rho
      (ψ := ψ) n]
    simpa [n] using
      (Representation.Coinvariants.mk_self_apply ((kernelAugmentationIdealRep (ψ := ψ)).ρ) n x)
  map_mul' h₁ h₂ := by
    apply Representation.Coinvariants.hom_ext
    ext x
    let s₁ : G := Function.surjInv hψ h₁
    let s₂ : G := Function.surjInv hψ h₂
    let s₁₂ : G := Function.surjInv hψ (h₁ * h₂)
    have hs₁ : ψ s₁ = h₁ := by
      simpa [s₁] using Function.surjInv_eq hψ h₁
    have hs₂ : ψ s₂ = h₂ := by
      simpa [s₂] using Function.surjInv_eq hψ h₂
    have hs₁₂ : ψ s₁₂ = h₁ * h₂ := by
      simpa [s₁₂] using Function.surjInv_eq hψ (h₁ * h₂)
    let n : ψ.ker := ⟨s₁ * s₂ * s₁₂⁻¹, by
      change ψ (s₁ * s₂ * s₁₂⁻¹) = 1
      rw [map_mul, map_mul, hs₁, hs₂, map_inv, hs₁₂]
      simp only [mul_inv_rev, mul_assoc, mul_inv_cancel_left, mul_inv_cancel]⟩
    have hs :
        ((groupAugmentationIdealRep (G := G)).ρ s₁)
            (((groupAugmentationIdealRep (G := G)).ρ s₂) x) =
          ((groupAugmentationIdealRep (G := G)).ρ (s₁ * s₂)) x := by
      exact congrArg
        (fun f : augmentationIdeal G →ₗ[ℤ] augmentationIdeal G => f x)
        (((groupAugmentationIdealRep (G := G)).ρ).map_mul s₁ s₂).symm
    rw [LinearMap.comp_apply, LinearMap.comp_apply]
    change
      Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
        (((groupAugmentationIdealRep (G := G)).ρ s₁₂) x) =
      kernelAugmentationIdealCoinvariantsEndOfSurjective (ψ := ψ) hψ h₁
        (kernelAugmentationIdealCoinvariantsEndOfSurjective (ψ := ψ) hψ h₂
          (Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ) x))
    rw [kernelAugmentationIdealCoinvariantsEndOfSurjective_mk (ψ := ψ) hψ,
      kernelAugmentationIdealCoinvariantsEndOfSurjective_mk (ψ := ψ) hψ]
    calc
      Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
          (((groupAugmentationIdealRep (G := G)).ρ s₁₂) x)
          =
        Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
          (((kernelAugmentationIdealRep (ψ := ψ)).ρ n)
            (((groupAugmentationIdealRep (G := G)).ρ s₁₂) x)) := by
              rw [Representation.Coinvariants.mk_self_apply]
      _ = Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
            (((groupAugmentationIdealRep (G := G)).ρ n.1)
              (((groupAugmentationIdealRep (G := G)).ρ s₁₂) x)) := by
                rw [kernelAugmentationIdealRep_rho_eq_groupAugmentationIdealRep_rho
                  (ψ := ψ) n]
      _ = Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
            (((groupAugmentationIdealRep (G := G)).ρ (n.1 * s₁₂)) x) := by
              have hs' :
                  ((groupAugmentationIdealRep (G := G)).ρ n.1)
                      (((groupAugmentationIdealRep (G := G)).ρ s₁₂) x) =
                    ((groupAugmentationIdealRep (G := G)).ρ (n.1 * s₁₂)) x := by
                  exact congrArg
                    (fun f : augmentationIdeal G →ₗ[ℤ] augmentationIdeal G => f x)
                    (((groupAugmentationIdealRep (G := G)).ρ).map_mul n.1 s₁₂).symm
              rw [hs']
      _ = Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
            (((groupAugmentationIdealRep (G := G)).ρ (s₁ * s₂)) x) := by
              congr 1
              simp only [mul_assoc, inv_mul_cancel, mul_one, MonoidHom.coe_mk, OneHom.coe_mk,
                  map_mul,
  Module.End.mul_apply, LinearMap.coe_mk, AddHom.coe_mk, s₁, s₂, s₁₂, n]
      _ = Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
            (((groupAugmentationIdealRep (G := G)).ρ s₁)
              (((groupAugmentationIdealRep (G := G)).ρ s₂) x)) := by
                rw [hs]

In the surjective case, the \(H\)-action on \(H_0(\ker\psi, I(\mathbb{Z}[G]))\) is bundled as linear endomorphisms.

Definition FoxDifferential.kernelAugmentationIdealCoinvariantsActionRingHomOfSurjective

def kernelAugmentationIdealCoinvariantsActionRingHomOfSurjective
    (hψ : Function.Surjective ψ) :
    GroupRing H →+* Module.End ℤ (KernelAugmentationIdealCoinvariants (ψ := ψ)) :=
  MonoidAlgebra.liftNCRingHom
    (Int.castRingHom (Module.End ℤ (KernelAugmentationIdealCoinvariants (ψ := ψ))))
    (kernelAugmentationIdealCoinvariantsModuleEndOfSurjective (ψ := ψ) hψ)
    (by
      intro z h
      apply LinearMap.ext
      intro x
      change z •
          kernelAugmentationIdealCoinvariantsModuleEndOfSurjective (ψ := ψ) hψ h x =
        kernelAugmentationIdealCoinvariantsModuleEndOfSurjective (ψ := ψ) hψ h (z • x)
      rw [map_zsmul])

The ring action of \(\mathbb{Z}[H]\) on \(H_0(\ker \psi, I(\mathbb{Z}[G]))\) induced by a surjective section.

Theorem FoxDifferential.kernelAugmentationIdealCoinvariantsActionRingHomOfSurjective_of

omit [DecidableEq H] [DecidableEq G] in
@[simp]
theorem kernelAugmentationIdealCoinvariantsActionRingHomOfSurjective_of
    (hψ : Function.Surjective ψ) (h : H) :
    kernelAugmentationIdealCoinvariantsActionRingHomOfSurjective (ψ := ψ) hψ
        (MonoidAlgebra.of ℤ H h) =
      kernelAugmentationIdealCoinvariantsModuleEndOfSurjective (ψ := ψ) hψ h

The surjective-case coefficient action on coinvariants has the displayed value on representatives.

Show Lean proof

Definition FoxDifferential.kernelAugmentationIdealCoinvariantsModuleOfSurjective

@[reducible] def kernelAugmentationIdealCoinvariantsModuleOfSurjective
    (hψ : Function.Surjective ψ) :
    Module (GroupRing H) (KernelAugmentationIdealCoinvariants (ψ := ψ)) :=
  Module.compHom _
    (kernelAugmentationIdealCoinvariantsActionRingHomOfSurjective (ψ := ψ) hψ)

The induced \(\mathbb{Z}[H]\)-module structure on \(H_0(\ker \psi, I(\mathbb{Z}[G]))\).

Theorem FoxDifferential.augmentationGeneratorSubtype_mul

omit [DecidableEq G] in
@[simp]
theorem augmentationGeneratorSubtype_mul (g₁ g₂ : G) :
    augmentationGeneratorSubtype (H := G) (g₁ * g₂) =
      augmentationGeneratorSubtype (H := G) g₁ +
        ((groupAugmentationIdealRep (G := G)).ρ g₁)
          (augmentationGeneratorSubtype (H := G) g₂)

The augmentation-generator identity \((g_1g_2-1)=(g_1-1)+g_1(g_2-1)\) inside \(I(\mathbb{Z}[G])\).

Show Lean proof

Definition FoxDifferential.kernelCoinvariantsBoundary

def kernelCoinvariantsBoundary (ψ : G →* H) :
    ψ.ker →* Multiplicative (KernelAugmentationIdealCoinvariants (ψ := ψ)) where
  toFun n := Multiplicative.ofAdd <|
    Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
      (augmentationGeneratorSubtype (H := G) n.1)
  map_one' := by
    apply Multiplicative.toAdd.injective
    have hzero : augmentationGeneratorSubtype (H := G) (1 : G) = 0 := by
      apply Subtype.ext
      simp only [augmentationGeneratorSubtype, augmentationGenerator, groupRing_of_one (H := G),
          sub_self,
  ZeroMemClass.coe_zero]
    simp only [OneMemClass.coe_one, hzero, map_zero, ofAdd_zero, toAdd_one]
  map_mul' n₁ n₂ := by
    apply Multiplicative.toAdd.injective
    change
      Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
        (augmentationGeneratorSubtype (H := G) (n₁.1 * n₂.1)) =
      Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
          (augmentationGeneratorSubtype (H := G) n₁.1) +
        Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
          (augmentationGeneratorSubtype (H := G) n₂.1)
    rw [augmentationGeneratorSubtype_mul, map_add]
    congr 1
    calc
      Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
          (((groupAugmentationIdealRep (G := G)).ρ n₁.1)
            (augmentationGeneratorSubtype (H := G) n₂.1))
        = Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
            (((kernelAugmentationIdealRep (ψ := ψ)).ρ n₁)
              (augmentationGeneratorSubtype (H := G) n₂.1)) := by
              rw [kernelAugmentationIdealRep_rho_eq_groupAugmentationIdealRep_rho (ψ := ψ) n₁]
      _ = Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
            (augmentationGeneratorSubtype (H := G) n₂.1) := by
              exact Representation.Coinvariants.mk_self_apply
                ((kernelAugmentationIdealRep (ψ := ψ)).ρ) n₁
                (augmentationGeneratorSubtype (H := G) n₂.1)

Kernel elements map to \(H_0(\ker \psi, I(\mathbb{Z}[G]))\) by \(n \mapsto [n - 1]\).

Definition FoxDifferential.kernelAbelianizationToCoinvariants

def kernelAbelianizationToCoinvariants (ψ : G →* H) :
    Abelianization ψ.ker →* Multiplicative (KernelAugmentationIdealCoinvariants (ψ := ψ)) :=
  Abelianization.lift (kernelCoinvariantsBoundary (ψ := ψ))

The map \(n \mapsto [n-1]\) factors through the abelianization of \(\ker \psi\).

Definition FoxDifferential.kernelAbelianizationToCoinvariantsAdd

def kernelAbelianizationToCoinvariantsAdd (ψ : G →* H) :
    KernelAbelianizationAdd ψ →+ KernelAugmentationIdealCoinvariants (ψ := ψ) where
  toFun x := Multiplicative.toAdd (kernelAbelianizationToCoinvariants (ψ := ψ) (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]

Additive form of the map \((\ker \psi)^{\mathrm{ab}} \to H_0(\ker \psi, I(\mathbb{Z}[G]))\).

Theorem FoxDifferential.kernelAbelianizationToCoinvariantsAdd_of

omit [DecidableEq H] [DecidableEq G] in
@[simp]
theorem kernelAbelianizationToCoinvariantsAdd_of (n : ψ.ker) :
    kernelAbelianizationToCoinvariantsAdd (ψ := ψ)
        (Additive.ofMul (Abelianization.of n)) =
      Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
        (augmentationGeneratorSubtype (H := G) n.1)

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

Show Lean proof

Definition FoxDifferential.kernelAbelianizationToCoinvariantsLinear

def kernelAbelianizationToCoinvariantsLinear (ψ : G →* H) :
    KernelAbelianizationAdd ψ →ₗ[ℤ] KernelAugmentationIdealCoinvariants (ψ := ψ) :=
  (kernelAbelianizationToCoinvariantsAdd (ψ := ψ)).toIntLinearMap

\(\mathbb{Z}\)-linear form of the map \((\ker \psi)^{\mathrm{ab}} \to H_0(\ker \psi, I(\mathbb{Z}[G]))\).

Definition FoxDifferential.kernelAbelianizationToCoinvariantsViaConnectingAdd

def kernelAbelianizationToCoinvariantsViaConnectingAdd (ψ : G →* H) :
    KernelAbelianizationAdd ψ →+ KernelAugmentationIdealCoinvariants (ψ := ψ) where
  toFun x :=
    -((groupHomology.H0Iso (kernelAugmentationIdealRep (ψ := ψ))).hom.hom
      ((kernelAugmentationConnecting (ψ := ψ)).hom
        ((kernelTrivialH1AddEquivAbelianization (ψ := ψ)).symm x)))
  map_zero' := by
    simp only [coinvariantsFunctor_obj_carrier, map_zero, neg_zero]
  map_add' x y := by
    rw [(kernelTrivialH1AddEquivAbelianization (ψ := ψ)).symm.map_add]
    simp only [coinvariantsFunctor_obj_carrier, map_add, neg_add_rev]
    abel_nf

The low-degree homology comparison \((\ker \psi)^{\mathrm{ab}} \to H_0(\ker \psi, I(\mathbb{Z}[G]))\) obtained from the connecting morphism \(H_1(\ker \psi, \mathbb{Z}) \to H_0(\ker \psi, I(\mathbb{Z}[G]))\). Our convention for \(\delta_0\) introduces a minus sign on generators.

Definition FoxDifferential.kernelAbelianizationToCoinvariantsViaConnectingLinear

def kernelAbelianizationToCoinvariantsViaConnectingLinear (ψ : G →* H) :
    KernelAbelianizationAdd ψ →ₗ[ℤ] KernelAugmentationIdealCoinvariants (ψ := ψ) :=
  (kernelAbelianizationToCoinvariantsViaConnectingAdd (ψ := ψ)).toIntLinearMap

\(\mathbb{Z}\)-linear form of the connecting-morphism comparison \((\ker \psi)^{\mathrm{ab}} \to H_0(\ker \psi, I(\mathbb{Z}[G]))\).

Theorem FoxDifferential.kernelAbelianizationToCoinvariantsViaConnectingAdd_of

omit [DecidableEq H] [DecidableEq G] in
@[simp]
theorem kernelAbelianizationToCoinvariantsViaConnectingAdd_of (n : ψ.ker) :
    kernelAbelianizationToCoinvariantsViaConnectingAdd (ψ := ψ)
        (Additive.ofMul (Abelianization.of n)) =
      Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
        (augmentationGeneratorSubtype (H := G) n.1)

The connecting-morphism comparison sends a kernel element to the corresponding augmentation-coinvariant class.

Show Lean proof

Theorem FoxDifferential.kernelAbelianizationToCoinvariantsViaConnectingLinear_of

omit [DecidableEq H] [DecidableEq G] in
@[simp]
theorem kernelAbelianizationToCoinvariantsViaConnectingLinear_of (n : ψ.ker) :
    kernelAbelianizationToCoinvariantsViaConnectingLinear (ψ := ψ)
        (Additive.ofMul (Abelianization.of n)) =
      Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
        (augmentationGeneratorSubtype (H := G) n.1)

The linear connecting-morphism comparison has the stated value on a kernel element.

Show Lean proof

Theorem FoxDifferential.kernelAbelianizationToCoinvariantsLinear_eq_viaConnecting

omit [DecidableEq H] [DecidableEq G] in
theorem kernelAbelianizationToCoinvariantsLinear_eq_viaConnecting
    (ψ : G →* H) :
    kernelAbelianizationToCoinvariantsLinear (ψ := ψ) =
      kernelAbelianizationToCoinvariantsViaConnectingLinear (ψ := ψ)

The linear abelianization-to-coinvariants map agrees with the map obtained from the connecting morphism.

Show Lean proof

Theorem FoxDifferential.kernelAbelianizationToCoinvariantsLinear_injective

omit [DecidableEq H] [DecidableEq G] in
theorem kernelAbelianizationToCoinvariantsLinear_injective
    (hψ : Function.Surjective ψ) :
    Function.Injective (kernelAbelianizationToCoinvariantsLinear (ψ := ψ))

The abelianization-to-coinvariants map is injective.

Show Lean proof

Theorem FoxDifferential.kernelAugmentationIdealCoinvariants_smul_mk_ofSurjective

omit [DecidableEq H] [DecidableEq G] in
@[simp]
theorem kernelAugmentationIdealCoinvariants_smul_mk_ofSurjective
    (hψ : Function.Surjective ψ) (h : H) (x : augmentationIdeal G) :
    letI := kernelAugmentationIdealCoinvariantsModuleOfSurjective (ψ := ψ) hψ
    (MonoidAlgebra.of ℤ H h : GroupRing H) •
        Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ) x =
      Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
        (((groupAugmentationIdealRep (G := G)).ρ (Function.surjInv hψ h)) x)

The induced \(H\)-action on kernel augmentation coinvariants is computed on representatives.

Show Lean proof

Theorem FoxDifferential.kernelAugmentationIdealCoinvariants_mk_group_action_eq_of_eq

omit [DecidableEq H] [DecidableEq G] in
theorem kernelAugmentationIdealCoinvariants_mk_group_action_eq_of_eq
    {g₁ g₂ : G} (h : ψ g₁ = ψ g₂) (x : augmentationIdeal G) :
    Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
        (((groupAugmentationIdealRep (G := G)).ρ g₁) x) =
      Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
        (((groupAugmentationIdealRep (G := G)).ρ g₂) x)

The coinvariant representative in the augmentation-ideal kernel is compatible with the group action whenever the underlying representatives are equal.

Show Lean proof

Definition FoxDifferential.kernelAugmentationIdealCoinvariantsGeneratorOfSurjective

def kernelAugmentationIdealCoinvariantsGeneratorOfSurjective
    (g : G) :
    KernelAugmentationIdealCoinvariants (ψ := ψ) :=
  Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
    (augmentationGeneratorSubtype (H := G) g)

The canonical differential generator \(g \mapsto [g - 1]\) in \(H_0(\ker \psi, I(\mathbb{Z}[G]))\).

Definition FoxDifferential.kernelAugmentationIdealCoinvariantsGeneratorHomOfSurjective

def kernelAugmentationIdealCoinvariantsGeneratorHomOfSurjective
    (hψ : Function.Surjective ψ) :
    letI := kernelAugmentationIdealCoinvariantsModuleOfSurjective (ψ := ψ) hψ
    DifferentialHom ψ (KernelAugmentationIdealCoinvariants (ψ := ψ)) := by
  letI := kernelAugmentationIdealCoinvariantsModuleOfSurjective (ψ := ψ) hψ
  exact
    { toFun := kernelAugmentationIdealCoinvariantsGeneratorOfSurjective (ψ := ψ)
      map_mul' := by
        intro g₁ g₂
        simpa only [scalarCrossedAction_apply] using
          kernelAugmentationIdealCoinvariantsGeneratorOfSurjective_map_mul
            (ψ := ψ) hψ g₁ g₂ }

The canonical coinvariant generator is a crossed differential in the surjective case.

Definition FoxDifferential.differentialToKernelAugmentationIdealCoinvariantsLinearOfSurjective

def differentialToKernelAugmentationIdealCoinvariantsLinearOfSurjective
    (hψ : Function.Surjective ψ) :
    letI := kernelAugmentationIdealCoinvariantsModuleOfSurjective (ψ := ψ) hψ
    DifferentialModule ψ →ₗ[GroupRing H] KernelAugmentationIdealCoinvariants (ψ := ψ) := by
  letI := kernelAugmentationIdealCoinvariantsModuleOfSurjective (ψ := ψ) hψ
  exact
    differentialModuleLift ψ
      (kernelAugmentationIdealCoinvariantsGeneratorHomOfSurjective (ψ := ψ) hψ)

The canonical linear map \(A_{\psi}\to H_0(\ker \psi, I(\mathbb{Z}[G]))\) sending \(d(g)\) to \([g-1]\).

Theorem FoxDifferential.differentialToKernelAugmentationIdealCoinvariantsLinearOfSurjective_d

omit [DecidableEq H] [DecidableEq G] in
@[simp]
theorem differentialToKernelAugmentationIdealCoinvariantsLinearOfSurjective_d
    (hψ : Function.Surjective ψ) (g : G) :
    letI := kernelAugmentationIdealCoinvariantsModuleOfSurjective (ψ := ψ) hψ
    differentialToKernelAugmentationIdealCoinvariantsLinearOfSurjective
        (ψ := ψ) hψ (universalDifferential ψ g) =
      kernelAugmentationIdealCoinvariantsGeneratorOfSurjective (ψ := ψ) g

The surjective-case differential-to-coinvariants map sends each universal differential generator to the corresponding coinvariant class.

Show Lean proof

Theorem FoxDifferential.differentialToKernelAugmentationIdealCoinvariantsLinearOfSurjective_boundary

omit [DecidableEq H] [DecidableEq G] in
@[simp 900]
theorem differentialToKernelAugmentationIdealCoinvariantsLinearOfSurjective_boundary
    (hψ : Function.Surjective ψ) (x : KernelAbelianizationAdd ψ) :
    letI := kernelAbelianizationModuleOfSurjective ψ hψ
    letI := kernelAugmentationIdealCoinvariantsModuleOfSurjective (ψ := ψ) hψ
    differentialToKernelAugmentationIdealCoinvariantsLinearOfSurjective (ψ := ψ) hψ
        (kernelAbelianizationBoundaryLinearOfSurjective ψ hψ x) =
      kernelAbelianizationToCoinvariantsLinear (ψ := ψ) x

The surjective-case differential-to-coinvariants map is compatible with the boundary map.

Show Lean proof

ProCGroups.FoxDifferential.Discrete.KernelBoundary.Homology

Declarations