ProCGroups.FoxDifferential.Completed.FiniteStage.RelationIdeal
The principal declarations in this module are:
foxAlgebraicStageRelationAugmentationGeneratorThe augmentation generator \(q-1\) attached to a finite-stage relation \(q \in \ker(F/[N,N]N^n \to F/N)\). -foxAlgebraicStageRelationAugmentationIdealThe source group-algebra ideal generated by finite-stage relation augmentation generators. -foxAlgebraicStageRelationAugmentationGenerator_mem_relationAugmentationIdealA finite-stage relation augmentation generator belongs to the relation augmentation ideal. -foxAlgebraicStageRelationAugmentationGenerator_mem_groupAlgebraMapKernelA relation augmentation generator maps to zero in the target group algebra.
imports
def foxAlgebraicStageRelationAugmentationGenerator
(q : foxAlgebraicStageRelationGroup (X := X) N n) :
foxAlgebraicStageSourceGroupAlgebra (X := X) N n :=
MonoidAlgebra.of (ModNCompletedCoeff n)
(FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n) q.1 - 1The augmentation generator \(q-1\) attached to a finite-stage relation \(q \in \ker(F/[N,N]N^n \to F/N)\).
def foxAlgebraicStageRelationAugmentationIdeal :
Ideal (foxAlgebraicStageSourceGroupAlgebra (X := X) N n) :=
Ideal.span
(Set.range (foxAlgebraicStageRelationAugmentationGenerator (X := X) N n))The source group-algebra ideal generated by finite-stage relation augmentation generators.
Theorem
FoxDifferential.foxAlgebraicStageRelationAugmentationGenerator_mem_relationAugmentationIdeal
omit [DecidableEq X] in
theorem foxAlgebraicStageRelationAugmentationGenerator_mem_relationAugmentationIdeal
(q : foxAlgebraicStageRelationGroup (X := X) N n) :
foxAlgebraicStageRelationAugmentationGenerator (X := X) N n q ∈
foxAlgebraicStageRelationAugmentationIdeal (X := X) N nA finite-stage relation augmentation generator belongs to the relation augmentation ideal.
Show Lean proof
by
exact Ideal.subset_span ⟨q, rfl⟩omit [DecidableEq X] in
theorem foxAlgebraicStageRelationAugmentationGenerator_mem_groupAlgebraMapKernel
(q : foxAlgebraicStageRelationGroup (X := X) N n) :
foxAlgebraicStageRelationAugmentationGenerator (X := X) N n q ∈
foxAlgebraicStageGroupAlgebraMapKernelIdeal (X := X) N nA relation augmentation generator maps to zero in the target group algebra.
Show Lean proof
by
rw [mem_foxAlgebraicStageGroupAlgebraMapKernelIdeal]
change foxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n
(MonoidAlgebra.of (ModNCompletedCoeff n)
(FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n) q.1 - 1) = 0
rw [map_sub, map_one, foxCommutatorPowerGroupAlgebraMap_of_quotient,
foxAlgebraicStageRelationGroup_target_eq_one]
rw [map_one, sub_self]omit [DecidableEq X] in
theorem foxAlgebraicStageRelationAugmentationIdeal_le_groupAlgebraMapKernel :
foxAlgebraicStageRelationAugmentationIdeal (X := X) N n ≤
foxAlgebraicStageGroupAlgebraMapKernelIdeal (X := X) N nThe generated relation augmentation ideal is contained in the kernel of the source-to-target finite group-algebra map.
Show Lean proof
by
refine Ideal.span_le.2 ?_
rintro x ⟨q, rfl⟩
exact foxAlgebraicStageRelationAugmentationGenerator_mem_groupAlgebraMapKernel (X := X) N n qdef foxAlgebraicStageTargetGroupAlgebraSection :
foxAlgebraicStageTargetGroupAlgebra (X := X) N n →ₗ[ModNCompletedCoeff n]
foxAlgebraicStageSourceGroupAlgebra (X := X) N n :=
(Finsupp.linearCombination (ModNCompletedCoeff n)
(fun h : foxAlgebraicStageTargetQuotient (X := X) N =>
MonoidAlgebra.of (ModNCompletedCoeff n)
(FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n)
(foxAlgebraicStageTargetQuotientLiftToSource (X := X) N n h))).comp
(MonoidAlgebra.coeffLinearEquiv (ModNCompletedCoeff n)).toLinearMapA section of the source-to-target finite group-algebra map, obtained by choosing a source quotient lift for each target quotient basis element. This is only a \(\mathbb{Z}/n\mathbb{Z}\)-linear section; no multiplicativity is asserted.
omit [DecidableEq X] in
@[simp]
theorem foxAlgebraicStageTargetGroupAlgebraSection_of
(h : foxAlgebraicStageTargetQuotient (X := X) N) :
foxAlgebraicStageTargetGroupAlgebraSection (X := X) N n
(MonoidAlgebra.of (ModNCompletedCoeff n)
(foxAlgebraicStageTargetQuotient (X := X) N) h) =
MonoidAlgebra.of (ModNCompletedCoeff n)
(FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n)
(foxAlgebraicStageTargetQuotientLiftToSource (X := X) N n h)The finite-stage target group-algebra section sends a group-like quotient element to the chosen lifted group-like element.
Show Lean proof
by
change
(Finsupp.linearCombination (ModNCompletedCoeff n)
(fun h : foxAlgebraicStageTargetQuotient (X := X) N =>
MonoidAlgebra.of (ModNCompletedCoeff n)
(FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n)
(foxAlgebraicStageTargetQuotientLiftToSource (X := X) N n h)))
(Finsupp.single h (1 : ModNCompletedCoeff n)) = _
rw [Finsupp.linearCombination_single, one_smul]omit [DecidableEq X] in
theorem foxCommutatorPowerGroupAlgebraMap_section
(y : foxAlgebraicStageTargetGroupAlgebra (X := X) N n) :
foxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n
(foxAlgebraicStageTargetGroupAlgebraSection (X := X) N n y) = yThe chosen group-algebra section is a right inverse to the finite source-to-target map.
Show Lean proof
by
classical
refine MonoidAlgebra.induction_on
(p := fun y : foxAlgebraicStageTargetGroupAlgebra (X := X) N n =>
foxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n
(foxAlgebraicStageTargetGroupAlgebraSection (X := X) N n y) = y)
y ?single ?add ?smul
· intro h
rw [foxAlgebraicStageTargetGroupAlgebraSection_of,
foxCommutatorPowerGroupAlgebraMap_of_quotient,
foxAlgebraicStageTargetQuotientLiftToSource_spec]
· intro x y hx hy
simp only [map_add, hx, hy]
· intro a x hx
rw [map_smul, foxCommutatorPowerGroupAlgebraMap_smul]
simp only [hx]omit [DecidableEq X] in
theorem foxCommutatorPowerGroupAlgebraMap_surjective :
Function.Surjective (foxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n)The finite source-to-target group-algebra map is surjective.
Show Lean proof
by
intro y
exact ⟨foxAlgebraicStageTargetGroupAlgebraSection (X := X) N n y,
foxCommutatorPowerGroupAlgebraMap_section (X := X) N n y⟩omit [DecidableEq X] in
theorem foxAlgebraicStage_sourceBasis_sub_section_mem_relationAugmentationIdeal
(s : FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n) :
MonoidAlgebra.of (ModNCompletedCoeff n)
(FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n) s -
foxAlgebraicStageTargetGroupAlgebraSection (X := X) N n
(foxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n
(MonoidAlgebra.of (ModNCompletedCoeff n)
(FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n) s)) ∈
foxAlgebraicStageRelationAugmentationIdeal (X := X) N nA source basis element minus the chosen lift of its target image lies in the finite-stage relation augmentation ideal.
Show Lean proof
by
let t : foxAlgebraicStageTargetQuotient (X := X) N :=
foxCommutatorPowerQuotientMapToNormalQuotient (F := FreeGroup X) N n s
let lift : FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n :=
foxAlgebraicStageTargetQuotientLiftToSource (X := X) N n t
let q : foxAlgebraicStageRelationGroup (X := X) N n :=
⟨lift⁻¹ * s, by
change foxCommutatorPowerQuotientMapToNormalQuotient (F := FreeGroup X) N n
(lift⁻¹ * s) = 1
rw [map_mul, map_inv]
have hlift :
foxCommutatorPowerQuotientMapToNormalQuotient (F := FreeGroup X) N n lift = t := by
simp only [foxAlgebraicStageTargetQuotientLiftToSource_spec, lift, t]
rw [hlift]
simp only [inv_mul_cancel, t]⟩
have hsection :
foxAlgebraicStageTargetGroupAlgebraSection (X := X) N n
(foxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n
(MonoidAlgebra.of (ModNCompletedCoeff n)
(FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n) s)) =
MonoidAlgebra.of (ModNCompletedCoeff n)
(FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n) lift := by
rw [foxCommutatorPowerGroupAlgebraMap_of_quotient,
foxAlgebraicStageTargetGroupAlgebraSection_of]
rw [hsection]
have hmul :
MonoidAlgebra.of (ModNCompletedCoeff n)
(FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n) lift *
foxAlgebraicStageRelationAugmentationGenerator (X := X) N n q =
MonoidAlgebra.of (ModNCompletedCoeff n)
(FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n) s -
MonoidAlgebra.of (ModNCompletedCoeff n)
(FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n) lift := by
simp only [foxAlgebraicStageRelationAugmentationGenerator, q, MonoidAlgebra.of_apply]
rw [mul_sub, MonoidAlgebra.single_mul_single, mul_one]
simp only [mul_inv_cancel_left, mul_one]
rw [← hmul]
exact (foxAlgebraicStageRelationAugmentationIdeal (X := X) N n).mul_mem_left _
(foxAlgebraicStageRelationAugmentationGenerator_mem_relationAugmentationIdeal (X := X) N n q)omit [DecidableEq X] in
theorem foxAlgebraicStage_sub_section_map_mem_relationAugmentationIdeal
(x : foxAlgebraicStageSourceGroupAlgebra (X := X) N n) :
x - foxAlgebraicStageTargetGroupAlgebraSection (X := X) N n
(foxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n x) ∈
foxAlgebraicStageRelationAugmentationIdeal (X := X) N nEvery finite-stage source group-algebra element minus the chosen lift of its target image lies in the relation augmentation ideal.
Show Lean proof
by
classical
refine MonoidAlgebra.induction_on
(p := fun x : foxAlgebraicStageSourceGroupAlgebra (X := X) N n =>
x - foxAlgebraicStageTargetGroupAlgebraSection (X := X) N n
(foxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n x) ∈
foxAlgebraicStageRelationAugmentationIdeal (X := X) N n)
x ?single ?add ?smul
· intro s
exact foxAlgebraicStage_sourceBasis_sub_section_mem_relationAugmentationIdeal (X := X) N n s
· intro x y hx hy
have hcalc :
x + y - foxAlgebraicStageTargetGroupAlgebraSection (X := X) N n
(foxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n (x + y)) =
(x - foxAlgebraicStageTargetGroupAlgebraSection (X := X) N n
(foxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n x)) +
(y - foxAlgebraicStageTargetGroupAlgebraSection (X := X) N n
(foxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n y)) := by
rw [map_add, map_add]
abel
rw [hcalc]
exact (foxAlgebraicStageRelationAugmentationIdeal (X := X) N n).add_mem hx hy
· intro a x hx
have hcalc :
a • x - foxAlgebraicStageTargetGroupAlgebraSection (X := X) N n
(foxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n (a • x)) =
a • (x - foxAlgebraicStageTargetGroupAlgebraSection (X := X) N n
(foxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n x)) := by
rw [foxCommutatorPowerGroupAlgebraMap_smul, map_smul, smul_sub]
rw [hcalc]
rw [Algebra.smul_def]
exact (foxAlgebraicStageRelationAugmentationIdeal (X := X) N n).mul_mem_left _ hxomit [DecidableEq X] in
theorem foxAlgebraicStageGroupAlgebraMapKernelIdeal_eq_relationAugmentationIdeal :
foxAlgebraicStageGroupAlgebraMapKernelIdeal (X := X) N n =
foxAlgebraicStageRelationAugmentationIdeal (X := X) N nThe kernel ideal of the finite source-to-target group-algebra map is exactly the ideal spanned by relation augmentation generators.
Show Lean proof
by
apply le_antisymm
· intro x hx
have hxmap :
foxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n x = 0 :=
(mem_foxAlgebraicStageGroupAlgebraMapKernelIdeal (X := X) (N := N) (n := n)).1 hx
have hdiff :=
foxAlgebraicStage_sub_section_map_mem_relationAugmentationIdeal (X := X) N n x
rw [hxmap, map_zero, sub_zero] at hdiff
exact hdiff
· exact foxAlgebraicStageRelationAugmentationIdeal_le_groupAlgebraMapKernel (X := X) N n
Theorem
FoxDifferential.foxAlgebraicStage_mem_groupAlgebraMapKernelIdeal_iff_relationAugmentationIdeal
omit [DecidableEq X] in
theorem foxAlgebraicStage_mem_groupAlgebraMapKernelIdeal_iff_relationAugmentationIdeal
{N : Subgroup (FreeGroup X)} [N.Normal] {n : ℕ}
{x : foxAlgebraicStageSourceGroupAlgebra (X := X) N n} :
x ∈ foxAlgebraicStageGroupAlgebraMapKernelIdeal (X := X) N n ↔
x ∈ foxAlgebraicStageRelationAugmentationIdeal (X := X) N nAt a finite Fox stage, membership in the source-to-target group-algebra map kernel ideal is equivalent to membership in the relation augmentation ideal.
Show Lean proof
by
rw [foxAlgebraicStageGroupAlgebraMapKernelIdeal_eq_relationAugmentationIdeal]