FoxDifferential.Completed.FiniteStage.Basic

10 Theorem | 6 Definition | 1 Instance

This module develops the Fox-differential part of the theory. It records the formulas that connect generators, boundaries, Jacobians, and completed coordinates.

Open this file on GitHub

import

FoxDifferential.Completed.CoefficientRings.AugmentationIdealPrimePower.SubtypeLinear

Imported by

Theorem FoxDifferential.modNCompletedGroupAlgebraStageMap_algebraMap GitHub

theorem modNCompletedGroupAlgebraStageMap_algebraMap
    (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) (c : ModNCompletedCoeff n) :
    modNCompletedGroupAlgebraStageMap n G U
        (algebraMap (ModNCompletedCoeff n) (ModNCompletedGroupRing n G) c) =
      algebraMap (ModNCompletedCoeff n) (ModNCompletedGroupAlgebraStage n G U) c

The finite-stage completed group-algebra projection preserves coefficient algebra maps.

Show proof

Definition finiteFoxCommutatorPowerRelatorSet GitHub

def finiteFoxCommutatorPowerRelatorSet (N : Subgroup F) (n : ℕ) : Set F :=
  {g | (∃ a ∈ N, ∃ b ∈ N, ⁅a, b⁆ = g) ∨ ∃ a ∈ N, a ^ n = g}

Relators defining the finite Fox source quotient: commutators in \(N\) and \(n\)-th powers in \(N\).

Definition finiteFoxCommutatorPowerSubgroup GitHub

def finiteFoxCommutatorPowerSubgroup (N : Subgroup F) (n : ℕ) : Subgroup F :=
  Subgroup.normalClosure (finiteFoxCommutatorPowerRelatorSet (F := F) N n)

Normal subgroup generated by commutators in \(N\) and \(n\)-th powers in \(N\).

Instance finiteFoxCommutatorPowerSubgroup_normal GitHub

instance finiteFoxCommutatorPowerSubgroup_normal
    (N : Subgroup F) (n : ℕ) :
    (finiteFoxCommutatorPowerSubgroup (F := F) N n).Normal := by
  dsimp [finiteFoxCommutatorPowerSubgroup]
  infer_instance

The finite Fox commutator-power subgroup is normal by construction.

Theorem finiteFoxCommutatorPowerRelatorSet_subset GitHub

theorem finiteFoxCommutatorPowerRelatorSet_subset
    (N : Subgroup F) (n : ℕ) :
    finiteFoxCommutatorPowerRelatorSet (F := F) N n ⊆ N

The finite Fox commutator-power relator set is contained in N.

Show proof

Theorem finiteFoxCommutatorPowerSubgroup_le_normal GitHub

theorem finiteFoxCommutatorPowerSubgroup_le_normal
    (N : Subgroup F) [N.Normal] (n : ℕ) :
    finiteFoxCommutatorPowerSubgroup (F := F) N n ≤ N

The finite Fox commutator-power subgroup is contained in \(N\) when \(N\) is normal.

Show proof

Definition finiteFoxCommutatorPowerQuotientMapToNormalQuotient GitHub

def finiteFoxCommutatorPowerQuotientMapToNormalQuotient
    (N : Subgroup F) [N.Normal] (n : ℕ) :
    F ⧸ finiteFoxCommutatorPowerSubgroup (F := F) N n →* F ⧸ N :=
  QuotientGroup.map _ _ (MonoidHom.id F)
    (finiteFoxCommutatorPowerSubgroup_le_normal (F := F) N n)

Natural quotient map \(F/[N,N]N^n \to F/N\).

Theorem finiteFoxCommutatorPowerQuotientMapToNormalQuotient_mk GitHub

theorem finiteFoxCommutatorPowerQuotientMapToNormalQuotient_mk
    (N : Subgroup F) [N.Normal] (n : ℕ) (g : F) :
    finiteFoxCommutatorPowerQuotientMapToNormalQuotient (F := F) N n
        (QuotientGroup.mk'
          (finiteFoxCommutatorPowerSubgroup (F := F) N n) g) =
      QuotientGroup.mk' N g

Evaluation of the natural quotient map \(F/[N,N]N^n \to F/N\) on a representative.

Show proof

Theorem finiteFoxCommutatorPowerQuotientMapToNormalQuotient_surjective GitHub

theorem finiteFoxCommutatorPowerQuotientMapToNormalQuotient_surjective
    (N : Subgroup F) [N.Normal] (n : ℕ) :
    Function.Surjective
      (finiteFoxCommutatorPowerQuotientMapToNormalQuotient (F := F) N n)

The natural quotient map \(F/[N,N]N^n \to F/N\) is surjective.

Show proof

Definition finiteFoxCommutatorPowerGroupAlgebraMap GitHub

def finiteFoxCommutatorPowerGroupAlgebraMap
    (N : Subgroup F) [N.Normal] (n : ℕ) :
    MonoidAlgebra (ModNCompletedCoeff n)
        (F ⧸ finiteFoxCommutatorPowerSubgroup (F := F) N n) →+*
      MonoidAlgebra (ModNCompletedCoeff n) (F ⧸ N) :=
  MonoidAlgebra.mapDomainRingHom (ModNCompletedCoeff n)
    (finiteFoxCommutatorPowerQuotientMapToNormalQuotient (F := F) N n)

Group-algebra map induced by the natural quotient \(F/[N,N]N^n \to F/N\).

Definition finiteFoxCommutatorPowerGroupAlgebraAlgHom GitHub

def finiteFoxCommutatorPowerGroupAlgebraAlgHom
    (N : Subgroup F) [N.Normal] (n : ℕ) :
    MonoidAlgebra (ModNCompletedCoeff n)
        (F ⧸ finiteFoxCommutatorPowerSubgroup (F := F) N n) →ₐ[
      ModNCompletedCoeff n]
      MonoidAlgebra (ModNCompletedCoeff n) (F ⧸ N) :=
  MonoidAlgebra.mapDomainAlgHom (ModNCompletedCoeff n) (ModNCompletedCoeff n)
    (finiteFoxCommutatorPowerQuotientMapToNormalQuotient (F := F) N n)

Algebra-hom version of the group-algebra map induced by \(F/[N,N]N^n \to F/N\).

Theorem finiteFoxCommutatorPowerGroupAlgebraAlgHom_apply GitHub

theorem finiteFoxCommutatorPowerGroupAlgebraAlgHom_apply
    (N : Subgroup F) [N.Normal] (n : ℕ)
    (x : MonoidAlgebra (ModNCompletedCoeff n)
        (F ⧸ finiteFoxCommutatorPowerSubgroup (F := F) N n)) :
    finiteFoxCommutatorPowerGroupAlgebraAlgHom (F := F) N n x =
      finiteFoxCommutatorPowerGroupAlgebraMap (F := F) N n x

The algebra-hom and ring-hom versions of the finite Fox quotient map agree on values.

Show proof

Definition finiteFoxCommutatorPowerSourceGroupAlgebraAugmentation GitHub

def finiteFoxCommutatorPowerSourceGroupAlgebraAugmentation
    (N : Subgroup F) (n : ℕ) :
    MonoidAlgebra (ModNCompletedCoeff n)
        (F ⧸ finiteFoxCommutatorPowerSubgroup (F := F) N n) →ₐ[
      ModNCompletedCoeff n] ModNCompletedCoeff n :=
  MonoidAlgebra.lift (ModNCompletedCoeff n) (ModNCompletedCoeff n)
    (F ⧸ finiteFoxCommutatorPowerSubgroup (F := F) N n)
    (1 : (F ⧸ finiteFoxCommutatorPowerSubgroup (F := F) N n) →*
      ModNCompletedCoeff n)

Augmentation map on the finite Fox source group algebra.

Theorem finiteFoxCommutatorPowerSourceGroupAlgebraAugmentation_of_quotient GitHub

theorem finiteFoxCommutatorPowerSourceGroupAlgebraAugmentation_of_quotient
    (N : Subgroup F) (n : ℕ)
    (q : F ⧸ finiteFoxCommutatorPowerSubgroup (F := F) N n) :
    finiteFoxCommutatorPowerSourceGroupAlgebraAugmentation (F := F) N n
        (MonoidAlgebra.of (ModNCompletedCoeff n)
          (F ⧸ finiteFoxCommutatorPowerSubgroup (F := F) N n) q) =
      1

The source augmentation sends every quotient group basis element to \(1\).

Show proof

Theorem finiteFoxCommutatorPowerGroupAlgebraMap_of GitHub

theorem finiteFoxCommutatorPowerGroupAlgebraMap_of
    (N : Subgroup F) [N.Normal] (n : ℕ) (g : F) :
    finiteFoxCommutatorPowerGroupAlgebraMap (F := F) N n
        (MonoidAlgebra.of (ModNCompletedCoeff n)
          (F ⧸ finiteFoxCommutatorPowerSubgroup (F := F) N n)
          (QuotientGroup.mk'
            (finiteFoxCommutatorPowerSubgroup (F := F) N n) g)) =
      MonoidAlgebra.of (ModNCompletedCoeff n) (F ⧸ N) (QuotientGroup.mk' N g)

The finite Fox source-to-target group-algebra map evaluated on a represented word.

Show proof

Theorem finiteFoxCommutatorPowerGroupAlgebraMap_of_quotient GitHub

theorem finiteFoxCommutatorPowerGroupAlgebraMap_of_quotient
    (N : Subgroup F) [N.Normal] (n : ℕ)
    (q : F ⧸ finiteFoxCommutatorPowerSubgroup (F := F) N n) :
    finiteFoxCommutatorPowerGroupAlgebraMap (F := F) N n
        (MonoidAlgebra.of (ModNCompletedCoeff n)
          (F ⧸ finiteFoxCommutatorPowerSubgroup (F := F) N n) q) =
      MonoidAlgebra.of (ModNCompletedCoeff n) (F ⧸ N)
        (finiteFoxCommutatorPowerQuotientMapToNormalQuotient (F := F) N n q)

The finite Fox source-to-target group-algebra map evaluated on a quotient basis element.

Show proof

Theorem finiteFoxCommutatorPowerGroupAlgebraMap_single_apply GitHub

theorem finiteFoxCommutatorPowerGroupAlgebraMap_single_apply
    (N : Subgroup F) [N.Normal] (n : ℕ)
    (q : F ⧸ finiteFoxCommutatorPowerSubgroup (F := F) N n)
    (a : ModNCompletedCoeff n) :
    finiteFoxCommutatorPowerGroupAlgebraMap (F := F) N n
        (MonoidAlgebra.single q a) =
      MonoidAlgebra.single
        (finiteFoxCommutatorPowerQuotientMapToNormalQuotient (F := F) N n q) a

The finite Fox source-to-target group-algebra map evaluated on a single coefficient basis term.

Show proof

FoxDifferential.Completed.FiniteStage.Basic

Declarations