Module

Homology.lean

Nyll.ProCGroups.FoxDifferential.Discrete.KernelBoundary.Homology

58 declarations indexed from sourceView source ↗

Module documentation

Fox differential: discrete — kernel boundary — homology

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\).

Imports2

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

Imported by2

instance

instMulActionKernelCodomainTrivial

L42 ↗

FoxDifferential.instMulActionKernelCodomainTrivial

Documentation

The kernel-boundary codomain carries the trivial multiplication action.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct MonoidalCategory
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
section KernelGroupRing
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
variable (ψ : G →* H) (hψ : Function.Surjective ψ)

Lean source · full declaration

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

abbrev

kernelGroupRingRepIsoRightTensor

L101 ↗

FoxDifferential.kernelGroupRingRepIsoRightTensor

Documentation

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

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct MonoidalCategory
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
section KernelGroupRing
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
variable (ψ : G →* H) (hψ : Function.Surjective ψ)

Lean source · statement

def kernelGroupRingRepIsoRightTensor :
    kernelGroupRingRep (ψ := ψ) ≅ kernelRightTensorRep (H := H) (ψ := ψ)

def

indBottomKernelUnderlyingEquiv

L172 ↗

FoxDifferential.indBottomKernelUnderlyingEquiv

Documentation

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

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct MonoidalCategory
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
section KernelGroupRing
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
variable (ψ : G →* H) (hψ : Function.Surjective ψ)

Lean source · statement

def indBottomKernelUnderlyingEquiv :
    Representation.IndV (⊥ : Subgroup ↥(ψ.ker)).subtype
      (Rep.trivial ℤ (⊥ : Subgroup ↥(ψ.ker)) (H →₀ ℤ)).ρ
      ≃ₗ[ℤ] (GroupRing ↥(ψ.ker)) ⊗[ℤ] (H →₀ ℤ)

theorem

indBottomKernelUnderlyingEquiv_mk

L190 ↗

FoxDifferential.indBottomKernelUnderlyingEquiv_mk

Documentation

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\).

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct MonoidalCategory
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
section KernelGroupRing
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
variable (ψ : G →* H) (hψ : Function.Surjective ψ)
omit [DecidableEq H] [DecidableEq G] in

Lean source · statement

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

def

kernelGroupRingRep_apply_single

L279 ↗

FoxDifferential.kernelGroupRingRep_apply_single

Documentation

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

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct MonoidalCategory
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
section 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 kernelGroupRingRep_apply_single (n : ψ.ker) (g : G) (m : ℤ) :
    ((kernelGroupRingRep (ψ := ψ)).ρ n) (MonoidAlgebra.single g m) =
      MonoidAlgebra.single (n • g) m

theorem

augmentation_kernelGroupRingRep

L286 ↗

FoxDifferential.augmentation_kernelGroupRingRep

Documentation

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

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct MonoidalCategory
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
section 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 augmentation_kernelGroupRingRep
    (n : ψ.ker) (x : GroupRing G) :
    augmentation G (((kernelGroupRingRep (ψ := ψ)).ρ n) x) = augmentation G x

theorem

kernelAugmentationIdealInclusion

L380 ↗

FoxDifferential.kernelAugmentationIdealInclusion

Documentation

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

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct MonoidalCategory
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
section KernelAugmentation
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
variable (ψ : G →* H)

Lean source · statement

def kernelAugmentationIdealInclusion :
    kernelAugmentationIdealRep (ψ := ψ) ⟶ kernelGroupRingRep (ψ := ψ)

def

kernelAugmentationShortComplex

L409 ↗

FoxDifferential.kernelAugmentationShortComplex

Documentation

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.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct MonoidalCategory
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
section KernelAugmentation
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
variable (ψ : G →* H)

Lean source · statement

def kernelAugmentationShortComplex :
    CategoryTheory.ShortComplex (Rep ℤ ↥(ψ.ker))

theorem

kernelAugmentationShortComplex_exact

L423 ↗

FoxDifferential.kernelAugmentationShortComplex_exact

Documentation

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

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct MonoidalCategory
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
section 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 kernelAugmentationShortComplex_exact :
    (kernelAugmentationShortComplex (ψ := ψ)).Exact

theorem

kernelAugmentationShortExact

L443 ↗

FoxDifferential.kernelAugmentationShortExact

Documentation

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.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct MonoidalCategory
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
section 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 kernelAugmentationShortExact :
    (kernelAugmentationShortComplex (ψ := ψ)).ShortExact

abbrev

kernelTrivialIntRep

L463 ↗

FoxDifferential.kernelTrivialIntRep

Documentation

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

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct MonoidalCategory
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
section KernelAugmentation
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
variable (ψ : G →* H)

Lean source · statement

abbrev kernelTrivialIntRep : Rep ℤ ↥(ψ.ker)

def

kernelAugmentationConnecting

L471 ↗

FoxDifferential.kernelAugmentationConnecting

Documentation

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.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct MonoidalCategory
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
section KernelAugmentation
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
variable (ψ : G →* H)

Lean source · statement

def kernelAugmentationConnecting :
    groupHomology (kernelTrivialIntRep (ψ := ψ)) 1 ⟶
      groupHomology (kernelAugmentationIdealRep (ψ := ψ)) 0

def

kernelTrivialH1AddEquivAbelianization

L483 ↗

FoxDifferential.kernelTrivialH1AddEquivAbelianization

Documentation

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

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct MonoidalCategory
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
section KernelAugmentation
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
variable (ψ : G →* H)

Lean source · statement

def kernelTrivialH1AddEquivAbelianization :
    groupHomology (kernelTrivialIntRep (ψ := ψ)) 1 ≃+
      Additive (Abelianization ψ.ker)

theorem

kernelTrivialH1AddEquivAbelianization_symm_of

L495 ↗

FoxDifferential.kernelTrivialH1AddEquivAbelianization_symm_of

Documentation

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\).

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct MonoidalCategory
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
section 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 kernelTrivialH1AddEquivAbelianization_symm_of (n : ψ.ker) :
    (kernelTrivialH1AddEquivAbelianization (ψ := ψ)).symm
        (Additive.ofMul (Abelianization.of n)) =
      groupHomology.H1π (kernelTrivialIntRep (ψ := ψ))
        ((groupHomology.cycles₁IsoOfIsTrivial (kernelTrivialIntRep (ψ := ψ))).inv
          (Finsupp.single n 1))

theorem

kernelAugmentationConnecting_boundaryCycle_of

L512 ↗

FoxDifferential.kernelAugmentationConnecting_boundaryCycle_of

Documentation

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

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct MonoidalCategory
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
section 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 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

theorem

kernelAugmentationConnecting_boundaryElement_of

L539 ↗

FoxDifferential.kernelAugmentationConnecting_boundaryElement_of

Documentation

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

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct MonoidalCategory
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
section 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 kernelAugmentationConnecting_boundaryElement_of (n : ψ.ker) :
    (kernelAugmentationShortComplex (ψ := ψ)).f.hom
      (-(augmentationGeneratorSubtype (H := G) n.1)) =
    groupHomology.d₁₀ (kernelGroupRingRep (ψ := ψ))
      (Finsupp.single n (MonoidAlgebra.single n.1 (1 : ℤ)))

theorem

kernelAugmentationConnecting_H0Iso_of

L563 ↗

FoxDifferential.kernelAugmentationConnecting_H0Iso_of

Documentation

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

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct MonoidalCategory
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
section 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 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)

theorem

kernelAugmentationConnecting_injective

L621 ↗

FoxDifferential.kernelAugmentationConnecting_injective

Documentation

The kernel-augmentation connecting map is injective.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct MonoidalCategory
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
section 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 kernelAugmentationConnecting_injective
    (hψ : Function.Surjective ψ) :
    Function.Injective (kernelAugmentationConnecting (ψ := ψ)).hom

abbrev

KernelAugmentationIdealCoinvariants

L652 ↗

FoxDifferential.KernelAugmentationIdealCoinvariants

Documentation

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

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct MonoidalCategory
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
section KernelAugmentation
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
variable (ψ : G →* H)

Lean source · statement

abbrev KernelAugmentationIdealCoinvariants (ψ : G →* H) : Type _

instance

instKernelAugmentationIdealCoinvariantsIntModule

L655 ↗

FoxDifferential.instKernelAugmentationIdealCoinvariantsIntModule

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct MonoidalCategory
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
section KernelAugmentation
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
variable (ψ : G →* H)

Lean source · statement

instance instKernelAugmentationIdealCoinvariantsIntModule :
    Module ℤ (KernelAugmentationIdealCoinvariants (ψ := ψ))

theorem

kernelAugmentationIdealRep_rho_eq_groupAugmentationIdealRep_rho

L665 ↗

FoxDifferential.kernelAugmentationIdealRep_rho_eq_groupAugmentationIdealRep_rho

Documentation

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

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct MonoidalCategory
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
section KernelAugmentation
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
variable (ψ : G →* H)
local instance instKernelAugmentationIdealCoinvariantsIntModule :
    Module ℤ (KernelAugmentationIdealCoinvariants (ψ := ψ)) :=
  Representation.Coinvariants.instModule ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
omit [DecidableEq H] [DecidableEq G] in

Lean source · statement

theorem kernelAugmentationIdealRep_rho_eq_groupAugmentationIdealRep_rho
    (n : ψ.ker) :
    (kernelAugmentationIdealRep (ψ := ψ)).ρ n =
      (groupAugmentationIdealRep (G := G)).ρ n.1

def

kernelAugmentationIdealCoinvariantsEndOfSurjective

L675 ↗

FoxDifferential.kernelAugmentationIdealCoinvariantsEndOfSurjective

Documentation

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

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct MonoidalCategory
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
section KernelAugmentation
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
variable (ψ : G →* H)
local instance instKernelAugmentationIdealCoinvariantsIntModule :
    Module ℤ (KernelAugmentationIdealCoinvariants (ψ := ψ)) :=
  Representation.Coinvariants.instModule ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
section CoinvariantsAction

Lean source · statement

def kernelAugmentationIdealCoinvariantsEndOfSurjective
    (hψ : Function.Surjective ψ) (h : H) :
    KernelAugmentationIdealCoinvariants (ψ := ψ) →ₗ[ℤ]
      KernelAugmentationIdealCoinvariants (ψ := ψ)

theorem

kernelAugmentationIdealCoinvariantsEndOfSurjective_mk

L745 ↗

FoxDifferential.kernelAugmentationIdealCoinvariantsEndOfSurjective_mk

Documentation

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

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct MonoidalCategory
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
section KernelAugmentation
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
variable (ψ : G →* H)
local instance instKernelAugmentationIdealCoinvariantsIntModule :
    Module ℤ (KernelAugmentationIdealCoinvariants (ψ := ψ)) :=
  Representation.Coinvariants.instModule ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
section CoinvariantsAction
omit [DecidableEq H] [DecidableEq G] in

Lean source · statement

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)

def

kernelAugmentationIdealCoinvariantsModuleEndOfSurjective

L757 ↗

FoxDifferential.kernelAugmentationIdealCoinvariantsModuleEndOfSurjective

Documentation

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

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct MonoidalCategory
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
section KernelAugmentation
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
variable (ψ : G →* H)
local instance instKernelAugmentationIdealCoinvariantsIntModule :
    Module ℤ (KernelAugmentationIdealCoinvariants (ψ := ψ)) :=
  Representation.Coinvariants.instModule ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
section CoinvariantsAction

Lean source · full declaration

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]

def

kernelAugmentationIdealCoinvariantsActionRingHomOfSurjective

L842 ↗

FoxDifferential.kernelAugmentationIdealCoinvariantsActionRingHomOfSurjective

Documentation

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

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct MonoidalCategory
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
section KernelAugmentation
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
variable (ψ : G →* H)
local instance instKernelAugmentationIdealCoinvariantsIntModule :
    Module ℤ (KernelAugmentationIdealCoinvariants (ψ := ψ)) :=
  Representation.Coinvariants.instModule ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
section CoinvariantsAction

Lean source · statement

def kernelAugmentationIdealCoinvariantsActionRingHomOfSurjective
    (hψ : Function.Surjective ψ) :
    GroupRing H →+* Module.End ℤ (KernelAugmentationIdealCoinvariants (ψ := ψ))

theorem

kernelAugmentationIdealCoinvariantsActionRingHomOfSurjective_of

L863 ↗

FoxDifferential.kernelAugmentationIdealCoinvariantsActionRingHomOfSurjective_of

Documentation

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

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct MonoidalCategory
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
section KernelAugmentation
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
variable (ψ : G →* H)
local instance instKernelAugmentationIdealCoinvariantsIntModule :
    Module ℤ (KernelAugmentationIdealCoinvariants (ψ := ψ)) :=
  Representation.Coinvariants.instModule ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
section CoinvariantsAction
omit [DecidableEq H] [DecidableEq G] in

Lean source · statement

theorem kernelAugmentationIdealCoinvariantsActionRingHomOfSurjective_of
    (hψ : Function.Surjective ψ) (h : H) :
    kernelAugmentationIdealCoinvariantsActionRingHomOfSurjective (ψ := ψ) hψ
        (MonoidAlgebra.of ℤ H h) =
      kernelAugmentationIdealCoinvariantsModuleEndOfSurjective (ψ := ψ) hψ h

def

kernelAugmentationIdealCoinvariantsModuleOfSurjective

L883 ↗

FoxDifferential.kernelAugmentationIdealCoinvariantsModuleOfSurjective

Documentation

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

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct MonoidalCategory
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
section KernelAugmentation
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
variable (ψ : G →* H)
local instance instKernelAugmentationIdealCoinvariantsIntModule :
    Module ℤ (KernelAugmentationIdealCoinvariants (ψ := ψ)) :=
  Representation.Coinvariants.instModule ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
section CoinvariantsAction

Lean source · statement

def kernelAugmentationIdealCoinvariantsModuleOfSurjective
    (hψ : Function.Surjective ψ) :
    Module (GroupRing H) (KernelAugmentationIdealCoinvariants (ψ := ψ))

theorem

augmentationGeneratorSubtype_mul

L895 ↗

FoxDifferential.augmentationGeneratorSubtype_mul

Documentation

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

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct MonoidalCategory
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
section KernelAugmentation
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
variable (ψ : G →* H)
local instance instKernelAugmentationIdealCoinvariantsIntModule :
    Module ℤ (KernelAugmentationIdealCoinvariants (ψ := ψ)) :=
  Representation.Coinvariants.instModule ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
section CoinvariantsAction
omit [DecidableEq G] in

Lean source · statement

theorem augmentationGeneratorSubtype_mul (g₁ g₂ : G) :
    augmentationGeneratorSubtype (H := G) (g₁ * g₂) =
      augmentationGeneratorSubtype (H := G) g₁ +
        ((groupAugmentationIdealRep (G := G)).ρ g₁)
          (augmentationGeneratorSubtype (H := G) g₂)

def

kernelCoinvariantsBoundary

L917 ↗

FoxDifferential.kernelCoinvariantsBoundary

Documentation

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

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct MonoidalCategory
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
section KernelAugmentation
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
variable (ψ : G →* H)
local instance instKernelAugmentationIdealCoinvariantsIntModule :
    Module ℤ (KernelAugmentationIdealCoinvariants (ψ := ψ)) :=
  Representation.Coinvariants.instModule ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
section CoinvariantsAction

Lean source · full declaration

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)

def

kernelAbelianizationToCoinvariants

L956 ↗

FoxDifferential.kernelAbelianizationToCoinvariants

Documentation

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

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct MonoidalCategory
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
section KernelAugmentation
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
variable (ψ : G →* H)
local instance instKernelAugmentationIdealCoinvariantsIntModule :
    Module ℤ (KernelAugmentationIdealCoinvariants (ψ := ψ)) :=
  Representation.Coinvariants.instModule ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
section CoinvariantsAction

Lean source · statement

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

def

kernelAbelianizationToCoinvariantsAdd

L961 ↗

FoxDifferential.kernelAbelianizationToCoinvariantsAdd

Documentation

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

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct MonoidalCategory
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
section KernelAugmentation
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
variable (ψ : G →* H)
local instance instKernelAugmentationIdealCoinvariantsIntModule :
    Module ℤ (KernelAugmentationIdealCoinvariants (ψ := ψ)) :=
  Representation.Coinvariants.instModule ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
section CoinvariantsAction

Lean source · full declaration

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]

theorem

kernelAbelianizationToCoinvariantsAdd_of

L975 ↗

FoxDifferential.kernelAbelianizationToCoinvariantsAdd_of

Documentation

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

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct MonoidalCategory
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
section KernelAugmentation
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
variable (ψ : G →* H)
local instance instKernelAugmentationIdealCoinvariantsIntModule :
    Module ℤ (KernelAugmentationIdealCoinvariants (ψ := ψ)) :=
  Representation.Coinvariants.instModule ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
section CoinvariantsAction
omit [DecidableEq H] [DecidableEq G] in

Lean source · statement

theorem kernelAbelianizationToCoinvariantsAdd_of (n : ψ.ker) :
    kernelAbelianizationToCoinvariantsAdd (ψ := ψ)
        (Additive.ofMul (Abelianization.of n)) =
      Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
        (augmentationGeneratorSubtype (H := G) n.1)

def

kernelAbelianizationToCoinvariantsLinear

L989 ↗

FoxDifferential.kernelAbelianizationToCoinvariantsLinear

Documentation

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

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct MonoidalCategory
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
section KernelAugmentation
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
variable (ψ : G →* H)
local instance instKernelAugmentationIdealCoinvariantsIntModule :
    Module ℤ (KernelAugmentationIdealCoinvariants (ψ := ψ)) :=
  Representation.Coinvariants.instModule ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
section CoinvariantsAction

Lean source · statement

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

def

kernelAbelianizationToCoinvariantsViaConnectingAdd

L999 ↗

FoxDifferential.kernelAbelianizationToCoinvariantsViaConnectingAdd

Documentation

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.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct MonoidalCategory
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
section KernelAugmentation
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
variable (ψ : G →* H)
local instance instKernelAugmentationIdealCoinvariantsIntModule :
    Module ℤ (KernelAugmentationIdealCoinvariants (ψ := ψ)) :=
  Representation.Coinvariants.instModule ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
section CoinvariantsAction

Lean source · full declaration

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

def

kernelAbelianizationToCoinvariantsViaConnectingLinear

L1016 ↗

FoxDifferential.kernelAbelianizationToCoinvariantsViaConnectingLinear

Documentation

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

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct MonoidalCategory
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
section KernelAugmentation
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
variable (ψ : G →* H)
local instance instKernelAugmentationIdealCoinvariantsIntModule :
    Module ℤ (KernelAugmentationIdealCoinvariants (ψ := ψ)) :=
  Representation.Coinvariants.instModule ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
section CoinvariantsAction

Lean source · statement

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

theorem

kernelAbelianizationToCoinvariantsViaConnectingAdd_of

L1026 ↗

FoxDifferential.kernelAbelianizationToCoinvariantsViaConnectingAdd_of

Documentation

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

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct MonoidalCategory
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
section KernelAugmentation
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
variable (ψ : G →* H)
local instance instKernelAugmentationIdealCoinvariantsIntModule :
    Module ℤ (KernelAugmentationIdealCoinvariants (ψ := ψ)) :=
  Representation.Coinvariants.instModule ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
section CoinvariantsAction
omit [DecidableEq H] [DecidableEq G] in

Lean source · statement

theorem kernelAbelianizationToCoinvariantsViaConnectingAdd_of (n : ψ.ker) :
    kernelAbelianizationToCoinvariantsViaConnectingAdd (ψ := ψ)
        (Additive.ofMul (Abelianization.of n)) =
      Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
        (augmentationGeneratorSubtype (H := G) n.1)

theorem

kernelAbelianizationToCoinvariantsViaConnectingLinear_of

L1044 ↗

FoxDifferential.kernelAbelianizationToCoinvariantsViaConnectingLinear_of

Documentation

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

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct MonoidalCategory
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
section KernelAugmentation
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
variable (ψ : G →* H)
local instance instKernelAugmentationIdealCoinvariantsIntModule :
    Module ℤ (KernelAugmentationIdealCoinvariants (ψ := ψ)) :=
  Representation.Coinvariants.instModule ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
section CoinvariantsAction
omit [DecidableEq H] [DecidableEq G] in

Lean source · statement

theorem kernelAbelianizationToCoinvariantsViaConnectingLinear_of (n : ψ.ker) :
    kernelAbelianizationToCoinvariantsViaConnectingLinear (ψ := ψ)
        (Additive.ofMul (Abelianization.of n)) =
      Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
        (augmentationGeneratorSubtype (H := G) n.1)

theorem

kernelAbelianizationToCoinvariantsLinear_eq_viaConnecting

L1058 ↗

FoxDifferential.kernelAbelianizationToCoinvariantsLinear_eq_viaConnecting

Documentation

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

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct MonoidalCategory
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
section KernelAugmentation
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
variable (ψ : G →* H)
local instance instKernelAugmentationIdealCoinvariantsIntModule :
    Module ℤ (KernelAugmentationIdealCoinvariants (ψ := ψ)) :=
  Representation.Coinvariants.instModule ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
section CoinvariantsAction
omit [DecidableEq H] [DecidableEq G] in

Lean source · statement

theorem kernelAbelianizationToCoinvariantsLinear_eq_viaConnecting
    (ψ : G →* H) :
    kernelAbelianizationToCoinvariantsLinear (ψ := ψ) =
      kernelAbelianizationToCoinvariantsViaConnectingLinear (ψ := ψ)

theorem

kernelAbelianizationToCoinvariantsLinear_injective

L1085 ↗

FoxDifferential.kernelAbelianizationToCoinvariantsLinear_injective

Documentation

The abelianization-to-coinvariants map is injective.

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct MonoidalCategory
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
section KernelAugmentation
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
variable (ψ : G →* H)
local instance instKernelAugmentationIdealCoinvariantsIntModule :
    Module ℤ (KernelAugmentationIdealCoinvariants (ψ := ψ)) :=
  Representation.Coinvariants.instModule ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
section CoinvariantsAction
omit [DecidableEq H] [DecidableEq G] in

Lean source · statement

theorem kernelAbelianizationToCoinvariantsLinear_injective
    (hψ : Function.Surjective ψ) :
    Function.Injective (kernelAbelianizationToCoinvariantsLinear (ψ := ψ))

theorem

kernelAugmentationIdealCoinvariants_smul_mk_ofSurjective

L1119 ↗

FoxDifferential.kernelAugmentationIdealCoinvariants_smul_mk_ofSurjective

Documentation

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

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct MonoidalCategory
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
section KernelAugmentation
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
variable (ψ : G →* H)
local instance instKernelAugmentationIdealCoinvariantsIntModule :
    Module ℤ (KernelAugmentationIdealCoinvariants (ψ := ψ)) :=
  Representation.Coinvariants.instModule ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
section CoinvariantsAction
omit [DecidableEq H] [DecidableEq G] in

Lean source · full declaration

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) := by
  let := kernelAugmentationIdealCoinvariantsModuleOfSurjective (ψ := ψ) hψ
  rw [show (MonoidAlgebra.of ℤ H h : GroupRing H) •
      Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ) x =
    kernelAugmentationIdealCoinvariantsActionRingHomOfSurjective (ψ := ψ) hψ
        (MonoidAlgebra.of ℤ H h)
        (Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ) x) by
      rfl]
  rw [kernelAugmentationIdealCoinvariantsActionRingHomOfSurjective_of (ψ := ψ) hψ]
  simpa [kernelAugmentationIdealCoinvariantsModuleEndOfSurjective] using
    (kernelAugmentationIdealCoinvariantsEndOfSurjective_mk (ψ := ψ) hψ h x)

theorem

kernelAugmentationIdealCoinvariants_mk_group_action_eq_of_eq

L1142 ↗

FoxDifferential.kernelAugmentationIdealCoinvariants_mk_group_action_eq_of_eq

Documentation

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

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct MonoidalCategory
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
section KernelAugmentation
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
variable (ψ : G →* H)
local instance instKernelAugmentationIdealCoinvariantsIntModule :
    Module ℤ (KernelAugmentationIdealCoinvariants (ψ := ψ)) :=
  Representation.Coinvariants.instModule ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
section CoinvariantsAction
omit [DecidableEq H] [DecidableEq G] in

Lean source · statement

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)

def

kernelAugmentationIdealCoinvariantsGeneratorOfSurjective

L1180 ↗

FoxDifferential.kernelAugmentationIdealCoinvariantsGeneratorOfSurjective

Documentation

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

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct MonoidalCategory
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
section KernelAugmentation
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
variable (ψ : G →* H)
local instance instKernelAugmentationIdealCoinvariantsIntModule :
    Module ℤ (KernelAugmentationIdealCoinvariants (ψ := ψ)) :=
  Representation.Coinvariants.instModule ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
section CoinvariantsAction

Lean source · statement

def kernelAugmentationIdealCoinvariantsGeneratorOfSurjective
    (g : G) :
    KernelAugmentationIdealCoinvariants (ψ := ψ)

theorem

kernelAugmentationIdealCoinvariantsGeneratorOfSurjective_map_mul

L1187 ↗

FoxDifferential.kernelAugmentationIdealCoinvariantsGeneratorOfSurjective_map_mul

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct MonoidalCategory
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
section KernelAugmentation
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
variable (ψ : G →* H)
local instance instKernelAugmentationIdealCoinvariantsIntModule :
    Module ℤ (KernelAugmentationIdealCoinvariants (ψ := ψ)) :=
  Representation.Coinvariants.instModule ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
section CoinvariantsAction
omit [DecidableEq H] [DecidableEq G] in

Lean source · full declaration

theorem kernelAugmentationIdealCoinvariantsGeneratorOfSurjective_map_mul
    (hψ : Function.Surjective ψ) (g₁ g₂ : G) :
    letI := kernelAugmentationIdealCoinvariantsModuleOfSurjective (ψ := ψ) hψ
    kernelAugmentationIdealCoinvariantsGeneratorOfSurjective (ψ := ψ) (g₁ * g₂) =
      kernelAugmentationIdealCoinvariantsGeneratorOfSurjective (ψ := ψ) g₁ +
        groupRingScalar ψ g₁ •
          kernelAugmentationIdealCoinvariantsGeneratorOfSurjective (ψ := ψ) g₂ := by
  let := kernelAugmentationIdealCoinvariantsModuleOfSurjective (ψ := ψ) hψ
  rw [kernelAugmentationIdealCoinvariantsGeneratorOfSurjective,
    augmentationGeneratorSubtype_mul]
  rw [map_add]
  congr 1
  calc
    Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
        (((groupAugmentationIdealRep (G := G)).ρ g₁)
          (augmentationGeneratorSubtype (H := G) g₂))
      = Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
          (((groupAugmentationIdealRep (G := G)).ρ
              (Function.surjInv hψ (ψ g₁)))
            (augmentationGeneratorSubtype (H := G) g₂)) := by
              apply kernelAugmentationIdealCoinvariants_mk_group_action_eq_of_eq (ψ := ψ)
              simpa using (Function.surjInv_eq hψ (ψ g₁)).symm
    _ = (MonoidAlgebra.of ℤ H (ψ g₁) : GroupRing H) •
          kernelAugmentationIdealCoinvariantsGeneratorOfSurjective (ψ := ψ) g₂ := by
            symm
            exact kernelAugmentationIdealCoinvariants_smul_mk_ofSurjective
              (ψ := ψ) hψ (ψ g₁) (augmentationGeneratorSubtype (H := G) g₂)

def

kernelAugmentationIdealCoinvariantsGeneratorHomOfSurjective

L1216 ↗

FoxDifferential.kernelAugmentationIdealCoinvariantsGeneratorHomOfSurjective

Documentation

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

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct MonoidalCategory
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
section KernelAugmentation
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
variable (ψ : G →* H)
local instance instKernelAugmentationIdealCoinvariantsIntModule :
    Module ℤ (KernelAugmentationIdealCoinvariants (ψ := ψ)) :=
  Representation.Coinvariants.instModule ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
section CoinvariantsAction

Lean source · full declaration

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₂ }

def

differentialToKernelAugmentationIdealCoinvariantsLinearOfSurjective

L1233 ↗

FoxDifferential.differentialToKernelAugmentationIdealCoinvariantsLinearOfSurjective

Documentation

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

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct MonoidalCategory
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
section KernelAugmentation
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
variable (ψ : G →* H)
local instance instKernelAugmentationIdealCoinvariantsIntModule :
    Module ℤ (KernelAugmentationIdealCoinvariants (ψ := ψ)) :=
  Representation.Coinvariants.instModule ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
section CoinvariantsAction

Lean source · full declaration

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

theorem

differentialToKernelAugmentationIdealCoinvariantsLinearOfSurjective_d

L1248 ↗

FoxDifferential.differentialToKernelAugmentationIdealCoinvariantsLinearOfSurjective_d

Documentation

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

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct MonoidalCategory
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
section KernelAugmentation
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
variable (ψ : G →* H)
local instance instKernelAugmentationIdealCoinvariantsIntModule :
    Module ℤ (KernelAugmentationIdealCoinvariants (ψ := ψ)) :=
  Representation.Coinvariants.instModule ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
section CoinvariantsAction
omit [DecidableEq H] [DecidableEq G] in

Lean source · full declaration

theorem differentialToKernelAugmentationIdealCoinvariantsLinearOfSurjective_d
    (hψ : Function.Surjective ψ) (g : G) :
    letI := kernelAugmentationIdealCoinvariantsModuleOfSurjective (ψ := ψ) hψ
    differentialToKernelAugmentationIdealCoinvariantsLinearOfSurjective
        (ψ := ψ) hψ (universalDifferential ψ g) =
      kernelAugmentationIdealCoinvariantsGeneratorOfSurjective (ψ := ψ) g := by
  let := kernelAugmentationIdealCoinvariantsModuleOfSurjective (ψ := ψ) hψ
  change
    differentialModuleLift ψ
        (kernelAugmentationIdealCoinvariantsGeneratorHomOfSurjective (ψ := ψ) hψ)
        (universalDifferential ψ g) =
      kernelAugmentationIdealCoinvariantsGeneratorOfSurjective (ψ := ψ) g
  exact
    differentialModuleLift_d
      (A := KernelAugmentationIdealCoinvariants (ψ := ψ))
      ψ
      (kernelAugmentationIdealCoinvariantsGeneratorHomOfSurjective (ψ := ψ) hψ)
      g

theorem

differentialToKernelAugmentationIdealCoinvariantsLinearOfSurjective_boundary

L1270 ↗

FoxDifferential.differentialToKernelAugmentationIdealCoinvariantsLinearOfSurjective_boundary

Documentation

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

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct MonoidalCategory
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
section KernelAugmentation
variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
variable (ψ : G →* H)
local instance instKernelAugmentationIdealCoinvariantsIntModule :
    Module ℤ (KernelAugmentationIdealCoinvariants (ψ := ψ)) :=
  Representation.Coinvariants.instModule ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
section CoinvariantsAction
omit [DecidableEq H] [DecidableEq G] in

Lean source · full declaration

theorem differentialToKernelAugmentationIdealCoinvariantsLinearOfSurjective_boundary
    (hψ : Function.Surjective ψ) (x : KernelAbelianizationAdd ψ) :
    letI := kernelAbelianizationModuleOfSurjective ψ hψ
    letI := kernelAugmentationIdealCoinvariantsModuleOfSurjective (ψ := ψ) hψ
    differentialToKernelAugmentationIdealCoinvariantsLinearOfSurjective (ψ := ψ) hψ
        (kernelAbelianizationBoundaryLinearOfSurjective ψ hψ x) =
      kernelAbelianizationToCoinvariantsLinear (ψ := ψ) x := by
  let := kernelAbelianizationModuleOfSurjective ψ hψ
  let := kernelAugmentationIdealCoinvariantsModuleOfSurjective (ψ := ψ) hψ
  change
    (fun y : Abelianization ψ.ker =>
      differentialToKernelAugmentationIdealCoinvariantsLinearOfSurjective (ψ := ψ) hψ
          (kernelAbelianizationBoundaryAdd ψ (Additive.ofMul y)) =
        kernelAbelianizationToCoinvariantsAdd (ψ := ψ) (Additive.ofMul y))
      (Additive.toMul x)
  refine QuotientGroup.induction_on (Additive.toMul x) ?_
  intro n
  calc
    differentialToKernelAugmentationIdealCoinvariantsLinearOfSurjective (ψ := ψ) hψ
        ((kernelAbelianizationBoundaryAdd ψ) (Additive.ofMul (Abelianization.of n))) =
      differentialToKernelAugmentationIdealCoinvariantsLinearOfSurjective (ψ := ψ) hψ
        (universalDifferential ψ n.1) := by
          exact congrArg
            (differentialToKernelAugmentationIdealCoinvariantsLinearOfSurjective
              (ψ := ψ) hψ)
            (kernelAbelianizationBoundaryAdd_of (ψ := ψ) n)
    _ = kernelAugmentationIdealCoinvariantsGeneratorOfSurjective (ψ := ψ) n.1 := by
          exact differentialToKernelAugmentationIdealCoinvariantsLinearOfSurjective_d
            (ψ := ψ) hψ n.1
    _ = kernelAbelianizationToCoinvariantsAdd (ψ := ψ) (Additive.ofMul (Abelianization.of n)) := by
          symm
          simp only [kernelAbelianizationToCoinvariantsAdd_of,
  kernelAugmentationIdealCoinvariantsGeneratorOfSurjective]

Module documentation

Fox differential: discrete — kernel boundary — homology

Declarations