SourceBoundary.lean

abbrev foxAlgebraicStageSourceCoordinateVector : Type u

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]

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)

def 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]

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)

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)

theorem foxAlgebraicStageCoordinateSourceToTarget_surjective :
    Function.Surjective (foxAlgebraicStageCoordinateSourceToTarget (X := X) N n)

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 n

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 n

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 n

def foxAlgebraicStageSourceBoundaryRelationIdealReduction [Fintype X] : Prop

theorem foxAlgebraicStageRelationBoundaryModuleExact_of_sourceBoundaryRelReduction
    [Fintype X]
    (hreduce : foxAlgebraicStageSourceBoundaryRelationIdealReduction (X := X) N n) :
    foxAlgebraicStageRelationBoundaryModuleExact (X := X) N n

theorem foxAlgebraicStageBoundaryCyclesCovered_of_sourceBoundaryRelReduction
    [Fintype X]
    (hreduce : foxAlgebraicStageSourceBoundaryRelationIdealReduction (X := X) N n) :
    foxAlgebraicStageBoundaryCyclesCoveredBySourceKernel (X := X) N n

theorem foxAlgebraicStageBoundaryModuloRelations_inj_of_sourceBoundaryRelReduction
    [Fintype X]
    (hreduce : foxAlgebraicStageSourceBoundaryRelationIdealReduction (X := X) N n) :
    Function.Injective (foxAlgebraicStageBoundaryModuloRelations (X := X) N n)

theorem foxAlgebraicStageSemiBoundaryCyclesCovered_of_sourceBoundaryRelReduction
    [Fintype X]
    (hreduce : foxAlgebraicStageSourceBoundaryRelationIdealReduction (X := X) N n) :
    foxAlgebraicStageSemidirectBoundaryCyclesCoveredBySourceKernel (X := X) N n