FoxDifferential.Discrete.GroupRing
This module develops Fox differentials and completed Fox coordinates for free, profinite, and pro-\(C\) group constructions.
import
- FoxDifferential.Discrete.DifferentialModule.Boundary
- Mathlib.Algebra.MonoidAlgebra.Basic
- Mathlib.RingTheory.Ideal.Maps
def augmentationAlgHom : GroupRing H →ₐ[ℤ] ℤ :=
MonoidAlgebra.lift ℤ ℤ H (1 : H →* ℤ)The augmentation algebra homomorphism \(\mathbb{Z}[H] \to \mathbb{Z}\).
def augmentation : GroupRing H →+* ℤ :=
(augmentationAlgHom H).toRingHomThe augmentation ring homomorphism \(\mathbb{Z}[H] \to \mathbb{Z}\).
def augmentationIdeal : Ideal (GroupRing H) :=
RingHom.ker (augmentation H)The augmentation ideal of the integral group ring \(\mathbb{Z}[H]\).
def augmentationGeneratorIdeal : Ideal (GroupRing H) :=
Ideal.span (Set.range (augmentationGenerator H))
@[simp]The ideal generated by the standard augmentation generators \(h-1\).
theorem augmentation_of (h : H) :
augmentation H (MonoidAlgebra.of ℤ H h) = 1The augmentation map has the stated value on group-ring elements.
Show proof
by
simp only [augmentation, augmentationAlgHom, AlgHom.toRingHom_eq_coe, MonoidAlgebra.of_apply, RingHom.coe_coe,
MonoidAlgebra.lift_single, MonoidHom.one_apply, Int.zsmul_eq_mul, mul_one]
@[simp]Proof. Compute in the integral group ring. The augmentation homomorphism sends every group basis element to \(1\) and extends linearly, so its values, kernel, and augmentation ideal are checked by reducing a finite sum to its coefficient sum. The ideal generated by the elements \(h-1\) is compared with this kernel by rewriting augmentation-zero finite sums as sums of such generators.
□theorem augmentation_one :
augmentation H (1 : GroupRing H) = 1The augmentation sends the group identity to \(1\).
Show proof
by
simp only [augmentation, augmentationAlgHom, AlgHom.toRingHom_eq_coe, map_one]Proof. Compute in the integral group ring. The augmentation homomorphism sends every group basis element to \(1\) and extends linearly, so its values, kernel, and augmentation ideal are checked by reducing a finite sum to its coefficient sum. The ideal generated by the elements \(h-1\) is compared with this kernel by rewriting augmentation-zero finite sums as sums of such generators.
□theorem mem_augmentationIdeal_iff {x : GroupRing H} :
x ∈ augmentationIdeal H ↔ augmentation H x = 0A group-ring element lies in the Fox augmentation ideal iff its augmentation is zero.
Show proof
by
rw [augmentationIdeal, RingHom.mem_ker]
@[simp]Proof. Compute in the integral group ring. The augmentation homomorphism sends every group basis element to \(1\) and extends linearly, so its values, kernel, and augmentation ideal are checked by reducing a finite sum to its coefficient sum. The ideal generated by the elements \(h-1\) is compared with this kernel by rewriting augmentation-zero finite sums as sums of such generators.
□theorem groupRingBoundary_mem_augmentationIdeal
{G : Type*} [Group G] (ψ : G →* H) (g : G) :
groupRingBoundary ψ g ∈ augmentationIdeal HThe group-ring boundary value \([\psi(g)]-1\) lies in the augmentation ideal.
Show proof
by
rw [mem_augmentationIdeal_iff]
simp only [augmentation, augmentationAlgHom, AlgHom.toRingHom_eq_coe, groupRingBoundary,
MonoidAlgebra.of_apply, RingHom.coe_coe, map_sub, MonoidAlgebra.lift_single, MonoidHom.one_apply, Int.zsmul_eq_mul,
mul_one, map_one, sub_self]
@[simp]Proof. Compute in the integral group ring. The augmentation homomorphism sends every group basis element to \(1\) and extends linearly, so its values, kernel, and augmentation ideal are checked by reducing a finite sum to its coefficient sum. The ideal generated by the elements \(h-1\) is compared with this kernel by rewriting augmentation-zero finite sums as sums of such generators.
□theorem augmentationGenerator_mem_augmentationIdeal (h : H) :
augmentationGenerator H h ∈ augmentationIdeal HEach standard generator \(h-1\) lies in the ordinary group-ring augmentation ideal.
Show proof
by
simpa [augmentationGenerator_eq_groupRingBoundary] using
groupRingBoundary_mem_augmentationIdeal (H := H) (G := H) (MonoidHom.id H) h
@[simp]Proof. Compute in the integral group ring. The augmentation homomorphism sends every group basis element to \(1\) and extends linearly, so its values, kernel, and augmentation ideal are checked by reducing a finite sum to its coefficient sum. The ideal generated by the elements \(h-1\) is compared with this kernel by rewriting augmentation-zero finite sums as sums of such generators.
□theorem augmentationGenerator_mem_augmentationGeneratorIdeal (h : H) :
augmentationGenerator H h ∈ augmentationGeneratorIdeal HAugmentation generators lie in the augmentation-generator ideal.
Show proof
by
exact Ideal.subset_span ⟨h, rfl⟩Proof. Compute in the integral group ring. The augmentation homomorphism sends every group basis element to \(1\) and extends linearly, so its values, kernel, and augmentation ideal are checked by reducing a finite sum to its coefficient sum. The ideal generated by the elements \(h-1\) is compared with this kernel by rewriting augmentation-zero finite sums as sums of such generators.
□theorem augmentationGeneratorIdeal_le_augmentationIdeal :
augmentationGeneratorIdeal H ≤ augmentationIdeal HThe generator-defined augmentation ideal is contained in the ordinary group-ring augmentation ideal.
Show proof
by
refine Ideal.span_le.2 ?_
rintro _ ⟨h, rfl⟩
exact augmentationGenerator_mem_augmentationIdeal H hProof. Compute in the integral group ring. The augmentation homomorphism sends every group basis element to \(1\) and extends linearly, so its values, kernel, and augmentation ideal are checked by reducing a finite sum to its coefficient sum. The ideal generated by the elements \(h-1\) is compared with this kernel by rewriting augmentation-zero finite sums as sums of such generators.
□theorem exists_mem_augmentationGeneratorIdeal_add (x : GroupRing H) :
∃ y ∈ augmentationGeneratorIdeal H, x = y + (augmentation H x : GroupRing H)An augmentation-zero group-ring element can be decomposed using the standard augmentation generators.
Show proof
by
refine (MonoidAlgebra.induction_on
(p := fun x =>
∃ y ∈ augmentationGeneratorIdeal H, x = y + (augmentation H x : GroupRing H))
x ?_ ?_ ?_)
· intro h
refine ⟨augmentationGenerator H h, augmentationGenerator_mem_augmentationGeneratorIdeal H h, ?_⟩
simp only [MonoidAlgebra.of_apply, augmentationGenerator, augmentation, augmentationAlgHom,
AlgHom.toRingHom_eq_coe, RingHom.coe_coe, MonoidAlgebra.lift_single, MonoidHom.one_apply, Int.zsmul_eq_mul, mul_one,
Int.cast_one, sub_add_cancel]
· intro x z hx hz
rcases hx with ⟨y, hy, hxy⟩
rcases hz with ⟨w, hw, hwz⟩
refine ⟨y + w, (augmentationGeneratorIdeal H).add_mem hy hw, ?_⟩
have hy0 : augmentation H y = 0 :=
(mem_augmentationIdeal_iff (H := H)).1 (augmentationGeneratorIdeal_le_augmentationIdeal H hy)
have hw0 : augmentation H w = 0 :=
(mem_augmentationIdeal_iff (H := H)).1 (augmentationGeneratorIdeal_le_augmentationIdeal H hw)
rw [hxy, hwz, map_add]
simp only [add_left_comm, add_assoc, map_add, hy0, map_intCast, Int.cast_eq, zero_add, hw0, Int.cast_add]
· intro n x hx
rcases hx with ⟨y, hy, hxy⟩
refine ⟨n • y, zsmul_mem hy n, ?_⟩
have hy0 : augmentation H y = 0 :=
(mem_augmentationIdeal_iff (H := H)).1 (augmentationGeneratorIdeal_le_augmentationIdeal H hy)
rw [hxy, smul_add]
simp only [zsmul_eq_mul, map_add, map_mul, map_intCast, Int.cast_eq, hy0, mul_zero, zero_add, Int.cast_mul]Proof. Compute in the integral group ring. The augmentation homomorphism sends every group basis element to \(1\) and extends linearly, so its values, kernel, and augmentation ideal are checked by reducing a finite sum to its coefficient sum. The ideal generated by the elements \(h-1\) is compared with this kernel by rewriting augmentation-zero finite sums as sums of such generators.
□theorem augmentationIdeal_le_augmentationGeneratorIdeal :
augmentationIdeal H ≤ augmentationGeneratorIdeal HThe ordinary group-ring augmentation ideal is contained in the ideal generated by the elements \(g-1\).
Show proof
by
intro x hx
rcases exists_mem_augmentationGeneratorIdeal_add H x with ⟨y, hy, hxy⟩
have haug : augmentation H x = 0 := (mem_augmentationIdeal_iff (H := H)).1 hx
rw [hxy, haug]
simpa using hyProof. Compute in the integral group ring. The augmentation homomorphism sends every group basis element to \(1\) and extends linearly, so its values, kernel, and augmentation ideal are checked by reducing a finite sum to its coefficient sum. The ideal generated by the elements \(h-1\) is compared with this kernel by rewriting augmentation-zero finite sums as sums of such generators.
□theorem augmentationGeneratorIdeal_eq_augmentationIdeal :
augmentationGeneratorIdeal H = augmentationIdeal HThe ideal generated by the standard elements \(g-1\) is the ordinary augmentation ideal.
Show proof
by
exact le_antisymm (augmentationGeneratorIdeal_le_augmentationIdeal H)
(augmentationIdeal_le_augmentationGeneratorIdeal H)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.
□def augmentationBoundary (ψ : G →* H) (g : G) : augmentationIdeal H :=
⟨groupRingBoundary ψ g, groupRingBoundary_mem_augmentationIdeal (H := H) ψ g⟩The Crowell boundary map with codomain restricted to the augmentation ideal.
def augmentationGeneratorSubtype (h : H) : augmentationIdeal H :=
⟨augmentationGenerator H h, augmentationGenerator_mem_augmentationIdeal H h⟩The standard generators \(h-1\) of the augmentation ideal, viewed in the ideal itself.
theorem toGroupRing_mem_augmentationIdeal (ψ : G →* H) (x : DifferentialModule ψ) :
toGroupRing ψ x ∈ augmentationIdeal HThe group-ring image of any differential-module element lies in the augmentation ideal.
Show proof
by
refine Submodule.Quotient.induction_on (p := relationSubmodule ψ) x ?_
intro y
change liftLinear (A := GroupRing H) (groupRingBoundary ψ) y ∈ augmentationIdeal H
rw [liftLinear, Finsupp.linearCombination_apply]
exact Submodule.sum_mem (augmentationIdeal H) fun g _ =>
(augmentationIdeal H).smul_mem _ (groupRingBoundary_mem_augmentationIdeal (H := H) ψ g)Proof. Compute in the integral group ring. The augmentation homomorphism sends every group basis element to \(1\) and extends linearly, so its values, kernel, and augmentation ideal are checked by reducing a finite sum to its coefficient sum. The ideal generated by the elements \(h-1\) is compared with this kernel by rewriting augmentation-zero finite sums as sums of such generators.
□def toAugmentationIdeal (ψ : G →* H) :
DifferentialModule ψ →ₗ[GroupRing H] augmentationIdeal H :=
LinearMap.codRestrict (augmentationIdeal H) (toGroupRing ψ)
(toGroupRing_mem_augmentationIdeal (H := H) ψ)
@[simp]The factorization \(A_{\psi} \to I(\mathbb{Z}[H])\) of the boundary map through the augmentation ideal.
theorem toAugmentationIdeal_d (ψ : G →* H) (g : G) :
toAugmentationIdeal (H := H) ψ (universalDifferential ψ g) =
augmentationBoundary (H := H) ψ gThe universal differential maps into the ordinary group-ring augmentation ideal.
Show proof
by
apply Subtype.ext
change toGroupRing ψ (universalDifferential ψ g) = groupRingBoundary ψ g
exact toGroupRing_d ψ g
@[simp]Proof. Use the Fox boundary formula and the augmentation calculation. The boundary lands in the augmentation ideal because its augmentation is zero, and the identity-case comparison is checked on generators before extending by linearity and the universal property of the differential module.
□theorem subtype_comp_toAugmentationIdeal (ψ : G →* H) :
(augmentationIdeal H).subtype.comp (toAugmentationIdeal (H := H) ψ) =
toGroupRing ψComposing the boundary factorization through the augmentation ideal with the subtype map gives the original boundary map.
Show proof
by
ext x
rflProof. 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 span_augmentationGeneratorSubtype_eq_top :
Submodule.span (GroupRing H) (Set.range (augmentationGeneratorSubtype (H := H))) = ⊤The standard augmentation generators span the augmentation ideal as a module.
Show proof
by
have hspan :
Submodule.span (GroupRing H)
(Set.range fun h => (⟨augmentationGenerator H h,
augmentationGenerator_mem_augmentationIdeal (H := H) h⟩ : augmentationIdeal H)) = ⊤ := by
rw [Submodule.span_range_subtype_eq_top_iff (p := augmentationIdeal H)
(s := augmentationGenerator H) (hs := augmentationGenerator_mem_augmentationIdeal (H := H))]
simpa [augmentationGeneratorIdeal] using
congrArg (fun I : Ideal (GroupRing H) => (I : Submodule (GroupRing H) (GroupRing H)))
(augmentationGeneratorIdeal_eq_augmentationIdeal (H := H))
simpa [augmentationGeneratorSubtype] using hspanProof. 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 toAugmentationIdeal_surjective (ψ : G →* H) (hψ : Function.Surjective ψ) :
Function.Surjective (toAugmentationIdeal (H := H) ψ)The boundary factorization onto the augmentation ideal is surjective in the identity case.
Show proof
by
apply (LinearMap.range_eq_top).1
have hle :
Submodule.span (GroupRing H) (Set.range (augmentationGeneratorSubtype (H := H))) ≤
LinearMap.range (toAugmentationIdeal (H := H) ψ) := by
refine Submodule.span_le.2 ?_
rintro _ ⟨h, rfl⟩
rcases hψ h with ⟨g, rfl⟩
refine ⟨universalDifferential ψ g, ?_⟩
exact toAugmentationIdeal_d (H := H) ψ g
have htop : ⊤ ≤ LinearMap.range (toAugmentationIdeal (H := H) ψ) := by
simpa [span_augmentationGeneratorSubtype_eq_top (H := H)] using hle
exact eq_top_iff.mpr htopProof. 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 toGroupRing_id_injective :
Function.Injective (toGroupRing (MonoidHom.id H))The identity-case map from the differential module to the group ring is injective.
Show proof
identityCrossedDifferentialBoundary_injective (S := ℤ) (G := H)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.
□def augmentationIdealToIdentityDifferentialModule :
augmentationIdeal H →ₗ[GroupRing H] DifferentialModule (MonoidHom.id H) where
toFun x :=
monoidAlgebraToIdentityCrossedDifferentialModule (S := ℤ) (G := H) x.1
map_add' x y := by
change
monoidAlgebraToIdentityCrossedDifferentialModule (S := ℤ) (G := H) (x.1 + y.1) =
monoidAlgebraToIdentityCrossedDifferentialModule (S := ℤ) (G := H) x.1 +
monoidAlgebraToIdentityCrossedDifferentialModule (S := ℤ) (G := H) y.1
simp only [map_add]
map_smul' r x := by
change
monoidAlgebraToIdentityCrossedDifferentialModule (S := ℤ) (G := H) (r * x.1) =
r • monoidAlgebraToIdentityCrossedDifferentialModule (S := ℤ) (G := H) x.1
apply toGroupRing_id_injective (H := H)
have hxaug :
(MonoidAlgebra.lift ℤ ℤ H (1 : H →* ℤ)) x.1 = 0 :=
(mem_augmentationIdeal_iff (H := H)).1 x.2
have hrxaug :
(MonoidAlgebra.lift ℤ ℤ H (1 : H →* ℤ)) (r * x.1) = 0 := by
rw [map_mul, hxaug, mul_zero]
calc
toGroupRing (MonoidHom.id H)
(monoidAlgebraToIdentityCrossedDifferentialModule (S := ℤ) (G := H) (r * x.1)) =
r * x.1 := by
exact
idCrossedDiffBoundary_monoidAlgebraToModule_of_augmentation_eq_zero
(S := ℤ) (G := H) hrxaug
_ =
r * toGroupRing (MonoidHom.id H)
(monoidAlgebraToIdentityCrossedDifferentialModule (S := ℤ) (G := H) x.1) := by
exact congrArg (fun z => r * z)
(idCrossedDiffBoundary_monoidAlgebraToModule_of_augmentation_eq_zero
(S := ℤ) (G := H) hxaug).symm
_ =
toGroupRing (MonoidHom.id H)
(r • monoidAlgebraToIdentityCrossedDifferentialModule (S := ℤ) (G := H) x.1) := by
rw [map_smul]
rflThe inverse map from the augmentation ideal to the identity differential module, obtained by integrating an augmentation-zero group-ring element.
theorem toAugmentationIdeal_augmentationIdealToIdentityDifferentialModule
(x : augmentationIdeal H) :
toAugmentationIdeal (H := H) (MonoidHom.id H)
(augmentationIdealToIdentityDifferentialModule (H := H) x) = xComposing from the augmentation ideal to the identity differential module and back gives the original augmentation-ideal element.
Show proof
by
apply Subtype.ext
change
toGroupRing (MonoidHom.id H)
(monoidAlgebraToIdentityCrossedDifferentialModule (S := ℤ) (G := H) x.1) =
x.1
have hxaug :
(MonoidAlgebra.lift ℤ ℤ H (1 : H →* ℤ)) x.1 = 0 :=
(mem_augmentationIdeal_iff (H := H)).1 x.2
exact
idCrossedDiffBoundary_monoidAlgebraToModule_of_augmentation_eq_zero
(S := ℤ) (G := H) hxaugProof. Use the Fox boundary formula and the augmentation calculation. The boundary lands in the augmentation ideal because its augmentation is zero, and the identity-case comparison is checked on generators before extending by linearity and the universal property of the differential module.
□theorem augmentationIdealToIdentityDifferentialModule_toAugmentationIdeal
(x : DifferentialModule (MonoidHom.id H)) :
augmentationIdealToIdentityDifferentialModule (H := H)
(toAugmentationIdeal (H := H) (MonoidHom.id H) x) = xComposing from the identity differential module to the augmentation ideal and back gives the original differential-module element.
Show proof
by
apply toGroupRing_id_injective (H := H)
change
toGroupRing (MonoidHom.id H)
(monoidAlgebraToIdentityCrossedDifferentialModule (S := ℤ) (G := H)
(toGroupRing (MonoidHom.id H) x)) =
toGroupRing (MonoidHom.id H) x
have hxaug :
(MonoidAlgebra.lift ℤ ℤ H (1 : H →* ℤ))
(toGroupRing (MonoidHom.id H) x) = 0 :=
(mem_augmentationIdeal_iff (H := H)).1
(toGroupRing_mem_augmentationIdeal (H := H) (MonoidHom.id H) x)
exact
idCrossedDiffBoundary_monoidAlgebraToModule_of_augmentation_eq_zero
(S := ℤ) (G := H) hxaugProof. Use the Fox boundary formula and the augmentation calculation. The boundary lands in the augmentation ideal because its augmentation is zero, and the identity-case comparison is checked on generators before extending by linearity and the universal property of the differential module.
□def identityDifferentialModuleEquivAugmentationIdeal :
DifferentialModule (MonoidHom.id H) ≃ₗ[GroupRing H] augmentationIdeal H where
toLinearMap := toAugmentationIdeal (H := H) (MonoidHom.id H)
invFun := augmentationIdealToIdentityDifferentialModule (H := H)
left_inv := augmentationIdealToIdentityDifferentialModule_toAugmentationIdeal (H := H)
right_inv := toAugmentationIdeal_augmentationIdealToIdentityDifferentialModule (H := H)Universe-polymorphic identity case of the Crowell differential module: \(A_{\mathrm{id}}\) is the augmentation ideal of the integral group ring.
theorem identityDifferentialModuleEquivAugmentationIdeal_toLinearMap :
(identityDifferentialModuleEquivAugmentationIdeal (H := H)).toLinearMap =
toAugmentationIdeal (H := H) (MonoidHom.id H)The linear map underlying the equivalence from the identity differential module to the augmentation ideal is the canonical map to that augmentation ideal.
Show proof
rflProof. Use the Fox boundary formula and the augmentation calculation. The boundary lands in the augmentation ideal because its augmentation is zero, and the identity-case comparison is checked on generators before extending by linearity and the universal property of the differential module.
□