FoxDifferential.Completed.ProCIntegerCoefficients.AugmentationIdeal.Basic
This module develops the augmentation side of the construction. It identifies the relevant kernels and ideals and compares the finite-stage and completed forms.
import
- FoxDifferential.Completed.ProCIntegerCoefficients.Core
- Mathlib.RingTheory.Ideal.Basic
def zcCompletedGroupAlgebraStandardAugmentationIdeal :
Ideal (ZCCompletedGroupAlgebra C H) :=
Ideal.span (Set.range fun h : H => zcGroupLike C H h - 1)The algebraic ideal generated by the standard completed augmentation generators \([h]-1\). The completed augmentation ideal itself is the kernel of the completed augmentation map, defined in the completed augmentation construction with \(\mathbb{Z}_C\)-coefficients.
theorem zcCompletedGroupAlgebraStandardAugmentationIdeal_eq_span :
((zcCompletedGroupAlgebraStandardAugmentationIdeal C H :
Ideal (ZCCompletedGroupAlgebra C H)) :
Submodule (ZCCompletedGroupAlgebra C H) (ZCCompletedGroupAlgebra C H)) =
Submodule.span (ZCCompletedGroupAlgebra C H)
(Set.range fun h : H => zcGroupLike C H h - 1)The standard completed augmentation-generator ideal, viewed as a submodule, is the submodule span of the standard generators.
Show proof
rflProof. Use the finite-stage augmentation maps of \(\mathbb{Z}_C\llbracket H\rrbracket\). The completed augmentation ideal is detected by all finite-stage projections: membership is equivalent to vanishing under every finite augmentation, and the standard generators \([h]-1\) project to the corresponding finite-stage generators. Closure, range, and inverse-limit statements follow from compatibility of finite-stage augmentation ideals under transition maps and from checking the formulas on group-like generators.
□theorem zcGroupLike_sub_one_mem_standardAugmentationIdeal (h : H) :
zcGroupLike C H h - 1 ∈ zcCompletedGroupAlgebraStandardAugmentationIdeal C HEach completed group-like generator \([h]-1\) lies in the algebraic standard augmentation-generator ideal.
Show proof
Ideal.subset_span (Set.mem_range_self h)Proof. Use the finite-stage augmentation maps of \(\mathbb{Z}_C\llbracket H\rrbracket\). The completed augmentation ideal is detected by all finite-stage projections: membership is equivalent to vanishing under every finite augmentation, and the standard generators \([h]-1\) project to the corresponding finite-stage generators. Closure, range, and inverse-limit statements follow from compatibility of finite-stage augmentation ideals under transition maps and from checking the formulas on group-like generators.
□theorem zcCompletedGroupAlgebraBoundary_mem_standardAugmentationIdeal
(ψ : G →* H) (g : G) :
zcCompletedGroupAlgebraBoundary C ψ g ∈
zcCompletedGroupAlgebraStandardAugmentationIdeal C HThe completed Fox boundary lies in the algebraic standard augmentation-generator ideal.
Show proof
by
simpa [zcCompletedGroupAlgebraBoundary] using
zcGroupLike_sub_one_mem_standardAugmentationIdeal C H (ψ g)Proof. Use the finite-stage augmentation maps of \(\mathbb{Z}_C\llbracket H\rrbracket\). The completed augmentation ideal is detected by all finite-stage projections: membership is equivalent to vanishing under every finite augmentation, and the standard generators \([h]-1\) project to the corresponding finite-stage generators. Closure, range, and inverse-limit statements follow from compatibility of finite-stage augmentation ideals under transition maps and from checking the formulas on group-like generators.
□def zcCompletedGroupAlgebraBoundaryToStandardAugmentationIdeal
(ψ : G →* H) (g : G) :
zcCompletedGroupAlgebraStandardAugmentationIdeal C H :=
⟨zcCompletedGroupAlgebraBoundary C ψ g,
zcCompletedGroupAlgebraBoundary_mem_standardAugmentationIdeal C H ψ g⟩The completed Fox boundary, with codomain restricted to the algebraic standard augmentation-generator ideal.
theorem zcCompletedGroupAlgebraBoundaryToStandardAugmentationIdeal_isCrossedDifferential
(ψ : G →* H) :
IsCrossedDifferential
(zcCompletedGroupAlgebraScalar C ψ)
(zcCompletedGroupAlgebraBoundaryToStandardAugmentationIdeal C H ψ)The standard-augmentation-ideal-valued completed Fox boundary is a crossed differential.
Show proof
by
intro g h
apply Subtype.ext
exact zcCompletedGroupAlgebraBoundary_mul C ψ g hProof. Use the finite-stage augmentation maps of \(\mathbb{Z}_C\llbracket H\rrbracket\). The completed augmentation ideal is detected by all finite-stage projections: membership is equivalent to vanishing under every finite augmentation, and the standard generators \([h]-1\) project to the corresponding finite-stage generators. Closure, range, and inverse-limit statements follow from compatibility of finite-stage augmentation ideals under transition maps and from checking the formulas on group-like generators.
□def zcToStdAugIdeal
(ψ : G →* H) :
ZCCompletedDifferentialModule C ψ →ₗ[ZCCompletedGroupAlgebra C H]
zcCompletedGroupAlgebraStandardAugmentationIdeal C H :=
zcCompletedDifferentialModuleLift
(A := zcCompletedGroupAlgebraStandardAugmentationIdeal C H) C ψ
(zcCompletedGroupAlgebraBoundaryToStandardAugmentationIdeal C H ψ)
(zcCompletedGroupAlgebraBoundaryToStandardAugmentationIdeal_isCrossedDifferential C H ψ)
@[simp]The completed Fox tail is restricted to the algebraic standard augmentation ideal as its codomain.
theorem zcToStdAugIdeal_val
(ψ : G →* H) (x : ZCCompletedDifferentialModule C ψ) :
((zcToStdAugIdeal C H ψ x :
ZCCompletedGroupAlgebra C H)) =
zcToCompletedGroupAlgebra C ψ xThe value of the standard-augmentation-ideal-valued completed Fox tail is the underlying completed group-algebra tail.
Show proof
by
let L := zcToStdAugIdeal C H ψ
have hL :
(zcCompletedGroupAlgebraStandardAugmentationIdeal C H).subtype.comp L =
zcToCompletedGroupAlgebra C ψ := by
apply zcCompletedDifferentialModuleHom_ext C ψ
intro g
simp only [zcToStdAugIdeal, LinearMap.coe_comp, Submodule.coe_subtype, Function.comp_apply,
zcCompletedDifferentialModuleLift_universal, zcCompletedGroupAlgebraBoundaryToStandardAugmentationIdeal,
zcToCompletedGroupAlgebra_universal, L]
simpa [L] using congrArg (fun f => f x) hLProof. Use the finite-stage augmentation maps of \(\mathbb{Z}_C\llbracket H\rrbracket\). The completed augmentation ideal is detected by all finite-stage projections: membership is equivalent to vanishing under every finite augmentation, and the standard generators \([h]-1\) project to the corresponding finite-stage generators. Closure, range, and inverse-limit statements follow from compatibility of finite-stage augmentation ideals under transition maps and from checking the formulas on group-like generators.
□theorem zcToCompletedGroupAlgebra_mem_standardAugmentationIdeal
(ψ : G →* H) (x : ZCCompletedDifferentialModule C ψ) :
zcToCompletedGroupAlgebra C ψ x ∈
zcCompletedGroupAlgebraStandardAugmentationIdeal C HThe completed Fox tail lands in the algebraic standard augmentation-generator ideal.
Show proof
by
simpa [zcToStdAugIdeal_val] using
(zcToStdAugIdeal C H ψ x).2Proof. Use the finite-stage augmentation maps of \(\mathbb{Z}_C\llbracket H\rrbracket\). The completed augmentation ideal is detected by all finite-stage projections: membership is equivalent to vanishing under every finite augmentation, and the standard generators \([h]-1\) project to the corresponding finite-stage generators. Closure, range, and inverse-limit statements follow from compatibility of finite-stage augmentation ideals under transition maps and from checking the formulas on group-like generators.
□theorem zcToCompletedGroupAlgebra_range_le_standardAugmentationIdeal
(ψ : G →* H) :
LinearMap.range (zcToCompletedGroupAlgebra C ψ) ≤
(zcCompletedGroupAlgebraStandardAugmentationIdeal C H :
Submodule (ZCCompletedGroupAlgebra C H) (ZCCompletedGroupAlgebra C H))The range of the completed Fox tail is contained in the algebraic standard augmentation-generator ideal.
Show proof
by
rintro x ⟨m, rfl⟩
exact zcToCompletedGroupAlgebra_mem_standardAugmentationIdeal C H ψ mProof. Use the finite-stage augmentation maps of \(\mathbb{Z}_C\llbracket H\rrbracket\). The completed augmentation ideal is detected by all finite-stage projections: membership is equivalent to vanishing under every finite augmentation, and the standard generators \([h]-1\) project to the corresponding finite-stage generators. Closure, range, and inverse-limit statements follow from compatibility of finite-stage augmentation ideals under transition maps and from checking the formulas on group-like generators.
□theorem zcToCompletedGroupAlgebra_range_eq_standardAugmentationIdeal_of_surjective
(ψ : G →* H) (hψ : Function.Surjective ψ) :
LinearMap.range (zcToCompletedGroupAlgebra C ψ) =
(zcCompletedGroupAlgebraStandardAugmentationIdeal C H :
Submodule (ZCCompletedGroupAlgebra C H) (ZCCompletedGroupAlgebra C H))If \(\psi\) is surjective, the completed Fox tail has range exactly the algebraic standard augmentation-generator ideal.
Show proof
by
refine le_antisymm
(zcToCompletedGroupAlgebra_range_le_standardAugmentationIdeal C H ψ) ?_
rw [zcCompletedGroupAlgebraStandardAugmentationIdeal_eq_span]
refine Submodule.span_le.2 ?_
rintro _ ⟨h, rfl⟩
rcases hψ h with ⟨g, rfl⟩
exact ⟨zcUniversalDifferential C ψ g, by simp only [zcToCompletedGroupAlgebra_universal, zcCompletedGroupAlgebraBoundary]⟩Proof. Use the finite-stage augmentation maps of \(\mathbb{Z}_C\llbracket H\rrbracket\). The completed augmentation ideal is detected by all finite-stage projections: membership is equivalent to vanishing under every finite augmentation, and the standard generators \([h]-1\) project to the corresponding finite-stage generators. Closure, range, and inverse-limit statements follow from compatibility of finite-stage augmentation ideals under transition maps and from checking the formulas on group-like generators.
□theorem zcToStdAugIdeal_surjective_of_surjective
(ψ : G →* H) (hψ : Function.Surjective ψ) :
Function.Surjective
(zcToStdAugIdeal C H ψ)If \(\psi\) is surjective, the standard-augmentation-ideal-valued completed Fox tail is surjective.
Show proof
by
intro y
have hy :
(y : ZCCompletedGroupAlgebra C H) ∈
LinearMap.range (zcToCompletedGroupAlgebra C ψ) := by
rw [zcToCompletedGroupAlgebra_range_eq_standardAugmentationIdeal_of_surjective
C H ψ hψ]
exact y.2
rcases hy with ⟨x, hx⟩
refine ⟨x, Subtype.ext ?_⟩
simpa [zcToStdAugIdeal_val] using hxProof. Use the finite-stage augmentation maps of \(\mathbb{Z}_C\llbracket H\rrbracket\). The completed augmentation ideal is detected by all finite-stage projections: membership is equivalent to vanishing under every finite augmentation, and the standard generators \([h]-1\) project to the corresponding finite-stage generators. Closure, range, and inverse-limit statements follow from compatibility of finite-stage augmentation ideals under transition maps and from checking the formulas on group-like generators.
□