FoxDifferential.Completed.ProCIntegerCoefficients.Augmentation
This module sets up the finite-stage and inverse-limit description of the construction. It records the stage maps, projections, and comparison lemmas used to pass back to the completed object.
import
- FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.InClass.Augmentation
- FoxDifferential.Completed.ProCIntegerCoefficients.AugmentationIdeal.Basic
- Mathlib.Algebra.Exact
- Mathlib.RingTheory.Ideal.Maps
abbrev zcCompletedGroupAlgebraTopIndex : CompletedGroupAlgebraIndexInClass H C :=
OrderDual.toDual (OpenNormalSubgroupInClass.top (C := C) (G := H))The canonical trivial group quotient used to read the completed augmentation.
theorem zcCompletedGroupAlgebraTopIndex_le
(U : CompletedGroupAlgebraIndexInClass H C) :
zcCompletedGroupAlgebraTopIndex C H ≤ UThe canonical trivial quotient is below every finite quotient index.
Show proof
by
change ((OrderDual.ofDual U).1 : Subgroup H) ≤ (⊤ : Subgroup H)
exact le_topProof. Unfold the \(\mathbb{Z}_C\)-completed group algebra as an inverse limit over finite \(C\)-quotient and coefficient stages. Ring operations, projections, augmentation, topology, and group-like elements are computed coordinatewise at finite group-algebra stages. Compatibility of transition maps and inverse-limit extensionality assemble the completed algebraic and topological statements.
□def zcCompletedGroupAlgebraAugmentationFamily
(x : ZCCompletedGroupAlgebra C H) (i : ProCIntegerIndex C) :
ProCIntegerStage C i := by
letI : Fact (0 < i.modulus) := ⟨i.positive⟩
exact
modNCompletedGroupAlgebraStageAugmentationInClass i.modulus H C
(zcCompletedGroupAlgebraTopIndex C H)
(zcCompletedGroupAlgebraProjection C H
(i, zcCompletedGroupAlgebraTopIndex C H) x)The finite coefficient coordinate of the completed augmentation \(\mathbb{Z}_C\llbracket H\rrbracket \to \mathbb{Z}_C\).
theorem zcCompletedGroupAlgebraAugmentationFamily_compatible
(x : ZCCompletedGroupAlgebra C H) {i j : ProCIntegerIndex C} (hij : i ≤ j) :
proCIntegerTransition (C := C) hij
(zcCompletedGroupAlgebraAugmentationFamily C H x j) =
zcCompletedGroupAlgebraAugmentationFamily C H x iThe finite coefficient coordinates of the completed augmentation are compatible.
Show proof
by
letI : Fact (0 < i.modulus) := ⟨i.positive⟩
letI : Fact (0 < j.modulus) := ⟨j.positive⟩
let U := zcCompletedGroupAlgebraTopIndex C H
have hx := x.2 (i, U) (j, U) ⟨hij, le_rfl⟩
dsimp [zcCompletedGroupAlgebraAugmentationFamily]
change
modNCompletedCoeffMap (n := i.modulus) (m := j.modulus) hij
((modNCompletedGroupAlgebraStageAugmentationInClass j.modulus H C U)
(x.1 (j, U))) =
(modNCompletedGroupAlgebraStageAugmentationInClass i.modulus H C U)
(x.1 (i, U))
rw [← hx]
simp only [zcCompletedGroupAlgebraTransition, RingHom.comp_apply,
modNCompletedGroupAlgebraTransitionInClass_id, RingHom.id_apply]
change
modNCompletedCoeffMap (n := i.modulus) (m := j.modulus) hij
((modNCompletedGroupAlgebraStageAugmentationInClass j.modulus H C U)
(x.1 (j, U))) =
(modNCompletedGroupAlgebraStageAugmentationInClass i.modulus H C U)
((modNCompletedGroupAlgebraStageCoeffMapInClass
(n := i.modulus) (m := j.modulus) (G := H) C U hij)
(x.1 (j, U)))
exact
(congrFun
(congrArg DFunLike.coe
(modNCompletedGroupAlgebraStageAugmentationInClass_comp_stageCoeffMap
(n := i.modulus) (G := H) C U (m := j.modulus) hij))
(x.1 (j, U))).symmProof. Unfold the \(\mathbb{Z}_C\)-completed group algebra as an inverse limit over finite \(C\)-quotient and coefficient stages. Ring operations, projections, augmentation, topology, and group-like elements are computed coordinatewise at finite group-algebra stages. Compatibility of transition maps and inverse-limit extensionality assemble the completed algebraic and topological statements.
□def zcCompletedGroupAlgebraAugmentation :
ZCCompletedGroupAlgebra C H →+* ZCCoeff C where
toFun x :=
Subtype.mk
(zcCompletedGroupAlgebraAugmentationFamily C H x)
(by
intro i j hij
exact zcCompletedGroupAlgebraAugmentationFamily_compatible C H x hij)
map_zero' := by
ext i
change zcCompletedGroupAlgebraAugmentationFamily C H
(0 : ZCCompletedGroupAlgebra C H) i = 0
simp only [zcCompletedGroupAlgebraAugmentationFamily, zcCompletedGroupAlgebraProjection_zero, map_zero]
map_one' := by
ext i
change zcCompletedGroupAlgebraAugmentationFamily C H
(1 : ZCCompletedGroupAlgebra C H) i = 1
simp only [zcCompletedGroupAlgebraAugmentationFamily, zcCompletedGroupAlgebraProjection_one, map_one]
map_add' x y := by
ext i
change zcCompletedGroupAlgebraAugmentationFamily C H (x + y) i =
zcCompletedGroupAlgebraAugmentationFamily C H x i +
zcCompletedGroupAlgebraAugmentationFamily C H y i
simp only [zcCompletedGroupAlgebraAugmentationFamily, zcCompletedGroupAlgebraProjection_add, map_add]
map_mul' x y := by
ext i
change zcCompletedGroupAlgebraAugmentationFamily C H (x * y) i =
zcCompletedGroupAlgebraAugmentationFamily C H x i *
zcCompletedGroupAlgebraAugmentationFamily C H y i
simp only [zcCompletedGroupAlgebraAugmentationFamily, zcCompletedGroupAlgebraProjection_mul, map_mul]The completed augmentation \(\mathbb{Z}_C\llbracket H\rrbracket \to \mathbb{Z}_C\), obtained by augmenting every finite stage \((\mathbb{Z}/n\mathbb{Z})[H/U]\) at the canonical trivial quotient of \(H\).
theorem proCIntegerProj_zcCompletedGroupAlgebraAugmentation
(i : ProCIntegerIndex C) (x : ZCCompletedGroupAlgebra C H) :
proCIntegerProj (C := C) i (zcCompletedGroupAlgebraAugmentation C H x) =
zcCompletedGroupAlgebraAugmentationFamily C H x iProjecting the completed augmentation gives the corresponding finite-stage augmentation.
Show proof
rflProof. Unfold the \(\mathbb{Z}_C\)-completed group algebra as an inverse limit over finite \(C\)-quotient and coefficient stages. Ring operations, projections, augmentation, topology, and group-like elements are computed coordinatewise at finite group-algebra stages. Compatibility of transition maps and inverse-limit extensionality assemble the completed algebraic and topological statements.
□theorem proCIntegerProj_zcCompletedGroupAlgebraAugmentation_eq_stage
(i : ZCCompletedGroupAlgebraIndex C H) (x : ZCCompletedGroupAlgebra C H) :
proCIntegerProj (C := C) i.1 (zcCompletedGroupAlgebraAugmentation C H x) =
modNCompletedGroupAlgebraStageAugmentationInClass i.1.modulus H C i.2
(zcCompletedGroupAlgebraProjection C H i x)The completed augmentation can be read after projecting to any finite group quotient stage, not only the canonical trivial quotient used in its definition.
Show proof
by
let T := zcCompletedGroupAlgebraTopIndex C H
letI : Fact (0 < i.1.modulus) := ⟨i.1.positive⟩
have hT : T ≤ i.2 := zcCompletedGroupAlgebraTopIndex_le C H i.2
have hx := x.2 (i.1, T) i ⟨le_rfl, hT⟩
dsimp [zcCompletedGroupAlgebraAugmentationFamily]
change
(modNCompletedGroupAlgebraStageAugmentationInClass i.1.modulus H C T) (x.1 (i.1, T)) =
(modNCompletedGroupAlgebraStageAugmentationInClass i.1.modulus H C i.2) (x.1 i)
rw [← hx]
simp only [zcCompletedGroupAlgebraTransition, RingHom.comp_apply,
modNCompletedGroupAlgebraStageCoeffMapInClass_rfl, RingHom.id_apply]
exact congrFun
(congrArg DFunLike.coe
(modNCompletedGroupAlgebraStageAugmentationInClass_compatible
(n := i.1.modulus) (G := H) C hT)) (x.1 i)Proof. Unfold the \(\mathbb{Z}_C\)-completed group algebra as an inverse limit over finite \(C\)-quotient and coefficient stages. Ring operations, projections, augmentation, topology, and group-like elements are computed coordinatewise at finite group-algebra stages. Compatibility of transition maps and inverse-limit extensionality assemble the completed algebraic and topological statements.
□theorem zcCompletedGroupAlgebraAugmentation_groupLike (h : H) :
zcCompletedGroupAlgebraAugmentation C H (zcGroupLike C H h) = 1The completed augmentation sends every group-like element to \(1\).
Show proof
by
ext i
simp only [proCIntegerProj_zcCompletedGroupAlgebraAugmentation, zcCompletedGroupAlgebraAugmentationFamily,
zcCompletedGroupAlgebraProjection_groupLike, OrderDual.ofDual_toDual, MonoidAlgebra.of_apply,
modNCompletedGroupAlgebraStageAugmentationInClass_single, proCIntegerProj_one]Proof. Unfold the \(\mathbb{Z}_C\)-completed group algebra as an inverse limit over finite \(C\)-quotient and coefficient stages. Ring operations, projections, augmentation, topology, and group-like elements are computed coordinatewise at finite group-algebra stages. Compatibility of transition maps and inverse-limit extensionality assemble the completed algebraic and topological statements.
□theorem zcCompletedGroupAlgebraAugmentation_boundary
{G : Type u} [Group G] (ψ : G →* H) (g : G) :
zcCompletedGroupAlgebraAugmentation C H
(zcCompletedGroupAlgebraBoundary C ψ g) = 0The completed Fox boundary has augmentation zero.
Show proof
by
simp only [zcCompletedGroupAlgebraBoundary, map_sub, zcCompletedGroupAlgebraAugmentation_groupLike, map_one,
sub_self]Proof. Unfold the \(\mathbb{Z}_C\)-completed group algebra as an inverse limit over finite \(C\)-quotient and coefficient stages. Ring operations, projections, augmentation, topology, and group-like elements are computed coordinatewise at finite group-algebra stages. Compatibility of transition maps and inverse-limit extensionality assemble the completed algebraic and topological statements.
□def zcCompletedGroupAlgebraAugmentationIdeal :
Ideal (ZCCompletedGroupAlgebra C H) :=
RingHom.ker (zcCompletedGroupAlgebraAugmentation C H)The completed augmentation ideal, defined as the kernel of \(\mathbb{Z}_C\llbracket H\rrbracket \to \mathbb{Z}_C\).
abbrev ZCCompletedGroupAlgebraAugmentationIdeal : Type u :=
zcCompletedGroupAlgebraAugmentationIdeal C H
@[simp]The completed augmentation ideal is bundled as a subtype.
theorem mem_zcCompletedGroupAlgebraAugmentationIdeal_iff
{x : ZCCompletedGroupAlgebra C H} :
x ∈ zcCompletedGroupAlgebraAugmentationIdeal C H ↔
zcCompletedGroupAlgebraAugmentation C H x = 0A completed integer group-algebra element lies in the completed augmentation ideal iff the completed augmentation sends it to zero.
Show proof
by
rw [zcCompletedGroupAlgebraAugmentationIdeal, RingHom.mem_ker]Proof. Unfold the \(\mathbb{Z}_C\)-completed group algebra as an inverse limit over finite \(C\)-quotient and coefficient stages. Ring operations, projections, augmentation, topology, and group-like elements are computed coordinatewise at finite group-algebra stages. Compatibility of transition maps and inverse-limit extensionality assemble the completed algebraic and topological statements.
□theorem zcCompletedGroupAlgebraStandardAugmentationIdeal_le_augmentationIdeal :
zcCompletedGroupAlgebraStandardAugmentationIdeal C H ≤
zcCompletedGroupAlgebraAugmentationIdeal C HThe algebraic standard-generator ideal is contained in the completed augmentation ideal.
Show proof
by
rw [zcCompletedGroupAlgebraStandardAugmentationIdeal]
refine Ideal.span_le.2 ?_
rintro x ⟨h, rfl⟩
change zcGroupLike C H h - 1 ∈ zcCompletedGroupAlgebraAugmentationIdeal C H
rw [mem_zcCompletedGroupAlgebraAugmentationIdeal_iff]
simp only [map_sub, zcCompletedGroupAlgebraAugmentation_groupLike, map_one, sub_self]Proof. Unfold the \(\mathbb{Z}_C\)-completed group algebra as an inverse limit over finite \(C\)-quotient and coefficient stages. Ring operations, projections, augmentation, topology, and group-like elements are computed coordinatewise at finite group-algebra stages. Compatibility of transition maps and inverse-limit extensionality assemble the completed algebraic and topological statements.
□theorem zcCompletedGroupAlgebraBoundary_mem_augmentationIdeal
{G : Type u} [Group G] (ψ : G →* H) (g : G) :
zcCompletedGroupAlgebraBoundary C ψ g ∈
zcCompletedGroupAlgebraAugmentationIdeal C HThe completed Fox boundary lies in the completed augmentation ideal.
Show proof
by
rw [mem_zcCompletedGroupAlgebraAugmentationIdeal_iff]
simp only [zcCompletedGroupAlgebraAugmentation_boundary]Proof. Unfold the \(\mathbb{Z}_C\)-completed group algebra as an inverse limit over finite \(C\)-quotient and coefficient stages. Ring operations, projections, augmentation, topology, and group-like elements are computed coordinatewise at finite group-algebra stages. Compatibility of transition maps and inverse-limit extensionality assemble the completed algebraic and topological statements.
□theorem exact_zcToCompletedGA_of_surj_of_standardAugmentationIdeal_eq_augmentationIdeal
{G : Type u} [Group G] (ψ : G →* H) (hψ : Function.Surjective ψ)
(hstandard :
zcCompletedGroupAlgebraStandardAugmentationIdeal C H =
zcCompletedGroupAlgebraAugmentationIdeal C H) :
Function.Exact
(zcToCompletedGroupAlgebra C ψ :
ZCCompletedDifferentialModule C ψ → ZCCompletedGroupAlgebra C H)
(zcCompletedGroupAlgebraAugmentation C H :
ZCCompletedGroupAlgebra C H → ZCCoeff C)If the completed augmentation kernel is the algebraic standard-generator ideal, then a surjective completed Fox boundary gives exactness at \(\mathbb{Z}_C\llbracket H\rrbracket\).
Show proof
by
intro z
constructor
· intro hz
have hzmem :
z ∈ zcCompletedGroupAlgebraStandardAugmentationIdeal C H := by
rw [hstandard]
exact (mem_zcCompletedGroupAlgebraAugmentationIdeal_iff
(C := C) (H := H) (x := z)).2 hz
have hzrange :
z ∈ LinearMap.range (zcToCompletedGroupAlgebra C ψ) := by
rw [zcToCompletedGroupAlgebra_range_eq_standardAugmentationIdeal_of_surjective
C H ψ hψ]
exact hzmem
exact hzrange
· rintro ⟨m, rfl⟩
have hmem :
zcToCompletedGroupAlgebra C ψ m ∈
zcCompletedGroupAlgebraAugmentationIdeal C H :=
zcCompletedGroupAlgebraStandardAugmentationIdeal_le_augmentationIdeal C H
(zcToCompletedGroupAlgebra_mem_standardAugmentationIdeal C H ψ m)
exact (mem_zcCompletedGroupAlgebraAugmentationIdeal_iff
(C := C) (H := H) (x := zcToCompletedGroupAlgebra C ψ m)).1 hmemProof. Unfold the \(\mathbb{Z}_C\)-completed group algebra as an inverse limit over finite \(C\)-quotient and coefficient stages. Ring operations, projections, augmentation, topology, and group-like elements are computed coordinatewise at finite group-algebra stages. Compatibility of transition maps and inverse-limit extensionality assemble the completed algebraic and topological statements.
□theorem exact_zcToCompletedGA_iff_standardAugmentationIdeal_eq_augmentationIdeal_of_surj
{G : Type u} [Group G] (ψ : G →* H) (hψ : Function.Surjective ψ) :
Function.Exact
(zcToCompletedGroupAlgebra C ψ :
ZCCompletedDifferentialModule C ψ → ZCCompletedGroupAlgebra C H)
(zcCompletedGroupAlgebraAugmentation C H :
ZCCompletedGroupAlgebra C H → ZCCoeff C) ↔
zcCompletedGroupAlgebraStandardAugmentationIdeal C H =
zcCompletedGroupAlgebraAugmentationIdeal C HFor a surjective coefficient group map, exactness of the algebraic completed Fox tail is equivalent to the algebraic standard-generator ideal already being the completed augmentation ideal. This isolates the closed-range obstruction for infinite completed group algebras.
Show proof
by
constructor
· intro hexact
apply le_antisymm
· exact zcCompletedGroupAlgebraStandardAugmentationIdeal_le_augmentationIdeal C H
· intro z hz
have hz0 :
zcCompletedGroupAlgebraAugmentation C H z = 0 :=
(mem_zcCompletedGroupAlgebraAugmentationIdeal_iff
(C := C) (H := H) (x := z)).1 hz
rcases (hexact z).1 hz0 with ⟨m, hm⟩
have hzrange :
z ∈ LinearMap.range (zcToCompletedGroupAlgebra C ψ) := ⟨m, hm⟩
rwa [zcToCompletedGroupAlgebra_range_eq_standardAugmentationIdeal_of_surjective
C H ψ hψ] at hzrange
· intro hstandard
exact
exact_zcToCompletedGA_of_surj_of_standardAugmentationIdeal_eq_augmentationIdeal
C H ψ hψ hstandardProof. Unfold the \(\mathbb{Z}_C\)-completed group algebra as an inverse limit over finite \(C\)-quotient and coefficient stages. Ring operations, projections, augmentation, topology, and group-like elements are computed coordinatewise at finite group-algebra stages. Compatibility of transition maps and inverse-limit extensionality assemble the completed algebraic and topological statements.
□theorem zcCompletedGroupAlgebraAugmentation_surjective :
Function.Surjective (zcCompletedGroupAlgebraAugmentation C H)The completed augmentation \(\mathbb{Z}_C\llbracket H\rrbracket \to \mathbb{Z}_C\) is surjective.
Show proof
by
intro a
refine ⟨⟨fun i => ?_, ?_⟩, ?_⟩
· letI : Fact (0 < i.1.modulus) := ⟨i.1.positive⟩
exact MonoidAlgebra.single
(1 : CompletedGroupAlgebraQuotientInClass H C i.2)
(proCIntegerProj (C := C) i.1 a)
· intro i j hij
letI : Fact (0 < i.1.modulus) := ⟨i.1.positive⟩
letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
change zcCompletedGroupAlgebraTransition C H hij
(MonoidAlgebra.single
(1 : CompletedGroupAlgebraQuotientInClass H C j.2)
(proCIntegerProj (C := C) j.1 a)) =
MonoidAlgebra.single
(1 : CompletedGroupAlgebraQuotientInClass H C i.2)
(proCIntegerProj (C := C) i.1 a)
rw [zcCompletedGroupAlgebraTransition_single]
have ha :
modNCompletedCoeffMap (n := i.1.modulus) (m := j.1.modulus) hij.1
(proCIntegerProj (C := C) j.1 a) =
proCIntegerProj (C := C) i.1 a :=
proCIntegerProj_transition (C := C) hij.1 a
simpa using congrArg
(fun b : ProCIntegerStage C i.1 =>
MonoidAlgebra.single
(1 : CompletedGroupAlgebraQuotientInClass H C i.2) b)
ha
· ext i
let T := zcCompletedGroupAlgebraTopIndex C H
letI : Fact (0 < i.modulus) := ⟨i.positive⟩
change
(modNCompletedGroupAlgebraStageAugmentationInClass i.modulus H C T)
(MonoidAlgebra.single
(1 : CompletedGroupAlgebraQuotientInClass H C T)
(proCIntegerProj (C := C) i a)) =
proCIntegerProj (C := C) i a
simp only [modNCompletedGroupAlgebraStageAugmentationInClass_single]Proof. Unfold the \(\mathbb{Z}_C\)-completed group algebra as an inverse limit over finite \(C\)-quotient and coefficient stages. Ring operations, projections, augmentation, topology, and group-like elements are computed coordinatewise at finite group-algebra stages. Compatibility of transition maps and inverse-limit extensionality assemble the completed algebraic and topological statements.
□