FoxDifferential.Discrete.KernelBoundary.IdentityAugmentation
This module develops the rewriting and basis constructions behind the subgroup calculations. It tracks words and relations through the chosen transversal to obtain the required presentation or basis statements.
import
- FoxDifferential.Discrete.GroupRing
- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
- Mathlib.RepresentationTheory.Homological.GroupHomology.Shapiro
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.
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 rightRegularRepresentation_apply_single (g h : H) (n : ℤ) :
rightRegularRepresentation H g (Finsupp.single h n) =
Finsupp.single (h * g⁻¹) nThe right-regular representation sends a single group element to the corresponding basis action.
Show proof
by
ext a
simp only [rightRegularRepresentation, MonoidAlgebra.of_apply, MonoidHom.coe_mk, OneHom.coe_mk,
LinearMap.coe_mk, AddHom.coe_mk, MonoidAlgebra.single_mul_single, mul_one]Proof. Unfold the relevant Fox differential, quotient, or finite-stage map. The asserted formula is checked on group-ring generators or quotient classes; linearity, the crossed-derivation rule, and the defining augmentation/kernel relations extend the calculation to the whole module.
□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 proof
by
exact rightRegularRepresentation_apply_single (H := H) g h (1 : ℤ)Proof. Unfold the relevant Fox differential, quotient, or finite-stage map. The asserted formula is checked on group-ring generators or quotient classes; linearity, the crossed-derivation rule, and the defining augmentation/kernel relations extend the calculation to the whole module.
□abbrev rightRegularRep : Rep ℤ H := Rep.of (rightRegularRepresentation H)The right-regular representation as an object of Rep \(\mathbb{Z}\) H.
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 proof
by
rw [groupHomology.d₂₁_single]
simp only [of_ρ, rightRegularRepresentation, MonoidAlgebra.of_apply, MonoidHom.coe_mk, OneHom.coe_mk, inv_inv,
LinearMap.coe_mk, AddHom.coe_mk, sub_eq_add_neg, add_comm, relationElement, MonoidHom.id_apply, Finsupp.smul_single,
smul_eq_mul, mul_one, neg_add_rev, add_left_comm, smul_add, smul_neg, neg_smul, neg_neg, add_assoc]Proof. Use the algebraic crossed-differential rule. The values on generators determine the map, and the product, inverse, quotient, and power formulas follow from the rule \(d(xy)=d(x)+x d(y)\) by induction and linearity. Universal-module and lift statements are checked on basis elements and then descend through the defining crossed-differential relations. Equality, naturality, and matrix formulas follow from generator or basis extensionality, while augmentation-kernel claims use the Fox fundamental formula.
□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 proof
by
rw [rightRegular_d₂₁_single]
simp only [relationElement_eq_crossedDifferentialRelationElement, neg_neg]Proof. Use the algebraic crossed-differential rule. The values on generators determine the map, and the product, inverse, quotient, and power formulas follow from the rule \(d(xy)=d(x)+x d(y)\) by induction and linearity. Universal-module and lift statements are checked on basis elements and then descend through the defining crossed-differential relations. Equality, naturality, and matrix formulas follow from generator or basis extensionality, while augmentation-kernel claims use the Fox fundamental formula.
□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 proof
by
induction x using Finsupp.induction with
| zero =>
simp only [relationSubmodule_eq_crossedDifferentialRelationSubmodule, map_zero, zero_mem]
| single_add g r x hg hx ih =>
have hs :
groupHomology.d₂₁ (rightRegularRep H) (Finsupp.single g r) ∈
relationSubmodule (MonoidHom.id H) := by
rw [rightRegular_d₂₁_single]
exact (relationSubmodule (MonoidHom.id H)).smul_mem _
(relationElement_mem (MonoidHom.id H) g.1 g.2)
simpa [map_add] using (relationSubmodule (MonoidHom.id H)).add_mem hs ihProof. Use the algebraic crossed-differential rule. The values on generators determine the map, and the product, inverse, quotient, and power formulas follow from the rule \(d(xy)=d(x)+x d(y)\) by induction and linearity. Universal-module and lift statements are checked on basis elements and then descend through the defining crossed-differential relations. Equality, naturality, and matrix formulas follow from generator or basis extensionality, while augmentation-kernel claims use the Fox fundamental formula.
□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 proof
by
calc
groupHomology.d₂₁ (rightRegularRep H) (r • Finsupp.single g a)
= groupHomology.d₂₁ (rightRegularRep H) (Finsupp.single g (r * a)) := by
simp only [Finsupp.smul_single, smul_eq_mul]
_ = (-(r * a)) • relationElement (MonoidHom.id H) g.1 g.2 := by
rw [rightRegular_d₂₁_single]
_ = r • ((-a) • relationElement (MonoidHom.id H) g.1 g.2) := by
simp only [relationElement_eq_crossedDifferentialRelationElement, neg_smul, smul_neg, smul_smul]
_ = r • groupHomology.d₂₁ (rightRegularRep H) (Finsupp.single g a) := by
rw [rightRegular_d₂₁_single]Proof. Use the algebraic crossed-differential rule. The values on generators determine the map, and the product, inverse, quotient, and power formulas follow from the rule \(d(xy)=d(x)+x d(y)\) by induction and linearity. Universal-module and lift statements are checked on basis elements and then descend through the defining crossed-differential relations. Equality, naturality, and matrix formulas follow from generator or basis extensionality, while augmentation-kernel claims use the Fox fundamental formula.
□theorem rightRegular_d₂₁_smul (r : GroupRing H) (x : H × H →₀ GroupRing H) :
groupHomology.d₂₁ (rightRegularRep H) (r • x) =
r • groupHomology.d₂₁ (rightRegularRep H) xThe right-regular \(d_{21}\) map is compatible with scalar multiplication.
Show proof
by
induction x using Finsupp.induction with
| zero =>
simp only [smul_zero, map_zero]
| single_add g a x hg hx ih =>
rw [smul_add, map_add, ih, rightRegular_d₂₁_smul_single]
simp only [map_add, smul_add]Proof. Use the algebraic crossed-differential rule. The values on generators determine the map, and the product, inverse, quotient, and power formulas follow from the rule \(d(xy)=d(x)+x d(y)\) by induction and linearity. Universal-module and lift statements are checked on basis elements and then descend through the defining crossed-differential relations. Equality, naturality, and matrix formulas follow from generator or basis extensionality, while augmentation-kernel claims use the Fox fundamental formula.
□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 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 proof
Iff.rflProof. Use the algebraic crossed-differential rule. The values on generators determine the map, and the product, inverse, quotient, and power formulas follow from the rule \(d(xy)=d(x)+x d(y)\) by induction and linearity. Universal-module and lift statements are checked on basis elements and then descend through the defining crossed-differential relations. Equality, naturality, and matrix formulas follow from generator or basis extensionality, while augmentation-kernel claims use the Fox fundamental formula.
□theorem relationElement_mem_rightRegularBoundariesSubmodule (g₁ g₂ : H) :
relationElement (MonoidHom.id H) g₁ g₂ ∈ rightRegularBoundariesSubmodule HEach identity-Crowell relation already lies in the right-regular boundary submodule.
Show proof
by
refine ⟨Finsupp.single (g₁, g₂) (-1), ?_⟩
simpa using
(relationElement_eq_rightRegular_d₂₁_single (H := H) g₁ g₂ (1 : GroupRing H)).symmProof. Use the algebraic crossed-differential rule. The values on generators determine the map, and the product, inverse, quotient, and power formulas follow from the rule \(d(xy)=d(x)+x d(y)\) by induction and linearity. Universal-module and lift statements are checked on basis elements and then descend through the defining crossed-differential relations. Equality, naturality, and matrix formulas follow from generator or basis extensionality, while augmentation-kernel claims use the Fox fundamental formula.
□theorem relationSubmodule_le_rightRegularBoundariesSubmodule :
relationSubmodule (MonoidHom.id H) ≤ rightRegularBoundariesSubmodule HThe identity Crowell relation submodule is contained in the right-regular boundary submodule.
Show proof
by
rw [relationSubmodule]
refine Submodule.span_le.2 ?_
rintro _ ⟨⟨g₁, g₂⟩, rfl⟩
exact relationElement_mem_rightRegularBoundariesSubmodule (H := H) g₁ g₂Proof. Use the algebraic crossed-differential rule. The values on generators determine the map, and the product, inverse, quotient, and power formulas follow from the rule \(d(xy)=d(x)+x d(y)\) by induction and linearity. Universal-module and lift statements are checked on basis elements and then descend through the defining crossed-differential relations. Equality, naturality, and matrix formulas follow from generator or basis extensionality, while augmentation-kernel claims use the Fox fundamental formula.
□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 proof
by
intro x hx
rcases hx with ⟨y, rfl⟩
exact rightRegular_d₂₁_mem_relationSubmodule (H := H) yProof. Use the algebraic crossed-differential rule. The values on generators determine the map, and the product, inverse, quotient, and power formulas follow from the rule \(d(xy)=d(x)+x d(y)\) by induction and linearity. Universal-module and lift statements are checked on basis elements and then descend through the defining crossed-differential relations. Equality, naturality, and matrix formulas follow from generator or basis extensionality, while augmentation-kernel claims use the Fox fundamental formula.
□theorem rightRegularBoundariesSubmodule_le_relationSubmodule :
rightRegularBoundariesSubmodule H ≤ relationSubmodule (MonoidHom.id H)The right-regular boundary submodule is contained in the relation submodule.
Show proof
by
intro x hx
exact rightRegular_boundaries₁_le_relationSubmodule (H := H) hxProof. Use the algebraic crossed-differential rule. The values on generators determine the map, and the product, inverse, quotient, and power formulas follow from the rule \(d(xy)=d(x)+x d(y)\) by induction and linearity. Universal-module and lift statements are checked on basis elements and then descend through the defining crossed-differential relations. Equality, naturality, and matrix formulas follow from generator or basis extensionality, while augmentation-kernel claims use the Fox fundamental formula.
□theorem relationSubmodule_eq_rightRegularBoundariesSubmodule :
relationSubmodule (MonoidHom.id H) = rightRegularBoundariesSubmodule HThe identity Crowell relations are exactly the right-regular degree-1 boundaries.
Show proof
by
exact le_antisymm
(relationSubmodule_le_rightRegularBoundariesSubmodule (H := H))
(rightRegularBoundariesSubmodule_le_relationSubmodule (H := H))Proof. Use the algebraic crossed-differential rule. The values on generators determine the map, and the product, inverse, quotient, and power formulas follow from the rule \(d(xy)=d(x)+x d(y)\) by induction and linearity. Universal-module and lift statements are checked on basis elements and then descend through the defining crossed-differential relations. Equality, naturality, and matrix formulas follow from generator or basis extensionality, while augmentation-kernel claims use the Fox fundamental formula.
□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 gThe lifted linear identity-boundary map has the stated value on a single group-ring generator.
Show proof
by
simp only [liftLinear, Finsupp.linearCombination_single, groupRingBoundary, MonoidHom.id_apply,
MonoidAlgebra.of_apply, smul_eq_mul, mul_sub, mul_one, augmentationGenerator]Proof. Unfold the relevant Fox differential, quotient, or finite-stage map. The asserted formula is checked on group-ring generators or quotient classes; linearity, the crossed-derivation rule, and the defining augmentation/kernel relations extend the calculation to the whole module.
□theorem liftLinear_groupRingBoundary_id_mem_augmentationIdeal (x : DifferentialPreModule H H) :
liftLinear (H := H) (G := H) (A := GroupRing H)
(groupRingBoundary (MonoidHom.id H)) x ∈ augmentationIdeal HThe pre-boundary map for the identity case lands in the augmentation ideal.
Show proof
by
rw [liftLinear, Finsupp.linearCombination_apply]
exact Submodule.sum_mem (augmentationIdeal H) fun g _ =>
(augmentationIdeal H).smul_mem _ <|
groupRingBoundary_mem_augmentationIdeal (H := H) (MonoidHom.id H) gProof. Use the algebraic crossed-differential rule. The values on generators determine the map, and the product, inverse, quotient, and power formulas follow from the rule \(d(xy)=d(x)+x d(y)\) by induction and linearity. Universal-module and lift statements are checked on basis elements and then descend through the defining crossed-differential relations. Equality, naturality, and matrix formulas follow from generator or basis extensionality, while augmentation-kernel claims use the Fox fundamental formula.
□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 proof
by
refine ⟨Finsupp.single h 1, ?_⟩
simp only [liftLinear_single, groupRingBoundary, MonoidHom.id_apply, MonoidAlgebra.of_apply, smul_eq_mul,
one_mul, augmentationGenerator]Proof. Use the algebraic crossed-differential rule. The values on generators determine the map, and the product, inverse, quotient, and power formulas follow from the rule \(d(xy)=d(x)+x d(y)\) by induction and linearity. Universal-module and lift statements are checked on basis elements and then descend through the defining crossed-differential relations. Equality, naturality, and matrix formulas follow from generator or basis extensionality, while augmentation-kernel claims use the Fox fundamental formula.
□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 proof
by
have hgen :
(augmentationGeneratorIdeal H : Submodule (GroupRing H) (GroupRing H)) ≤
LinearMap.range (liftLinear (H := H) (G := H) (A := GroupRing H)
(groupRingBoundary (MonoidHom.id H))) := by
refine Ideal.span_le.2 ?_
rintro _ ⟨h, rfl⟩
exact augmentationGenerator_mem_range_liftLinear_groupRingBoundary_id (H := H) h
simpa [congrArg
(fun I : Ideal (GroupRing H) => (I : Submodule (GroupRing H) (GroupRing H)))
(augmentationGeneratorIdeal_eq_augmentationIdeal (H := H))] using hgenProof. Use the algebraic crossed-differential rule. The values on generators determine the map, and the product, inverse, quotient, and power formulas follow from the rule \(d(xy)=d(x)+x d(y)\) by induction and linearity. Universal-module and lift statements are checked on basis elements and then descend through the defining crossed-differential relations. Equality, naturality, and matrix formulas follow from generator or basis extensionality, while augmentation-kernel claims use the Fox fundamental formula.
□theorem liftLinear_groupRingBoundary_id_eq_d₁₀ :
(liftLinear (H := H) (G := H) (A := GroupRing H)
(groupRingBoundary (MonoidHom.id H))).restrictScalars ℤ =
(groupHomology.d₁₀ (rightRegularRep H)).homFor the identity homomorphism, the lifted group-ring boundary equals the degree-one differential for the right-regular representation.
Show proof
by
apply Finsupp.lhom_ext
intro g r
rw [groupHomology.d₁₀_single]
simp only [liftLinear, LinearMap.coe_restrictScalars, Finsupp.linearCombination_single, groupRingBoundary,
MonoidHom.id_apply, MonoidAlgebra.of_apply, sub_eq_add_neg, smul_eq_mul, mul_add, mul_neg, mul_one, of_ρ,
rightRegularRepresentation, MonoidHom.coe_mk, OneHom.coe_mk, inv_inv, LinearMap.coe_mk, AddHom.coe_mk]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) xThe identity group-ring boundary lift is evaluated on canonical generators and then extended linearly.
Show proof
by
exact congrArg (fun f : DifferentialPreModule H H →ₗ[ℤ] GroupRing H => f x)
(liftLinear_groupRingBoundary_id_eq_d₁₀ H)Proof. Use the algebraic crossed-differential rule. The values on generators determine the map, and the product, inverse, quotient, and power formulas follow from the rule \(d(xy)=d(x)+x d(y)\) by induction and linearity. Universal-module and lift statements are checked on basis elements and then descend through the defining crossed-differential relations. Equality, naturality, and matrix formulas follow from generator or basis extensionality, while augmentation-kernel claims use the Fox fundamental formula.
□theorem rightRegular_d₁₀_mem_augmentationIdeal (x : DifferentialPreModule H H) :
groupHomology.d₁₀ (rightRegularRep H) x ∈ augmentationIdeal HThe right-regular degree-0 differential lands in the augmentation ideal.
Show proof
by
simpa [liftLinear_groupRingBoundary_id_apply] using
liftLinear_groupRingBoundary_id_mem_augmentationIdeal (H := H) xProof. Use the algebraic crossed-differential rule. The values on generators determine the map, and the product, inverse, quotient, and power formulas follow from the rule \(d(xy)=d(x)+x d(y)\) by induction and linearity. Universal-module and lift statements are checked on basis elements and then descend through the defining crossed-differential relations. Equality, naturality, and matrix formulas follow from generator or basis extensionality, while augmentation-kernel claims use the Fox fundamental formula.
□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 proof
by
ext y
constructor
· rintro ⟨x, rfl⟩
exact rightRegular_d₁₀_mem_augmentationIdeal (H := H) x
· intro hy
rcases augmentationIdeal_le_range_liftLinear_groupRingBoundary_id (H := H) hy with ⟨x, hx⟩
refine ⟨x, ?_⟩
rw [← LinearMap.congr_fun (liftLinear_groupRingBoundary_id_eq_d₁₀ (H := H)) x]
exact hxProof. Use the algebraic crossed-differential rule. The values on generators determine the map, and the product, inverse, quotient, and power formulas follow from the rule \(d(xy)=d(x)+x d(y)\) by induction and linearity. Universal-module and lift statements are checked on basis elements and then descend through the defining crossed-differential relations. Equality, naturality, and matrix formulas follow from generator or basis extensionality, while augmentation-kernel claims use the Fox fundamental formula.
□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.
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 indBottomTrivialUnderlyingEquiv_mk (h : H) (n : ℤ) :
indBottomTrivialUnderlyingEquiv H
(Representation.IndV.mk (⊥ : Subgroup H).subtype (bottomTrivialRep H).ρ h n) =
Finsupp.single h nThe 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 proof
by
change (TensorProduct.rid ℤ (GroupRing H))
((Representation.Coinvariants.lift
(Representation.tprod (((Rep.leftRegular ℤ H).ρ.comp (⊥ : Subgroup H).subtype))
(bottomTrivialRep H).ρ)
LinearMap.id
(fun x => by
ext y
have : x = (1 : (⊥ : Subgroup H)) := Subsingleton.elim _ _
subst this
simp only [of_ρ, Function.comp_apply, map_one, LinearMap.id_comp, LinearMap.coe_comp,
Finsupp.lsingle_apply, AlgebraTensorModule.curry_apply, LinearMap.restrictScalars_self, curry_apply,
Module.End.one_apply, LinearMap.id_coe, id_eq]))
(Representation.Coinvariants.mk _ (Finsupp.single h 1 ⊗ₜ[ℤ] n))) = _
rw [Representation.Coinvariants.lift_mk]
simp only [LinearMap.id_coe, id_eq, rid_tmul, MonoidAlgebra.smul_single, Int.zsmul_eq_mul, mul_one]Proof. Use the algebraic crossed-differential rule. The values on generators determine the map, and the product, inverse, quotient, and power formulas follow from the rule \(d(xy)=d(x)+x d(y)\) by induction and linearity. Universal-module and lift statements are checked on basis elements and then descend through the defining crossed-differential relations. Equality, naturality, and matrix formulas follow from generator or basis extensionality, while augmentation-kernel claims use the Fox fundamental formula.
□def indBottomTrivialIsoRightRegular :
Rep.ind (⊥ : Subgroup H).subtype (bottomTrivialRep H) ≅ rightRegularRep H :=
Action.mkIso (indBottomTrivialUnderlyingEquiv H).toModuleIso fun g => by
refine ModuleCat.hom_ext <| Representation.IndV.hom_ext (φ := (⊥ : Subgroup H).subtype)
(ρ := (bottomTrivialRep H).ρ) ?_
intro h
ext n
change (indBottomTrivialUnderlyingEquiv H)
(((Rep.ind (⊥ : Subgroup H).subtype (bottomTrivialRep H)).ρ g)
((Representation.IndV.mk (⊥ : Subgroup H).subtype (bottomTrivialRep H).ρ h) (1 : ℤ))) n =
(rightRegularRepresentation H g
(indBottomTrivialUnderlyingEquiv H
((Representation.IndV.mk (⊥ : Subgroup H).subtype (bottomTrivialRep H).ρ h) (1 : ℤ)))) n
have hind :
(((Rep.ind (⊥ : Subgroup H).subtype (bottomTrivialRep H)).ρ g)
((Representation.IndV.mk (⊥ : Subgroup H).subtype (bottomTrivialRep H).ρ h) (1 : ℤ))) =
(Representation.IndV.mk (⊥ : Subgroup H).subtype (bottomTrivialRep H).ρ (h * g⁻¹))
(1 : ℤ) := by
simp only [Rep.ind, of_ρ, ind_apply, LinearMap.coe_comp, Function.comp_apply, mk_apply, Coinvariants.map_mk,
LinearMap.rTensor_tmul, Finsupp.lmapDomain_apply, Finsupp.mapDomain_single]
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.
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.symmGroup homology respects isomorphic representations.
def rightRegularH1IsoBottom :
groupHomology (rightRegularRep H) 1 ≅ groupHomology (bottomTrivialRep H) 1 := by
exact (groupHomologyIsoOfRepIso H (indBottomTrivialIsoRightRegular H).symm 1) ≪≫
groupHomology.indIso (⊥ : Subgroup H) (bottomTrivialRep H) 1The first homology of the right-regular representation is identified with the first homology of the trivial subgroup.
theorem rightRegular_H1_isZero : Limits.IsZero (groupHomology (rightRegularRep H) 1)The first homology of the right-regular representation vanishes.
Show proof
by
classical
let hbot : Limits.IsZero (groupHomology (bottomTrivialRep H) 1) := by
simpa using (isZero_groupHomology_succ_of_subsingleton (A := bottomTrivialRep H) 0)
exact hbot.of_iso (rightRegularH1IsoBottom H)Proof. Use the algebraic crossed-differential rule. The values on generators determine the map, and the product, inverse, quotient, and power formulas follow from the rule \(d(xy)=d(x)+x d(y)\) by induction and linearity. Universal-module and lift statements are checked on basis elements and then descend through the defining crossed-differential relations. Equality, naturality, and matrix formulas follow from generator or basis extensionality, while augmentation-kernel claims use the Fox fundamental formula.
□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 proof
by
classical
apply le_antisymm
· intro x hx
let hzero := rightRegular_H1_isZero H
haveI : Subsingleton (groupHomology (rightRegularRep H) 1) :=
ModuleCat.subsingleton_of_isZero hzero
let z : groupHomology.cycles₁ (rightRegularRep H) := ⟨x, hx⟩
exact (groupHomology.H1π_eq_zero_iff (A := rightRegularRep H) z).1 (Subsingleton.elim _ _)
· exact groupHomology.boundaries₁_le_cycles₁ (rightRegularRep H)Proof. Use the algebraic crossed-differential rule. The values on generators determine the map, and the product, inverse, quotient, and power formulas follow from the rule \(d(xy)=d(x)+x d(y)\) by induction and linearity. Universal-module and lift statements are checked on basis elements and then descend through the defining crossed-differential relations. Equality, naturality, and matrix formulas follow from generator or basis extensionality, while augmentation-kernel claims use the Fox fundamental formula.
□theorem mem_rightRegularBoundariesSubmodule_iff_d₁₀_eq_zero
{H : Type} [Group H] {x : DifferentialPreModule H H} :
x ∈ rightRegularBoundariesSubmodule H ↔ groupHomology.d₁₀ (rightRegularRep H) x = 0For the right-regular representation, a 1-chain is a boundary exactly when its degree-0 differential vanishes.
Show proof
by
constructor
· intro hx
have hx' : x ∈ groupHomology.boundaries₁ (rightRegularRep H) := hx
have hcycle := groupHomology.mem_cycles₁_of_mem_boundaries₁ (A := rightRegularRep H) x hx'
simpa [groupHomology.cycles₁, LinearMap.mem_ker] using hcycle
· intro hx
have hcycle : x ∈ groupHomology.cycles₁ (rightRegularRep H) := by
simpa [groupHomology.cycles₁, LinearMap.mem_ker] using hx
have hbound : x ∈ groupHomology.boundaries₁ (rightRegularRep H) := by
simpa [rightRegular_cycles₁_eq_boundaries₁ (H := H)] using hcycle
exact hboundProof. Use the algebraic crossed-differential rule. The values on generators determine the map, and the product, inverse, quotient, and power formulas follow from the rule \(d(xy)=d(x)+x d(y)\) by induction and linearity. Universal-module and lift statements are checked on basis elements and then descend through the defining crossed-differential relations. Equality, naturality, and matrix formulas follow from generator or basis extensionality, while augmentation-kernel claims use the Fox fundamental formula.
□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)).symmThe quotient of the free pre-module by right-regular degree-1 boundaries is the identity Crowell differential module.
theorem rightRegularBoundariesQuotientEquivIdentityDifferentialModule_mk
(x : DifferentialPreModule H H) :
rightRegularBoundariesQuotientEquivIdentityDifferentialModule H
(Submodule.Quotient.mk x) =
(relationSubmodule (MonoidHom.id H)).mkQ xThe 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 proof
by
rw [rightRegularBoundariesQuotientEquivIdentityDifferentialModule,
Submodule.quotEquivOfEq_mk]
rflProof. Use the algebraic crossed-differential rule. The values on generators determine the map, and the product, inverse, quotient, and power formulas follow from the rule \(d(xy)=d(x)+x d(y)\) by induction and linearity. Universal-module and lift statements are checked on basis elements and then descend through the defining crossed-differential relations. Equality, naturality, and matrix formulas follow from generator or basis extensionality, while augmentation-kernel claims use the Fox fundamental formula.
□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 [relationSubmodule_eq_crossedDifferentialRelationSubmodule, map_add]
map_smul' := by
intro r x
simp only [relationSubmodule_eq_crossedDifferentialRelationSubmodule, map_smul, RingHom.id_apply]}The quotient by right-regular boundaries maps onto the augmentation ideal.
theorem rightRegularBoundariesQuotientToAugmentationIdeal_mk_single (h : H) :
rightRegularBoundariesQuotientToAugmentationIdeal H
(Submodule.Quotient.mk (Finsupp.single h 1)) =
augmentationGeneratorSubtype (H := H) hThe quotient map from right-regular boundaries to the augmentation ideal sends a single generator to the corresponding augmentation generator.
Show proof
by
apply Subtype.ext
simpa [rightRegularBoundariesQuotientToAugmentationIdeal,
rightRegularBoundariesQuotientEquivIdentityDifferentialModule_mk,
augmentationGeneratorSubtype, augmentationGenerator, groupRingBoundary]
using toGroupRing_d (MonoidHom.id H) hProof. Unfold the relevant Fox differential, quotient, or finite-stage map. The asserted formula is checked on group-ring generators or quotient classes; linearity, the crossed-derivation rule, and the defining augmentation/kernel relations extend the calculation to the whole module.
□theorem rightRegularBoundariesQuotientToAugmentationIdeal_surjective :
Function.Surjective (rightRegularBoundariesQuotientToAugmentationIdeal H)The quotient by right-regular boundaries surjects onto the augmentation ideal.
Show proof
by
intro y
rcases toAugmentationIdeal_surjective (H := H) (MonoidHom.id H) (fun h => ⟨h, rfl⟩) y with
⟨x, hx⟩
refine ⟨(rightRegularBoundariesQuotientEquivIdentityDifferentialModule H).symm x, ?_⟩
simpa [rightRegularBoundariesQuotientToAugmentationIdeal] using hxProof. Use the algebraic crossed-differential rule. The values on generators determine the map, and the product, inverse, quotient, and power formulas follow from the rule \(d(xy)=d(x)+x d(y)\) by induction and linearity. Universal-module and lift statements are checked on basis elements and then descend through the defining crossed-differential relations. Equality, naturality, and matrix formulas follow from generator or basis extensionality, while augmentation-kernel claims use the Fox fundamental formula.
□theorem rightRegularBoundariesQuotientToAugmentationIdeal_eq_zero_iff
{H : Type} [Group H]
{q : DifferentialPreModule H H ⧸ (rightRegularBoundariesSubmodule H)} :
rightRegularBoundariesQuotientToAugmentationIdeal H q = 0 ↔ q = 0The quotient-to-augmentation map has trivial kernel.
Show proof
by
refine Submodule.Quotient.induction_on _ q ?_
intro x
constructor
· intro hx
have hx' : groupHomology.d₁₀ (rightRegularRep H) x = 0 := by
have hxval := congrArg Subtype.val hx
change toGroupRing (MonoidHom.id H)
((rightRegularBoundariesQuotientEquivIdentityDifferentialModule H)
(Submodule.Quotient.mk x)) = 0 at hxval
rw [rightRegularBoundariesQuotientEquivIdentityDifferentialModule_mk] at hxval
change liftLinear (H := H) (G := H) (A := GroupRing H)
(groupRingBoundary (MonoidHom.id H)) x = 0 at hxval
simpa [liftLinear_groupRingBoundary_id_apply] using hxval
have hmem : x ∈ rightRegularBoundariesSubmodule H := by
exact (mem_rightRegularBoundariesSubmodule_iff_d₁₀_eq_zero (H := H) (x := x)).2 hx'
exact (Submodule.Quotient.mk_eq_zero (p := rightRegularBoundariesSubmodule H) (x := x)).2 hmem
· intro hq
simp only [hq, map_zero]Proof. Use the algebraic crossed-differential rule. The values on generators determine the map, and the product, inverse, quotient, and power formulas follow from the rule \(d(xy)=d(x)+x d(y)\) by induction and linearity. Universal-module and lift statements are checked on basis elements and then descend through the defining crossed-differential relations. Equality, naturality, and matrix formulas follow from generator or basis extensionality, while augmentation-kernel claims use the Fox fundamental formula.
□theorem rightRegularBoundariesQuotientToAugmentationIdeal_injective :
Function.Injective (rightRegularBoundariesQuotientToAugmentationIdeal H)The map from the quotient of right-regular boundaries to the ordinary augmentation ideal is injective.
Show proof
by
intro x y hxy
apply sub_eq_zero.mp
refine (rightRegularBoundariesQuotientToAugmentationIdeal_eq_zero_iff (H := H) (q := x - y)).1 ?_
simpa [LinearMap.map_sub] using sub_eq_zero.mpr hxyProof. Use the algebraic crossed-differential rule. The values on generators determine the map, and the product, inverse, quotient, and power formulas follow from the rule \(d(xy)=d(x)+x d(y)\) by induction and linearity. Universal-module and lift statements are checked on basis elements and then descend through the defining crossed-differential relations. Equality, naturality, and matrix formulas follow from generator or basis extensionality, while augmentation-kernel claims use the Fox fundamental formula.
□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 identityDifferentialModuleEquivAugmentationIdeal_d (h : H) :
identityDifferentialModuleEquivAugmentationIdeal (H := H)
(universalDifferential (MonoidHom.id H) h) =
augmentationGeneratorSubtype (H := H) hUnder the identity differential module equivalence, the universal differential \(d(h)\) corresponds to the augmentation generator \(h-1\).
Show proof
by
change
(identityDifferentialModuleEquivAugmentationIdeal (H := H)).toLinearMap
(universalDifferential (MonoidHom.id H) h) =
augmentationGeneratorSubtype (H := H) h
rw [identityDifferentialModuleEquivAugmentationIdeal_toLinearMap]
rw [toAugmentationIdeal_d]
apply Subtype.ext
rflProof. Use the algebraic crossed-differential rule. The values on generators determine the map, and the product, inverse, quotient, and power formulas follow from the rule \(d(xy)=d(x)+x d(y)\) by induction and linearity. Universal-module and lift statements are checked on basis elements and then descend through the defining crossed-differential relations. Equality, naturality, and matrix formulas follow from generator or basis extensionality, while augmentation-kernel claims use the Fox fundamental formula.
□