ProCGroups.FoxDifferential.Discrete.KernelBoundary.IdentityAugmentation

31 Theorems | 10 Definitions | 2 Abbreviations

The principal declarations in this module are:

coinvariantsLEquivOfSubsingleton For a representation of a subsingleton monoid, taking coinvariants does not change the underlying module. - rightRegularRepresentation The right-regular \(\mathbb{Z}\)-linear representation on \(\mathbb{Z}[H]\), given by right multiplication by \(g^{-1}\). This is the representation whose low-degree group homology matches the identity-case Crowell relations. - rightRegularRepresentation_apply_single The right-regular representation sends a single group element to the corresponding basis action. - rightRegularRepresentation_apply_of The right-regular representation has the displayed value on a representative.

imports

ProCGroups.FoxDifferential.Discrete.GroupRing
Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Mathlib.RepresentationTheory.Homological.GroupHomology.Shapiro

Imported by

Definition FoxDifferential.coinvariantsLEquivOfSubsingleton

def coinvariantsLEquivOfSubsingleton
    {k G V : Type*} [CommRing k] [Monoid G] [Subsingleton G]
    [AddCommGroup V] [Module k V] (ρ : Representation k G V) :
    Representation.Coinvariants ρ ≃ₗ[k] V := by
  refine LinearEquiv.ofLinear
    (Representation.Coinvariants.lift ρ LinearMap.id ?_)
    (Representation.Coinvariants.mk ρ)
    ?_ ?_
  · intro g
    ext x
    have : g = (1 : G) := Subsingleton.elim _ _
    subst this
    simp only [map_one, LinearMap.id_comp, Module.End.one_apply, LinearMap.id_coe, id_eq]
  · ext x
    simp only [Coinvariants.lift_comp_mk, LinearMap.id_coe, id_eq]
  · apply Representation.Coinvariants.hom_ext
    ext x
    simp only [LinearMap.coe_comp, Function.comp_apply, Coinvariants.lift_mk, LinearMap.id_coe,
        id_eq,
  LinearMap.id_comp]

For a representation of a subsingleton monoid, taking coinvariants does not change the underlying module.

Definition FoxDifferential.rightRegularRepresentation

def rightRegularRepresentation : Representation ℤ H (GroupRing H) where
  toFun g :=
    { toFun := fun x => x * MonoidAlgebra.of ℤ H g⁻¹
      map_add' := by
        intro x y
        simp only [MonoidAlgebra.of_apply, add_mul]
      map_smul' := by
        intro n x
        simpa using smul_mul_assoc n x (MonoidAlgebra.of ℤ H g⁻¹) }
  map_one' := by
    ext x
    simp only [inv_one, MonoidAlgebra.of_apply, LinearMap.coe_comp, LinearMap.coe_mk, AddHom.coe_mk,
  Function.comp_apply, MonoidAlgebra.lsingle_apply, MonoidAlgebra.single_mul_single, mul_one,
      Module.End.one_apply]
  map_mul' g₁ g₂ := by
    ext x
    simp only [mul_inv_rev, MonoidAlgebra.of_apply, LinearMap.coe_comp, LinearMap.coe_mk,
        AddHom.coe_mk,
  Function.comp_apply, MonoidAlgebra.lsingle_apply, MonoidAlgebra.single_mul_single, mul_one,
      Module.End.mul_apply,
  mul_assoc]

The right-regular \(\mathbb{Z}\)-linear representation on \(\mathbb{Z}[H]\), given by right multiplication by \(g^{-1}\). This is the representation whose low-degree group homology matches the identity-case Crowell relations.

Theorem FoxDifferential.rightRegularRepresentation_apply_single

omit [DecidableEq H] in
@[simp]
theorem rightRegularRepresentation_apply_single (g h : H) (n : ℤ) :
    rightRegularRepresentation H g (MonoidAlgebra.single h n) =
      MonoidAlgebra.single (h * g⁻¹) n

The right-regular representation sends a single group element to the corresponding basis action.

Show Lean proof

Theorem FoxDifferential.rightRegularRepresentation_apply_of

omit [DecidableEq H] in
@[simp]
theorem rightRegularRepresentation_apply_of (g h : H) :
    rightRegularRepresentation H g (MonoidAlgebra.of ℤ H h : GroupRing H) =
      MonoidAlgebra.of ℤ H (h * g⁻¹)

The right-regular representation has the displayed value on a representative.

Show Lean proof

Abbreviation FoxDifferential.rightRegularRep

abbrev rightRegularRep : Rep ℤ H := Rep.of (rightRegularRepresentation H)

The right-regular representation as an object of Rep \(\mathbb{Z}\) H.

Theorem FoxDifferential.rightRegular_d₂₁_single

omit [DecidableEq H] in
theorem rightRegular_d₂₁_single (g₁ g₂ : H) (r : GroupRing H) :
    groupHomology.d₂₁ (rightRegularRep H) (Finsupp.single (g₁, g₂) r) =
      (-r) • relationElement (MonoidHom.id H) g₁ g₂

The Crowell identity relations are precisely the \(d_{21}\)-images of the right-regular representation, on basis elements.

Show Lean proof

Theorem FoxDifferential.relationElement_eq_rightRegular_d₂₁_single

omit [DecidableEq H] in
theorem relationElement_eq_rightRegular_d₂₁_single (g₁ g₂ : H) (r : GroupRing H) :
    r • relationElement (MonoidHom.id H) g₁ g₂ =
      groupHomology.d₂₁ (rightRegularRep H) (Finsupp.single (g₁, g₂) (-r))

Rewriting the right-regular boundary identity in the Crowell direction.

Show Lean proof

Theorem FoxDifferential.rightRegular_d₂₁_mem_relationSubmodule

omit [DecidableEq H] in
theorem rightRegular_d₂₁_mem_relationSubmodule (x : H × H →₀ GroupRing H) :
    groupHomology.d₂₁ (rightRegularRep H) x ∈ relationSubmodule (MonoidHom.id H)

Every right-regular 1-boundary is a Crowell relation in the identity differential module.

Show Lean proof

Theorem FoxDifferential.rightRegular_d₂₁_smul_single

omit [DecidableEq H] in
@[simp]
theorem rightRegular_d₂₁_smul_single (r : GroupRing H) (g : H × H) (a : GroupRing H) :
    groupHomology.d₂₁ (rightRegularRep H) (r • Finsupp.single g a) =
      r • groupHomology.d₂₁ (rightRegularRep H) (Finsupp.single g a)

The scalar-multiplication formula for \(d_{21}\) holds on singleton generators.

Show Lean proof

Theorem FoxDifferential.rightRegular_d₂₁_smul

omit [DecidableEq H] in
theorem rightRegular_d₂₁_smul (r : GroupRing H) (x : H × H →₀ GroupRing H) :
    groupHomology.d₂₁ (rightRegularRep H) (r • x) =
      r • groupHomology.d₂₁ (rightRegularRep H) x

The right-regular \(d_{21}\) map is compatible with scalar multiplication.

Show Lean proof

Definition FoxDifferential.rightRegularBoundariesSubmodule

def rightRegularBoundariesSubmodule : Submodule (GroupRing H) (DifferentialPreModule H H) where
  carrier := groupHomology.boundaries₁ (rightRegularRep H)
  zero_mem' := by
    exact ⟨0, by simp only [map_zero]⟩
  add_mem' := by
    intro x y hx hy
    exact (groupHomology.boundaries₁ (rightRegularRep H)).add_mem hx hy
  smul_mem' := by
    intro r x hx
    rcases hx with ⟨y, rfl⟩
    exact ⟨r • y, rightRegular_d₂₁_smul (H := H) r y⟩

The degree-1 boundaries for the right-regular representation, regarded as a \(\mathbb{Z}[H]\)-submodule of the free pre-module.

Theorem FoxDifferential.mem_rightRegularBoundariesSubmodule

omit [DecidableEq H] in
@[simp]
theorem mem_rightRegularBoundariesSubmodule {x : DifferentialPreModule H H} :
    x ∈ rightRegularBoundariesSubmodule H ↔ x ∈ groupHomology.boundaries₁ (rightRegularRep H)

The displayed right-regular boundary lies in the right-regular boundary submodule.

Show Lean proof

Theorem FoxDifferential.relationElement_mem_rightRegularBoundariesSubmodule

omit [DecidableEq H] in
theorem relationElement_mem_rightRegularBoundariesSubmodule (g₁ g₂ : H) :
    relationElement (MonoidHom.id H) g₁ g₂ ∈ rightRegularBoundariesSubmodule H

Each identity-Crowell relation already lies in the right-regular boundary submodule.

Show Lean proof

Theorem FoxDifferential.relationSubmodule_le_rightRegularBoundariesSubmodule

omit [DecidableEq H] in
theorem relationSubmodule_le_rightRegularBoundariesSubmodule :
    relationSubmodule (MonoidHom.id H) ≤ rightRegularBoundariesSubmodule H

The identity Crowell relation submodule is contained in the right-regular boundary submodule.

Show Lean proof

Theorem FoxDifferential.rightRegular_boundaries₁_le_relationSubmodule

omit [DecidableEq H] in
theorem rightRegular_boundaries₁_le_relationSubmodule :
    groupHomology.boundaries₁ (rightRegularRep H) ≤
      (relationSubmodule (MonoidHom.id H)).restrictScalars ℤ

The degree-1 boundaries for the right-regular representation lie in the Crowell relation submodule.

Show Lean proof

Theorem FoxDifferential.rightRegularBoundariesSubmodule_le_relationSubmodule

omit [DecidableEq H] in
theorem rightRegularBoundariesSubmodule_le_relationSubmodule :
    rightRegularBoundariesSubmodule H ≤ relationSubmodule (MonoidHom.id H)

The right-regular boundary submodule is contained in the relation submodule.

Show Lean proof

Theorem FoxDifferential.relationSubmodule_eq_rightRegularBoundariesSubmodule

omit [DecidableEq H] in
theorem relationSubmodule_eq_rightRegularBoundariesSubmodule :
    relationSubmodule (MonoidHom.id H) = rightRegularBoundariesSubmodule H

The identity Crowell relations are exactly the right-regular degree-1 boundaries.

Show Lean proof

Theorem FoxDifferential.liftLinear_groupRingBoundary_id_single

omit [DecidableEq H] in
@[simp]
theorem liftLinear_groupRingBoundary_id_single (g : H) (r : GroupRing H) :
    liftLinear (H := H) (G := H) (A := GroupRing H)
        (groupRingBoundary (MonoidHom.id H)) (Finsupp.single g r) =
      r * augmentationGenerator H g

The lifted linear identity-boundary map has the stated value on a single group-ring generator.

Show Lean proof

Theorem FoxDifferential.liftLinear_groupRingBoundary_id_mem_augmentationIdeal

omit [DecidableEq H] in
theorem liftLinear_groupRingBoundary_id_mem_augmentationIdeal (x : DifferentialPreModule H H) :
    liftLinear (H := H) (G := H) (A := GroupRing H)
        (groupRingBoundary (MonoidHom.id H)) x ∈ augmentationIdeal H

The pre-boundary map for the identity case lands in the augmentation ideal.

Show Lean proof

Theorem FoxDifferential.augmentationGenerator_mem_range_liftLinear_groupRingBoundary_id

omit [DecidableEq H] in
theorem augmentationGenerator_mem_range_liftLinear_groupRingBoundary_id (h : H) :
    augmentationGenerator H h ∈
      LinearMap.range (liftLinear (H := H) (G := H) (A := GroupRing H)
        (groupRingBoundary (MonoidHom.id H)))

The standard generator \(h-1\) of the augmentation ideal lies in the image of the identity pre-boundary map.

Show Lean proof

Theorem FoxDifferential.augmentationIdeal_le_range_liftLinear_groupRingBoundary_id

omit [DecidableEq H] in
theorem augmentationIdeal_le_range_liftLinear_groupRingBoundary_id :
    (augmentationIdeal H : Submodule (GroupRing H) (GroupRing H)) ≤
      LinearMap.range (liftLinear (H := H) (G := H) (A := GroupRing H)
        (groupRingBoundary (MonoidHom.id H)))

The augmentation ideal is generated by the image of the identity pre-boundary map.

Show Lean proof

Theorem FoxDifferential.liftLinear_groupRingBoundary_id_eq_d₁₀

omit [DecidableEq H] in
theorem liftLinear_groupRingBoundary_id_eq_d₁₀ :
    (liftLinear (H := H) (G := H) (A := GroupRing H)
        (groupRingBoundary (MonoidHom.id H))).restrictScalars ℤ =
      (groupHomology.d₁₀ (rightRegularRep H)).hom

For the identity homomorphism, the lifted group-ring boundary equals the degree-one differential for the right-regular representation.

Show Lean proof

Theorem FoxDifferential.liftLinear_groupRingBoundary_id_apply

omit [DecidableEq H] in
theorem liftLinear_groupRingBoundary_id_apply (x : DifferentialPreModule H H) :
    liftLinear (H := H) (G := H) (A := GroupRing H)
        (groupRingBoundary (MonoidHom.id H)) x =
      groupHomology.d₁₀ (rightRegularRep H) x

The identity group-ring boundary lift is evaluated on canonical generators and then extended linearly.

Show Lean proof

Theorem FoxDifferential.rightRegular_d₁₀_mem_augmentationIdeal

omit [DecidableEq H] in
theorem rightRegular_d₁₀_mem_augmentationIdeal (x : DifferentialPreModule H H) :
    groupHomology.d₁₀ (rightRegularRep H) x ∈ augmentationIdeal H

The right-regular degree-0 differential lands in the augmentation ideal.

Show Lean proof

Theorem FoxDifferential.rightRegular_d₁₀_range_eq_augmentationIdeal

omit [DecidableEq H] in
theorem rightRegular_d₁₀_range_eq_augmentationIdeal :
    LinearMap.range (groupHomology.d₁₀ (rightRegularRep H)).hom =
      (augmentationIdeal H).restrictScalars ℤ

The canonical augmentation ideal is the kernel of the ordinary group-ring augmentation map.

Show Lean proof

Abbreviation FoxDifferential.bottomTrivialRep

abbrev bottomTrivialRep : Rep ℤ (⊥ : Subgroup H) :=
  Rep.trivial ℤ (⊥ : Subgroup H) ℤ

The trivial representation of the trivial subgroup of \(H\). Shapiro identifies its induced representation with the right-regular representation.

Definition FoxDifferential.indBottomTrivialUnderlyingEquiv

def indBottomTrivialUnderlyingEquiv :
    Representation.IndV (⊥ : Subgroup H).subtype (bottomTrivialRep H).ρ ≃ₗ[ℤ] GroupRing H := by
  let ρt : Representation ℤ (⊥ : Subgroup H) (TensorProduct ℤ (GroupRing H) ℤ) :=
    Representation.tprod
      (((Rep.leftRegular ℤ H).ρ.comp (⊥ : Subgroup H).subtype))
      (bottomTrivialRep H).ρ
  let e1 : Representation.Coinvariants ρt ≃ₗ[ℤ] TensorProduct ℤ (GroupRing H) ℤ :=
    coinvariantsLEquivOfSubsingleton ρt
  exact e1.trans (TensorProduct.rid ℤ (GroupRing H))

The induced module from the trivial subgroup is just the group ring.

Theorem FoxDifferential.indBottomTrivialUnderlyingEquiv_mk

omit [DecidableEq H] in
@[simp 900]
theorem indBottomTrivialUnderlyingEquiv_mk (h : H) (n : ℤ) :
    indBottomTrivialUnderlyingEquiv H
      (Representation.IndV.mk (⊥ : Subgroup H).subtype (bottomTrivialRep H).ρ h n) =
        MonoidAlgebra.single h n

The bottom-trivial induced-module equivalence sends the induced representative with element \(h\) and coefficient \(n\) to the singleton group-ring element at \(h\) with coefficient \(n\).

Show Lean proof

Definition FoxDifferential.indBottomTrivialIsoRightRegular

def indBottomTrivialIsoRightRegular :
    Rep.ind (⊥ : Subgroup H).subtype (bottomTrivialRep H) ≅ rightRegularRep H := by
  refine Rep.mkIso
    (Representation.Equiv.mk (indBottomTrivialUnderlyingEquiv H) ?_)
  intro g
  apply Representation.IndV.hom_ext
  intro h
  apply LinearMap.ext
  intro n
  change (indBottomTrivialUnderlyingEquiv H)
      (((Rep.ind (⊥ : Subgroup H).subtype (bottomTrivialRep H)).ρ g)
        ((Representation.IndV.mk (⊥ : Subgroup H).subtype (bottomTrivialRep H).ρ h) n)) =
    (rightRegularRepresentation H g
      (indBottomTrivialUnderlyingEquiv H
        ((Representation.IndV.mk (⊥ : Subgroup H).subtype (bottomTrivialRep H).ρ h) n)))
  have hind :
      (((Rep.ind (⊥ : Subgroup H).subtype (bottomTrivialRep H)).ρ g)
        ((Representation.IndV.mk (⊥ : Subgroup H).subtype (bottomTrivialRep H).ρ h) n)) =
      (Representation.IndV.mk (⊥ : Subgroup H).subtype (bottomTrivialRep H).ρ (h * g⁻¹))
        n := by
    exact Representation.ind_mk
      (φ := (⊥ : Subgroup H).subtype) (ρ := (bottomTrivialRep H).ρ) g h n
  rw [hind, indBottomTrivialUnderlyingEquiv_mk, indBottomTrivialUnderlyingEquiv_mk]
  simp only [rightRegularRepresentation_apply_single]

Shapiro's lemma identifies the induced trivial representation of the trivial subgroup with the right-regular representation.

Definition FoxDifferential.groupHomologyIsoOfRepIso

def groupHomologyIsoOfRepIso {A B : Rep ℤ H} (e : A ≅ B) (n : ℕ) :
    groupHomology A n ≅ groupHomology B n where
  hom := groupHomology.map (MonoidHom.id H) e.hom n
  inv := groupHomology.map (MonoidHom.id H) e.inv n
  hom_inv_id := by
    have h := groupHomology.map_id_comp (φ := e.hom) (ψ := e.inv) (n := n)
    rw [e.hom_inv_id, groupHomology.map_id] at h
    simpa using h.symm
  inv_hom_id := by
    have h := groupHomology.map_id_comp (φ := e.inv) (ψ := e.hom) (n := n)
    rw [e.inv_hom_id, groupHomology.map_id] at h
    simpa using h.symm

Group homology respects isomorphic representations.

Definition FoxDifferential.rightRegularH1IsoBottom

def rightRegularH1IsoBottom :
    groupHomology (rightRegularRep H) 1 ≅ groupHomology (bottomTrivialRep H) 1 := by
  exact (groupHomologyIsoOfRepIso H (indBottomTrivialIsoRightRegular H).symm 1) ≪≫
    groupHomology.indIso (⊥ : Subgroup H) (bottomTrivialRep H) 1

The first homology of the right-regular representation is identified with the first homology of the trivial subgroup.

Theorem FoxDifferential.rightRegular_H1_isZero

omit [DecidableEq H] in
theorem rightRegular_H1_isZero : Limits.IsZero (groupHomology (rightRegularRep H) 1)

The first homology of the right-regular representation vanishes.

Show Lean proof

Theorem FoxDifferential.rightRegular_cycles₁_eq_boundaries₁

omit [DecidableEq H] in
theorem rightRegular_cycles₁_eq_boundaries₁ :
    groupHomology.cycles₁ (rightRegularRep H) = groupHomology.boundaries₁ (rightRegularRep H)

In degree 1, right-regular cycles are exactly right-regular boundaries.

Show Lean proof

Theorem FoxDifferential.mem_rightRegularBoundariesSubmodule_iff_d₁₀_eq_zero

theorem mem_rightRegularBoundariesSubmodule_iff_d₁₀_eq_zero
    {H : Type} [Group H] {x : DifferentialPreModule H H} :
    x ∈ rightRegularBoundariesSubmodule H ↔ groupHomology.d₁₀ (rightRegularRep H) x = 0

For the right-regular representation, a 1-chain is a boundary exactly when its degree-0 differential vanishes.

Show Lean proof

Definition FoxDifferential.rightRegularBoundariesQuotientEquivIdentityDifferentialModule

def rightRegularBoundariesQuotientEquivIdentityDifferentialModule :
    (DifferentialPreModule H H ⧸ (rightRegularBoundariesSubmodule H)) ≃ₗ[GroupRing H]
      DifferentialModule (MonoidHom.id H) :=
  Submodule.quotEquivOfEq (rightRegularBoundariesSubmodule H)
    (relationSubmodule (MonoidHom.id H))
    (relationSubmodule_eq_rightRegularBoundariesSubmodule (H := H)).symm

The quotient of the free pre-module by right-regular degree-1 boundaries is the identity Crowell differential module.

Theorem FoxDifferential.rightRegularBoundariesQuotientEquivIdentityDifferentialModule_mk

omit [DecidableEq H] in
@[simp]
theorem rightRegularBoundariesQuotientEquivIdentityDifferentialModule_mk
    (x : DifferentialPreModule H H) :
    rightRegularBoundariesQuotientEquivIdentityDifferentialModule H
      (Submodule.Quotient.mk x) =
        (relationSubmodule (MonoidHom.id H)).mkQ x

The equivalence from the quotient by right-regular boundaries to the identity differential module sends a quotient class to the corresponding relation-submodule quotient class.

Show Lean proof

Definition FoxDifferential.rightRegularBoundariesQuotientToAugmentationIdeal

def rightRegularBoundariesQuotientToAugmentationIdeal :
    (DifferentialPreModule H H ⧸ (rightRegularBoundariesSubmodule H)) →ₗ[GroupRing H]
      augmentationIdeal H :=
  { toFun := fun x =>
      toAugmentationIdeal (H := H) (MonoidHom.id H)
        (rightRegularBoundariesQuotientEquivIdentityDifferentialModule H x)
    map_add' := by
      intro x y
      simp only [map_add]
    map_smul' := by
      intro r x
      simp only [map_smul, RingHom.id_apply]}

The quotient by right-regular boundaries maps onto the augmentation ideal.

Theorem FoxDifferential.rightRegularBoundariesQuotientToAugmentationIdeal_mk_single

omit [DecidableEq H] in
@[simp]
theorem rightRegularBoundariesQuotientToAugmentationIdeal_mk_single (h : H) :
    rightRegularBoundariesQuotientToAugmentationIdeal H
      (Submodule.Quotient.mk (Finsupp.single h 1)) =
        augmentationGeneratorSubtype (H := H) h

The quotient map from right-regular boundaries to the augmentation ideal sends a single generator to the corresponding augmentation generator.

Show Lean proof

Theorem FoxDifferential.rightRegularBoundariesQuotientToAugmentationIdeal_surjective

omit [DecidableEq H] in
theorem rightRegularBoundariesQuotientToAugmentationIdeal_surjective :
    Function.Surjective (rightRegularBoundariesQuotientToAugmentationIdeal H)

The quotient by right-regular boundaries surjects onto the augmentation ideal.

Show Lean proof

Theorem FoxDifferential.rightRegularBoundariesQuotientToAugmentationIdeal_eq_zero_iff

theorem rightRegularBoundariesQuotientToAugmentationIdeal_eq_zero_iff
    {H : Type} [Group H]
    {q : DifferentialPreModule H H ⧸ (rightRegularBoundariesSubmodule H)} :
    rightRegularBoundariesQuotientToAugmentationIdeal H q = 0 ↔ q = 0

The quotient-to-augmentation map has trivial kernel.

Show Lean proof

Theorem FoxDifferential.rightRegularBoundariesQuotientToAugmentationIdeal_injective

omit [DecidableEq H] in
theorem rightRegularBoundariesQuotientToAugmentationIdeal_injective :
    Function.Injective (rightRegularBoundariesQuotientToAugmentationIdeal H)

The map from the quotient of right-regular boundaries to the ordinary augmentation ideal is injective.

Show Lean proof

Definition FoxDifferential.rightRegularBoundariesQuotientEquivAugmentationIdeal

def rightRegularBoundariesQuotientEquivAugmentationIdeal :
    (DifferentialPreModule H H ⧸ (rightRegularBoundariesSubmodule H)) ≃ₗ[GroupRing H]
      augmentationIdeal H :=
  LinearEquiv.ofBijective (rightRegularBoundariesQuotientToAugmentationIdeal H)
    ⟨rightRegularBoundariesQuotientToAugmentationIdeal_injective (H := H),
      rightRegularBoundariesQuotientToAugmentationIdeal_surjective (H := H)⟩

The right-regular boundary quotient is exactly the augmentation ideal.

Theorem FoxDifferential.identityDifferentialModuleEquivAugmentationIdeal_d

omit [DecidableEq H] in
@[simp]
theorem identityDifferentialModuleEquivAugmentationIdeal_d (h : H) :
    identityDifferentialModuleEquivAugmentationIdeal (H := H)
        (universalDifferential (MonoidHom.id H) h) =
      augmentationGeneratorSubtype (H := H) h

Under the identity differential module equivalence, the universal differential \(d(h)\) corresponds to the augmentation generator \(h-1\).

Show Lean proof

ProCGroups.FoxDifferential.Discrete.KernelBoundary.IdentityAugmentation

Declarations