ProCGroups.FoxDifferential.Completed.FiniteStage.SourceBoundary
The principal declarations in this module are:
foxAlgebraicStageSourceCoordinateVectorSource-valued coordinate vectors over \((\mathbb{Z}/n\mathbb{Z})[F/([N,N]N^n)]\). -foxAlgebraicStageSourceFoxBoundaryThe source Fox boundary/Euler map \(a \mapsto \sum_i a_i([x_i]-1)\) over the source quotient. -foxAlgebraicStageSourceFoxBoundary_applyThe finite-stage source Fox boundary is evaluated on the canonical generators and then extended linearly to the finite-stage coordinate module. -foxAlgebraicStageCoordinateSourceToTarget_applyThe finite-stage source-to-target coordinate map is evaluated by applying the target quotient map to the chosen coordinate.
imports
abbrev foxAlgebraicStageSourceCoordinateVector : Type u :=
X → foxAlgebraicStageSourceGroupAlgebra (X := X) N nSource-valued coordinate vectors over \((\mathbb{Z}/n\mathbb{Z})[F/([N,N]N^n)]\).
def foxAlgebraicStageSourceFoxBoundary [Fintype X] :
foxAlgebraicStageSourceCoordinateVector (X := X) N n →ₗ[
foxAlgebraicStageSourceGroupAlgebra (X := X) N n]
foxAlgebraicStageSourceGroupAlgebra (X := X) N n where
toFun v :=
∑ i : X,
v i *
(MonoidAlgebra.of (ModNCompletedCoeff n)
(FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n)
(QuotientGroup.mk'
(foxCommutatorPowerSubgroup (F := FreeGroup X) N n)
(FreeGroup.of i)) - 1)
map_add' := by
intro v w
simp only [Pi.add_apply, QuotientGroup.mk'_apply, MonoidAlgebra.of_apply, add_mul,
Finset.sum_add_distrib]
map_smul' := by
intro r v
simp only [Pi.smul_apply, smul_eq_mul, QuotientGroup.mk'_apply, MonoidAlgebra.of_apply,
mul_assoc,
RingHom.id_apply, Finset.mul_sum]The source Fox boundary/Euler map \(a \mapsto \sum_i a_i([x_i]-1)\) over the source quotient.
omit [DecidableEq X] [N.Normal] in
@[simp]
theorem foxAlgebraicStageSourceFoxBoundary_apply [Fintype X]
(v : foxAlgebraicStageSourceCoordinateVector (X := X) N n) :
foxAlgebraicStageSourceFoxBoundary (X := X) N n v =
∑ i : X,
v i *
(MonoidAlgebra.of (ModNCompletedCoeff n)
(FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n)
(QuotientGroup.mk'
(foxCommutatorPowerSubgroup (F := FreeGroup X) N n)
(FreeGroup.of i)) - 1)The finite-stage source Fox boundary is evaluated on the canonical generators and then extended linearly to the finite-stage coordinate module.
Show Lean proof
rfldef foxAlgebraicStageCoordinateSourceToTarget :
foxAlgebraicStageSourceCoordinateVector (X := X) N n →ₗ[ModNCompletedCoeff n]
foxAlgebraicStageCoordinateVector (X := X) N n where
toFun v := fun i =>
foxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n (v i)
map_add' := by
intro v w
funext i
simp only [Pi.add_apply, map_add]
map_smul' := by
intro a v
funext i
simp only [Pi.smul_apply, foxCommutatorPowerGroupAlgebraMap_smul, RingHom.id_apply]Apply the finite source-to-target group-algebra map coordinatewise.
omit [DecidableEq X] in
@[simp]
theorem foxAlgebraicStageCoordinateSourceToTarget_apply
(v : foxAlgebraicStageSourceCoordinateVector (X := X) N n) (i : X) :
foxAlgebraicStageCoordinateSourceToTarget (X := X) N n v i =
foxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n (v i)The finite-stage source-to-target coordinate map is evaluated by applying the target quotient map to the chosen coordinate.
Show Lean proof
rflomit [DecidableEq X] in
theorem foxAlgebraicStageFoxBoundary_coordinateSourceToTarget
[Fintype X]
(v : foxAlgebraicStageSourceCoordinateVector (X := X) N n) :
foxAlgebraicStageFoxBoundary (X := X) N n
(foxAlgebraicStageCoordinateSourceToTarget (X := X) N n v) =
foxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n
(foxAlgebraicStageSourceFoxBoundary (X := X) N n v)The source boundary commutes with the source-to-target group-algebra map.
Show Lean proof
by
rw [foxAlgebraicStageFoxBoundary_apply, foxAlgebraicStageSourceFoxBoundary_apply]
rw [map_sum]
apply Finset.sum_congr rfl
intro i hi
rw [foxAlgebraicStageCoordinateSourceToTarget_apply, RingHom.map_mul, map_sub, map_one,
foxCommutatorPowerGroupAlgebraMap_of]omit [DecidableEq X] in
theorem foxAlgebraicStageCoordinateSourceToTarget_surjective :
Function.Surjective (foxAlgebraicStageCoordinateSourceToTarget (X := X) N n)The finite-stage coordinatewise source-to-target map is surjective.
Show Lean proof
by
intro v
have hcoord : ∀ i : X,
∃ a : foxAlgebraicStageSourceGroupAlgebra (X := X) N n,
foxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n a = v i := by
intro i
exact foxCommutatorPowerGroupAlgebraMap_surjective (X := X) N n (v i)
choose a ha using hcoord
refine ⟨a, ?_⟩
funext i
exact ha iomit [DecidableEq X] in
theorem foxAlgebraicStageSourceFoxBoundary_mem_groupAlgebraMapKernel_of_lift_cycle
[Fintype X]
{v : foxAlgebraicStageCoordinateVector (X := X) N n}
{a : foxAlgebraicStageSourceCoordinateVector (X := X) N n}
(ha : foxAlgebraicStageCoordinateSourceToTarget (X := X) N n a = v)
(hv : v ∈ foxAlgebraicStageBoundaryCycleSubmodule (X := X) N n) :
foxAlgebraicStageSourceFoxBoundary (X := X) N n a ∈
foxAlgebraicStageGroupAlgebraMapKernelIdeal (X := X) N nIf a source coordinate vector lifts a target boundary cycle, then its source boundary lies in the source-to-target group-algebra kernel.
Show Lean proof
by
rw [mem_foxAlgebraicStageGroupAlgebraMapKernelIdeal]
calc
foxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n
(foxAlgebraicStageSourceFoxBoundary (X := X) N n a) =
foxAlgebraicStageFoxBoundary (X := X) N n
(foxAlgebraicStageCoordinateSourceToTarget (X := X) N n a) := by
exact (foxAlgebraicStageFoxBoundary_coordinateSourceToTarget (X := X) N n a).symm
_ = foxAlgebraicStageFoxBoundary (X := X) N n v := by
rw [ha]
_ = 0 := hv
Theorem
FoxDifferential.foxAlgebraicStageSourceFoxBoundary_mem_relationAugmentationIdeal_of_lift_cycle
omit [DecidableEq X] in
theorem foxAlgebraicStageSourceFoxBoundary_mem_relationAugmentationIdeal_of_lift_cycle
[Fintype X]
{v : foxAlgebraicStageCoordinateVector (X := X) N n}
{a : foxAlgebraicStageSourceCoordinateVector (X := X) N n}
(ha : foxAlgebraicStageCoordinateSourceToTarget (X := X) N n a = v)
(hv : v ∈ foxAlgebraicStageBoundaryCycleSubmodule (X := X) N n) :
foxAlgebraicStageSourceFoxBoundary (X := X) N n a ∈
foxAlgebraicStageRelationAugmentationIdeal (X := X) N nIf a source coordinate vector lifts a target boundary cycle, then its source boundary lies in the explicit relation augmentation ideal.
Show Lean proof
by
rw [← foxAlgebraicStage_mem_groupAlgebraMapKernelIdeal_iff_relationAugmentationIdeal
(X := X) (N := N) (n := n)]
exact foxAlgebraicStageSourceFoxBoundary_mem_groupAlgebraMapKernel_of_lift_cycle
(X := X) N n ha hvomit [DecidableEq X] in
theorem exists_foxAlgebraicStageSourceCoordinate_lift_boundaryCycle_relationIdeal
[Fintype X]
(v : foxAlgebraicStageCoordinateVector (X := X) N n)
(hv : v ∈ foxAlgebraicStageBoundaryCycleSubmodule (X := X) N n) :
∃ a : foxAlgebraicStageSourceCoordinateVector (X := X) N n,
foxAlgebraicStageCoordinateSourceToTarget (X := X) N n a = v ∧
foxAlgebraicStageSourceFoxBoundary (X := X) N n a ∈
foxAlgebraicStageRelationAugmentationIdeal (X := X) N nEvery finite target boundary cycle has a source-coordinate lift whose source boundary is in the relation augmentation ideal.
Show Lean proof
by
rcases foxAlgebraicStageCoordinateSourceToTarget_surjective (X := X) N n v with ⟨a, ha⟩
exact ⟨a, ha,
foxAlgebraicStageSourceFoxBoundary_mem_relationAugmentationIdeal_of_lift_cycle
(X := X) N n ha hv⟩def foxAlgebraicStageSourceBoundaryRelationIdealReduction [Fintype X] : Prop :=
∀ a : foxAlgebraicStageSourceCoordinateVector (X := X) N n,
foxAlgebraicStageSourceFoxBoundary (X := X) N n a ∈
foxAlgebraicStageRelationAugmentationIdeal (X := X) N n →
foxAlgebraicStageCoordinateSourceToTarget (X := X) N n a ∈
foxAlgebraicStageRelationBoundarySubmodule (X := X) N nSource-boundary relation-ideal reduction: if every source coordinate vector whose source boundary lies in the relation augmentation ideal projects to a relation-boundary vector, then the finite-stage coordinate complex is exact.
theorem foxAlgebraicStageRelationBoundaryModuleExact_of_sourceBoundaryRelReduction
[Fintype X]
(hreduce : foxAlgebraicStageSourceBoundaryRelationIdealReduction (X := X) N n) :
foxAlgebraicStageRelationBoundaryModuleExact (X := X) N nThe source-boundary relation-ideal reduction implies finite-stage module exactness.
Show Lean proof
by
intro v hv
rcases exists_foxAlgebraicStageSourceCoordinate_lift_boundaryCycle_relationIdeal
(X := X) N n v hv with ⟨a, ha, hboundary⟩
have hrel := hreduce a hboundary
simpa [ha] using hreltheorem foxAlgebraicStageBoundaryCyclesCovered_of_sourceBoundaryRelReduction
[Fintype X]
(hreduce : foxAlgebraicStageSourceBoundaryRelationIdealReduction (X := X) N n) :
foxAlgebraicStageBoundaryCyclesCoveredBySourceKernel (X := X) N nThe source-boundary relation-ideal reduction implies finite-stage coordinate coverage.
Show Lean proof
foxAlgebraicStageBoundaryCyclesCoveredBySourceKernel_of_relationBoundaryModuleExact
(X := X) N n
(foxAlgebraicStageRelationBoundaryModuleExact_of_sourceBoundaryRelReduction
(X := X) N n hreduce)theorem foxAlgebraicStageBoundaryModuloRelations_inj_of_sourceBoundaryRelReduction
[Fintype X]
(hreduce : foxAlgebraicStageSourceBoundaryRelationIdealReduction (X := X) N n) :
Function.Injective (foxAlgebraicStageBoundaryModuloRelations (X := X) N n)The source-boundary relation-ideal reduction gives injectivity of the finite quotient obstruction boundary.
Show Lean proof
foxAlgebraicStageBoundaryModuloRelations_injective_of_relationBoundaryModuleExact
(X := X) N n
(foxAlgebraicStageRelationBoundaryModuleExact_of_sourceBoundaryRelReduction
(X := X) N n hreduce)theorem foxAlgebraicStageSemiBoundaryCyclesCovered_of_sourceBoundaryRelReduction
[Fintype X]
(hreduce : foxAlgebraicStageSourceBoundaryRelationIdealReduction (X := X) N n) :
foxAlgebraicStageSemidirectBoundaryCyclesCoveredBySourceKernel (X := X) N nThe source-boundary relation-ideal reduction gives the finite semidirect coverage statement.
Show Lean proof
(foxAlgebraicStageSemidirectBoundaryCyclesCoveredBySourceKernel_iff
(X := X) (N := N) (n := n)).2
(foxAlgebraicStageBoundaryCyclesCovered_of_sourceBoundaryRelReduction
(X := X) N n hreduce)