ProCGroups.FoxDifferential.Completed.FiniteStage.BoundarySubgroups

5 Theorems | 2 Definitions

The principal declarations in this module are:

foxAlgebraicStageSemidirectBoundaryCycleSubgroup Finite semidirect boundary cycles form a subgroup. - foxAlgebraicStageSemidirectSourceKernelDerivativeSubgroup Finite source-kernel derivative semidirect points form a subgroup. - foxAlgebraicStageSemidirectBoundaryCycleSubgroup_coe The boundary-cycle subgroup of the finite Fox semidirect product has the boundary-cycle set as its underlying set. - foxAlgebraicStageSemidirectSourceKernelDerivativeSet_iff Source-kernel semidirect points are exactly points with right component \(1\) and left component in the source-kernel derivative subgroup.

import

ProCGroups.FoxDifferential.Completed.FiniteStage.SemidirectCycles

Imported by

Definition FoxDifferential.foxAlgebraicStageSemidirectBoundaryCycleSubgroup

def foxAlgebraicStageSemidirectBoundaryCycleSubgroup [Fintype X] :
    Subgroup (FoxAlgebraicStageSemidirect (X := X) N n) where
  carrier := foxAlgebraicStageSemidirectBoundaryCycleSet (X := X) N n
  one_mem' := by
    constructor
    · simp only [FoxAlgebraicStageSemidirect.one_right]
    · exact (foxAlgebraicStageBoundaryCycleSubmodule (X := X) N n).zero_mem
  mul_mem' := by
    intro y z hy hz
    rcases hy with ⟨hyright, hyleft⟩
    rcases hz with ⟨hzright, hzleft⟩
    constructor
    · simp only [FoxAlgebraicStageSemidirect.mul_right, hyright, hzright, mul_one]
    · rw [FoxAlgebraicStageSemidirect.mul_left, hyright]
      have hone :
          (MonoidAlgebra.of (ModNCompletedCoeff n)
            (foxAlgebraicStageTargetQuotient (X := X) N) 1 :
              foxAlgebraicStageTargetGroupAlgebra (X := X) N n) = 1 := by
        exact map_one
          (MonoidAlgebra.of (ModNCompletedCoeff n)
            (foxAlgebraicStageTargetQuotient (X := X) N))
      rw [hone, one_smul]
      exact (foxAlgebraicStageBoundaryCycleSubmodule (X := X) N n).add_mem hyleft hzleft
  inv_mem' := by
    intro y hy
    rcases hy with ⟨hyright, hyleft⟩
    constructor
    · simp only [FoxAlgebraicStageSemidirect.inv_right, hyright, inv_one]
    · rw [FoxAlgebraicStageSemidirect.inv_left, hyright, inv_one]
      have hone :
          (MonoidAlgebra.of (ModNCompletedCoeff n)
            (foxAlgebraicStageTargetQuotient (X := X) N) 1 :
              foxAlgebraicStageTargetGroupAlgebra (X := X) N n) = 1 := by
        exact map_one
          (MonoidAlgebra.of (ModNCompletedCoeff n)
            (foxAlgebraicStageTargetQuotient (X := X) N))
      rw [hone, one_smul]
      exact (foxAlgebraicStageBoundaryCycleSubmodule (X := X) N n).neg_mem hyleft

Finite semidirect boundary cycles form a subgroup.

Theorem FoxDifferential.foxAlgebraicStageSemidirectBoundaryCycleSubgroup_coe

omit [DecidableEq X] in
@[simp]
theorem foxAlgebraicStageSemidirectBoundaryCycleSubgroup_coe [Fintype X] :
    ((foxAlgebraicStageSemidirectBoundaryCycleSubgroup (X := X) N n :
        Subgroup (FoxAlgebraicStageSemidirect (X := X) N n)) :
          Set (FoxAlgebraicStageSemidirect (X := X) N n)) =
      foxAlgebraicStageSemidirectBoundaryCycleSet (X := X) N n

The boundary-cycle subgroup of the finite Fox semidirect product has the boundary-cycle set as its underlying set.

Show Lean proof

Theorem FoxDifferential.foxAlgebraicStageSemidirectSourceKernelDerivativeSet_iff

theorem foxAlgebraicStageSemidirectSourceKernelDerivativeSet_iff
    {N : Subgroup (FreeGroup X)} [N.Normal] {n : ℕ}
    {y : FoxAlgebraicStageSemidirect (X := X) N n} :
    y ∈ foxAlgebraicStageSemidirectSourceKernelDerivativeSet (X := X) N n ↔
      y.right = 1 ∧
        y.left ∈ foxAlgebraicStageSourceKernelDerivativeSet (X := X) N n

Source-kernel semidirect points are exactly points with right component \(1\) and left component in the source-kernel derivative subgroup.

Show Lean proof

Definition FoxDifferential.foxAlgebraicStageSemidirectSourceKernelDerivativeSubgroup

def foxAlgebraicStageSemidirectSourceKernelDerivativeSubgroup :
    Subgroup (FoxAlgebraicStageSemidirect (X := X) N n) where
  carrier :=
    { y | y.right = 1 ∧
        y.left ∈ foxAlgebraicStageSourceKernelDerivativeAddSubgroup (X := X) N n }
  one_mem' := by
    exact ⟨rfl, (foxAlgebraicStageSourceKernelDerivativeAddSubgroup (X := X) N n).zero_mem⟩
  mul_mem' := by
    intro y z hy hz
    rcases hy with ⟨hyright, hyleft⟩
    rcases hz with ⟨hzright, hzleft⟩
    constructor
    · simp only [FoxAlgebraicStageSemidirect.mul_right, hyright, hzright, mul_one]
    · rw [FoxAlgebraicStageSemidirect.mul_left, hyright]
      have hone :
          (MonoidAlgebra.of (ModNCompletedCoeff n)
            (foxAlgebraicStageTargetQuotient (X := X) N) 1 :
              foxAlgebraicStageTargetGroupAlgebra (X := X) N n) = 1 := by
        exact map_one
          (MonoidAlgebra.of (ModNCompletedCoeff n)
            (foxAlgebraicStageTargetQuotient (X := X) N))
      rw [hone, one_smul]
      exact
        (foxAlgebraicStageSourceKernelDerivativeAddSubgroup (X := X) N n).add_mem hyleft hzleft
  inv_mem' := by
    intro y hy
    rcases hy with ⟨hyright, hyleft⟩
    constructor
    · simp only [FoxAlgebraicStageSemidirect.inv_right, hyright, inv_one]
    · rw [FoxAlgebraicStageSemidirect.inv_left, hyright, inv_one]
      have hone :
          (MonoidAlgebra.of (ModNCompletedCoeff n)
            (foxAlgebraicStageTargetQuotient (X := X) N) 1 :
              foxAlgebraicStageTargetGroupAlgebra (X := X) N n) = 1 := by
        exact map_one
          (MonoidAlgebra.of (ModNCompletedCoeff n)
            (foxAlgebraicStageTargetQuotient (X := X) N))
      rw [hone, one_smul]
      exact (foxAlgebraicStageSourceKernelDerivativeAddSubgroup (X := X) N n).neg_mem hyleft

Finite source-kernel derivative semidirect points form a subgroup.

Theorem FoxDifferential.foxAlgebraicStageSemidirectSourceKernelDerivativeSubgroup_coe

@[simp]
theorem foxAlgebraicStageSemidirectSourceKernelDerivativeSubgroup_coe :
    ((foxAlgebraicStageSemidirectSourceKernelDerivativeSubgroup (X := X) N n :
        Subgroup (FoxAlgebraicStageSemidirect (X := X) N n)) :
          Set (FoxAlgebraicStageSemidirect (X := X) N n)) =
      foxAlgebraicStageSemidirectSourceKernelDerivativeSet (X := X) N n

The finite-stage semidirect source-kernel derivative subgroup coerces to its defining carrier.

Show Lean proof

Theorem FoxDifferential.foxAlgebraicStageSemidirectSourceKernelDerivativeSubgroup_le_boundaryCycleSubgroup

theorem foxAlgebraicStageSemidirectSourceKernelDerivativeSubgroup_le_boundaryCycleSubgroup
    [Fintype X] :
    foxAlgebraicStageSemidirectSourceKernelDerivativeSubgroup (X := X) N n ≤
      foxAlgebraicStageSemidirectBoundaryCycleSubgroup (X := X) N n

The finite source-kernel derivative subgroup lies inside finite semidirect boundary cycles.

Show Lean proof

Theorem FoxDifferential.foxAlgebraicStageSemiBoundaryCycleSubgroup_le_sourceKernelDerivSubgroup_iff_coord

theorem foxAlgebraicStageSemiBoundaryCycleSubgroup_le_sourceKernelDerivSubgroup_iff_coord
    {N : Subgroup (FreeGroup X)} [N.Normal] {n : ℕ} [Fintype X] :
    foxAlgebraicStageSemidirectBoundaryCycleSubgroup (X := X) N n ≤
        foxAlgebraicStageSemidirectSourceKernelDerivativeSubgroup (X := X) N n ↔
      foxAlgebraicStageBoundaryCyclesCoveredBySourceKernel (X := X) N n

Semidirect finite-stage coverage is equivalently subgroup inclusion.

Show Lean proof

ProCGroups.FoxDifferential.Completed.FiniteStage.BoundarySubgroups

Declarations