ProCGroups.FoxDifferential.Completed.FiniteStage.RelationSubmodule
The principal declarations in this module are:
foxAlgebraicStageRelationBoundarySubmoduleThe \((\mathbb{Z}/n\mathbb{Z})[F/N]\)-submodule generated by finite-stage relation-boundary vectors. -foxAlgebraicStageRelationBoundaryImageSubmoduleThe actual relation-boundary image as a finite group-algebra submodule. -foxAlgebraicStageRelationBoundaryRange_subset_relationBoundarySubmoduleEvery actual relation-boundary vector lies in the generated relation-boundary submodule. -foxAlgebraicStageRelationBoundaryAddMonoidHom_mem_relationBoundarySubmoduleA relation boundary of a finite-stage relation lies in the generated submodule.
def foxAlgebraicStageRelationBoundarySubmodule :
Submodule (foxAlgebraicStageTargetGroupAlgebra (X := X) N n)
(foxAlgebraicStageCoordinateVector (X := X) N n) :=
Submodule.span (foxAlgebraicStageTargetGroupAlgebra (X := X) N n)
(foxAlgebraicStageRelationBoundaryRange (X := X) N n :
Set (foxAlgebraicStageCoordinateVector (X := X) N n))The \((\mathbb{Z}/n\mathbb{Z})[F/N]\)-submodule generated by finite-stage relation-boundary vectors.
theorem foxAlgebraicStageRelationBoundaryRange_subset_relationBoundarySubmodule :
(foxAlgebraicStageRelationBoundaryRange (X := X) N n :
Set (foxAlgebraicStageCoordinateVector (X := X) N n)) ⊆
foxAlgebraicStageRelationBoundarySubmodule (X := X) N nEvery actual relation-boundary vector lies in the generated relation-boundary submodule.
Show Lean proof
by
exact Submodule.subset_spantheorem foxAlgebraicStageRelationBoundaryAddMonoidHom_mem_relationBoundarySubmodule
(q : Additive (foxAlgebraicStageRelationGroup (X := X) N n)) :
foxAlgebraicStageRelationBoundaryAddMonoidHom (X := X) N n q ∈
foxAlgebraicStageRelationBoundarySubmodule (X := X) N nA relation boundary of a finite-stage relation lies in the generated submodule.
Show Lean proof
by
apply foxAlgebraicStageRelationBoundaryRange_subset_relationBoundarySubmodule (X := X) N n
exact (mem_foxAlgebraicStageRelationBoundaryRange_iff
(X := X) (N := N) (n := n)).2 ⟨q, rfl⟩theorem foxAlgebraicStageRelationBoundaryRange_smul_mem
(a : foxAlgebraicStageTargetGroupAlgebra (X := X) N n)
{v : foxAlgebraicStageCoordinateVector (X := X) N n}
(hv : v ∈ foxAlgebraicStageRelationBoundaryRange (X := X) N n) :
a • v ∈ foxAlgebraicStageRelationBoundaryRange (X := X) N nThe actual relation-boundary image is stable under arbitrary finite group-algebra scalars.
Show Lean proof
by
classical
refine MonoidAlgebra.induction_linear
(M := foxAlgebraicStageTargetQuotient (X := X) N)
(R := ModNCompletedCoeff n)
(p := fun a : foxAlgebraicStageTargetGroupAlgebra (X := X) N n =>
a • v ∈ foxAlgebraicStageRelationBoundaryRange (X := X) N n)
a ?zero ?add ?single
· simp only [zero_smul, zero_mem]
· intro a b ha hb
rw [add_smul]
exact (foxAlgebraicStageRelationBoundaryRange (X := X) N n).add_mem ha hb
· intro h c
rcases ZMod.intCast_surjective c with ⟨m, rfl⟩
have hbase :
(MonoidAlgebra.of (ModNCompletedCoeff n)
(foxAlgebraicStageTargetQuotient (X := X) N) h) • v ∈
foxAlgebraicStageRelationBoundaryRange (X := X) N n :=
foxAlgebraicStageRelationBoundaryRange_basis_smul_mem (X := X) N n h hv
have hsingle :
((MonoidAlgebra.single h (m : ModNCompletedCoeff n) :
foxAlgebraicStageTargetGroupAlgebra (X := X) N n) • v :
foxAlgebraicStageCoordinateVector (X := X) N n) =
(m : ℤ) •
((MonoidAlgebra.of (ModNCompletedCoeff n)
(foxAlgebraicStageTargetQuotient (X := X) N) h) • v :
foxAlgebraicStageCoordinateVector (X := X) N n) := by
have hsingleAlg :
(MonoidAlgebra.single h (m : ModNCompletedCoeff n) :
foxAlgebraicStageTargetGroupAlgebra (X := X) N n) =
(m : ModNCompletedCoeff n) •
MonoidAlgebra.of (ModNCompletedCoeff n)
(foxAlgebraicStageTargetQuotient (X := X) N) h := by
exact (MonoidAlgebra.smul_of h (m : ModNCompletedCoeff n)).symm
rw [hsingleAlg]
rw [smul_assoc]
exact Int.cast_smul_eq_zsmul (ModNCompletedCoeff n) m
((MonoidAlgebra.of (ModNCompletedCoeff n)
(foxAlgebraicStageTargetQuotient (X := X) N) h) • v :
foxAlgebraicStageCoordinateVector (X := X) N n)
rw [hsingle]
exact (foxAlgebraicStageRelationBoundaryRange (X := X) N n).zsmul_mem hbase mdef foxAlgebraicStageRelationBoundaryImageSubmodule :
Submodule (foxAlgebraicStageTargetGroupAlgebra (X := X) N n)
(foxAlgebraicStageCoordinateVector (X := X) N n) where
carrier := foxAlgebraicStageRelationBoundaryRange (X := X) N n
zero_mem' := (foxAlgebraicStageRelationBoundaryRange (X := X) N n).zero_mem
add_mem' := by
intro x y hx hy
exact (foxAlgebraicStageRelationBoundaryRange (X := X) N n).add_mem hx hy
smul_mem' := by
intro a v hv
exact foxAlgebraicStageRelationBoundaryRange_smul_mem (X := X) N n a hvThe actual relation-boundary image as a finite group-algebra submodule.
@[simp]
theorem foxAlgebraicStageRelationBoundaryImageSubmodule_coe :
((foxAlgebraicStageRelationBoundaryImageSubmodule (X := X) N n :
Submodule (foxAlgebraicStageTargetGroupAlgebra (X := X) N n)
(foxAlgebraicStageCoordinateVector (X := X) N n)) :
Set (foxAlgebraicStageCoordinateVector (X := X) N n)) =
foxAlgebraicStageSourceKernelDerivativeSet (X := X) N nThe relation-boundary image submodule has the finite-stage source-kernel derivative set as its underlying set.
Show Lean proof
by
simp only [foxAlgebraicStageRelationBoundaryImageSubmodule,
foxAlgebraicStageRelationBoundaryRange_coe,
Submodule.coe_set_mk, AddSubmonoid.coe_set_mk, AddSubsemigroup.coe_set_mk]theorem foxAlgebraicStageRelationBoundarySubmodule_eq_imageSubmodule :
foxAlgebraicStageRelationBoundarySubmodule (X := X) N n =
foxAlgebraicStageRelationBoundaryImageSubmodule (X := X) N nThe generated relation-boundary submodule is the actual relation-boundary image, because the image is already stable under the finite target group algebra.
Show Lean proof
by
apply le_antisymm
· refine Submodule.span_le.2 ?_
intro v hv
exact hv
· intro v hv
exact foxAlgebraicStageRelationBoundaryRange_subset_relationBoundarySubmodule (X := X) N n hvtheorem foxAlgebraicStageRelationBoundarySubmodule_le_boundaryCycleSubmodule
[Fintype X] :
foxAlgebraicStageRelationBoundarySubmodule (X := X) N n ≤
foxAlgebraicStageBoundaryCycleSubmodule (X := X) N nThe relation-boundary submodule is contained in the finite Fox boundary cycles.
Show Lean proof
by
refine Submodule.span_le.2 ?_
intro v hv
exact foxAlgebraicStageRelationBoundary_range_le_boundaryCycleSubmodule (X := X) N n hvdef foxAlgebraicStageRelationBoundaryModuleExact [Fintype X] : Prop :=
foxAlgebraicStageBoundaryCycleSubmodule (X := X) N n ≤
foxAlgebraicStageRelationBoundarySubmodule (X := X) N nModule-level finite-stage exactness at the coordinate module: \(\ker\partial\) is contained in the submodule generated by finite relation boundaries.
theorem foxAlgebraicStageRelationBoundaryModuleExact_of_relationBoundaryExact
[Fintype X]
(hexact : foxAlgebraicStageRelationBoundaryExact (X := X) N n) :
foxAlgebraicStageRelationBoundaryModuleExact (X := X) N nFunction-level relation-boundary exactness implies the module-level finite exactness target.
Show Lean proof
by
intro v hv
have hcovered : foxAlgebraicStageBoundaryCyclesCoveredBySourceKernel (X := X) N n :=
foxAlgebraicStageBoundaryCyclesCoveredBySourceKernel_of_relationBoundaryExact
(X := X) N n hexact
have hvsource : v ∈ foxAlgebraicStageSourceKernelDerivativeSet (X := X) N n :=
hcovered hv
have hvrange : v ∈ foxAlgebraicStageRelationBoundaryRange (X := X) N n := by
change v ∈ foxAlgebraicStageSourceKernelDerivativeSet (X := X) N n
exact hvsource
exact foxAlgebraicStageRelationBoundaryRange_subset_relationBoundarySubmodule
(X := X) N n hvrange
Theorem
FoxDifferential.foxAlgebraicStageRelationBoundaryModuleExact_of_boundaryCyclesCoveredBySourceKernel
theorem foxAlgebraicStageRelationBoundaryModuleExact_of_boundaryCyclesCoveredBySourceKernel
[Fintype X]
(hcovered : foxAlgebraicStageBoundaryCyclesCoveredBySourceKernel (X := X) N n) :
foxAlgebraicStageRelationBoundaryModuleExact (X := X) N nThe set-level finite coverage target implies the module-level finite exactness target.
Show Lean proof
by
intro v hv
have hvsource : v ∈ foxAlgebraicStageSourceKernelDerivativeSet (X := X) N n := hcovered hv
have hvrange : v ∈ foxAlgebraicStageRelationBoundaryRange (X := X) N n := by
change v ∈ foxAlgebraicStageSourceKernelDerivativeSet (X := X) N n
exact hvsource
exact foxAlgebraicStageRelationBoundaryRange_subset_relationBoundarySubmodule
(X := X) N n hvrange
Theorem
FoxDifferential.foxAlgebraicStageBoundaryCyclesCoveredBySourceKernel_of_relationBoundaryModuleExact
theorem foxAlgebraicStageBoundaryCyclesCoveredBySourceKernel_of_relationBoundaryModuleExact
[Fintype X]
(hexact : foxAlgebraicStageRelationBoundaryModuleExact (X := X) N n) :
foxAlgebraicStageBoundaryCyclesCoveredBySourceKernel (X := X) N nModule-level finite exactness is strong enough to recover the set-level source-kernel coverage, because the relation-boundary image is already a finite group-algebra submodule.
Show Lean proof
by
intro v hv
have hvrel : v ∈ foxAlgebraicStageRelationBoundarySubmodule (X := X) N n := hexact hv
rw [foxAlgebraicStageRelationBoundarySubmodule_eq_imageSubmodule (X := X) N n] at hvrel
simpa [foxAlgebraicStageRelationBoundaryImageSubmodule] using hvrel
Theorem
FoxDifferential.foxAlgebraicStageRelationBoundaryModuleExact_iff_submodule_eq_boundaryCycleSubmodule
theorem foxAlgebraicStageRelationBoundaryModuleExact_iff_submodule_eq_boundaryCycleSubmodule
{N : Subgroup (FreeGroup X)} [N.Normal] {n : ℕ} [Fintype X] :
foxAlgebraicStageRelationBoundaryModuleExact (X := X) N n ↔
foxAlgebraicStageRelationBoundarySubmodule (X := X) N n =
foxAlgebraicStageBoundaryCycleSubmodule (X := X) N nModule exactness is equivalent to equality between \(\ker \partial\) and the generated relation-boundary submodule.
Show Lean proof
by
constructor
· intro hexact
exact le_antisymm
(foxAlgebraicStageRelationBoundarySubmodule_le_boundaryCycleSubmodule (X := X) N n)
hexact
· intro h v hv
rw [h]
exact hvtheorem relationBoundarySubmodule_eq_boundaryCycleSubmodule_of_relExact
[Fintype X]
(hexact : foxAlgebraicStageRelationBoundaryExact (X := X) N n) :
foxAlgebraicStageRelationBoundarySubmodule (X := X) N n =
foxAlgebraicStageBoundaryCycleSubmodule (X := X) N nFunction-level finite exactness identifies \(\ker \partial\) with the generated relation-boundary submodule.
Show Lean proof
(foxAlgebraicStageRelationBoundaryModuleExact_iff_submodule_eq_boundaryCycleSubmodule
(X := X) (N := N) (n := n)).1
(foxAlgebraicStageRelationBoundaryModuleExact_of_relationBoundaryExact
(X := X) N n hexact)