Yamaguchi Lean 4 Library
ProCGroups.FoxDifferential.Discrete.KernelBoundary.Quotient
ProCGroups/FoxDifferential/Discrete/KernelBoundary/Quotient

ProCGroups.FoxDifferential.Discrete.KernelBoundary.Quotient

12 Theorems | 7 Definitions | 1 Abbreviation

The principal declarations in this module are:

  • HeadQuotientOfSurjective The quotient of \(A_{\psi}\) by the image of the head map. - toIdentityDifferentialModule The canonical map from \(A_{\psi}\) to the derived module of the identity map on \(H\). - toIdentityDifferentialModule_d The canonical map to the identity differential module sends the universal differential of \(g\) to the universal differential of its image. - toAugmentationIdeal_id_comp_toIdentityDifferentialModule For the identity map, composing the identity differential module with the augmentation-ideal map gives the expected augmentation boundary.
import
Imported by

Declarations

Abbreviation FoxDifferential.HeadQuotientOfSurjective 
abbrev HeadQuotientOfSurjective (ψ : G →* H) (hψ : Function.Surjective ψ) : Type _ :=
  DifferentialModule ψ ⧸ kernelAbelianizationBoundaryRangeOfSurjective ψ hψ

The quotient of \(A_{\psi}\) by the image of the head map.

Definition FoxDifferential.toIdentityDifferentialModule 
def toIdentityDifferentialModule (ψ : G →* H) :
    DifferentialModule ψ →ₗ[GroupRing H] DifferentialModule (MonoidHom.id H) :=
  differentialModuleLift ψ
    { toFun := fun g => universalDifferential (MonoidHom.id H) (ψ g)
      map_mul' := by
        intro g₁ g₂
        simpa [map_mul] using
          universalDifferential_mul (MonoidHom.id H) (ψ g₁) (ψ g₂) }

The canonical map from \(A_{\psi}\) to the derived module of the identity map on \(H\).

Theorem FoxDifferential.toIdentityDifferentialModule_d 
@[simp]
theorem toIdentityDifferentialModule_d (ψ : G →* H) (g : G) :
    toIdentityDifferentialModule ψ (universalDifferential ψ g) = universalDifferential
        (MonoidHom.id H) (ψ g)

The canonical map to the identity differential module sends the universal differential of \(g\) to the universal differential of its image.

Show Lean proof
Theorem FoxDifferential.toAugmentationIdeal_id_comp_toIdentityDifferentialModule 
theorem toAugmentationIdeal_id_comp_toIdentityDifferentialModule
    (ψ : G →* H) :
    (toAugmentationIdeal (H := H) (MonoidHom.id H)).comp (toIdentityDifferentialModule ψ) =
      toAugmentationIdeal (H := H) ψ

For the identity map, composing the identity differential module with the augmentation-ideal map gives the expected augmentation boundary.

Show Lean proof
Theorem FoxDifferential.toIdentityDifferentialModule_kernelAbelianizationBoundaryLinearOfSurjective 
@[simp]
theorem toIdentityDifferentialModule_kernelAbelianizationBoundaryLinearOfSurjective
    (ψ : G →* H) (hψ : Function.Surjective ψ) (x : KernelAbelianizationAdd ψ) :
    toIdentityDifferentialModule ψ
      (kernelAbelianizationBoundaryLinearOfSurjective ψ hψ x) = 0

Composing the surjective-case kernel-boundary map with the identity differential-module map gives the corresponding identity-module boundary value.

Show Lean proof
Theorem FoxDifferential.kernelAbelianizationBoundaryRangeOfSurjective_le_ker_toIdentityDiffModule 
theorem kernelAbelianizationBoundaryRangeOfSurjective_le_ker_toIdentityDiffModule
    (ψ : G →* H) (hψ : Function.Surjective ψ) :
    kernelAbelianizationBoundaryRangeOfSurjective ψ hψ ≤
      LinearMap.ker (toIdentityDifferentialModule ψ)

The surjective-case kernel-boundary range lies in the kernel of the map to the identity differential module.

Show Lean proof
Definition FoxDifferential.headQuotientToIdentityDifferentialModule 
def headQuotientToIdentityDifferentialModule
    (ψ : G →* H) (hψ : Function.Surjective ψ) :
    HeadQuotientOfSurjective ψ hψ →ₗ[GroupRing H] DifferentialModule (MonoidHom.id H) :=
  (kernelAbelianizationBoundaryRangeOfSurjective ψ hψ).liftQ
    (toIdentityDifferentialModule ψ)
    (kernelAbelianizationBoundaryRangeOfSurjective_le_ker_toIdentityDiffModule ψ hψ)

The quotient map \(A_{\psi} / \operatorname{im}(\mathrm{head}) \to A_{\mathrm{id}}\).

Theorem FoxDifferential.headQuotientToIdentityDifferentialModule_mkQ 
@[simp]
theorem headQuotientToIdentityDifferentialModule_mkQ
    (ψ : G →* H) (hψ : Function.Surjective ψ) (x : DifferentialModule ψ) :
    headQuotientToIdentityDifferentialModule ψ hψ
      ((kernelAbelianizationBoundaryRangeOfSurjective ψ hψ).mkQ x) =
        toIdentityDifferentialModule ψ x

The map from the head quotient to the identity differential module has the stated value on quotient classes.

Show Lean proof
Definition FoxDifferential.headQuotientSectionOfSurjective 
def headQuotientSectionOfSurjective
    (ψ : G →* H) (hψ : Function.Surjective ψ) (h : H) :
    HeadQuotientOfSurjective ψ hψ :=
  (kernelAbelianizationBoundaryRangeOfSurjective ψ hψ).mkQ
    (universalDifferential ψ (Function.surjInv hψ h))

A section of \(\psi\) is viewed as a differential map into the head quotient.

Definition FoxDifferential.headQuotientSectionHomOfSurjective 
def headQuotientSectionHomOfSurjective
    (ψ : G →* H) (hψ : Function.Surjective ψ) :
    DifferentialHom (MonoidHom.id H) (HeadQuotientOfSurjective ψ hψ) where
  toFun := headQuotientSectionOfSurjective ψ hψ
  map_mul' := by
    intro h₁ h₂
    simpa only [scalarCrossedAction_apply] using
      headQuotientSectionOfSurjective_map_mul ψ hψ h₁ h₂

The head-quotient section in the surjective case is a crossed differential.

Definition FoxDifferential.fromIdentityDifferentialModuleOfSurjective 
def fromIdentityDifferentialModuleOfSurjective
    (ψ : G →* H) (hψ : Function.Surjective ψ) :
    DifferentialModule (MonoidHom.id H) →ₗ[GroupRing H] HeadQuotientOfSurjective ψ hψ :=
  differentialModuleLift (MonoidHom.id H) (headQuotientSectionHomOfSurjective ψ hψ)

The inverse-direction map \(A_{\mathrm{id}} \to A_{\psi} / \operatorname{im}(\mathrm{head})\) is induced by a surjective section of \(\psi\).

Theorem FoxDifferential.fromIdentityDifferentialModuleOfSurjective_d 
@[simp]
theorem fromIdentityDifferentialModuleOfSurjective_d
    (ψ : G →* H) (hψ : Function.Surjective ψ) (h : H) :
    fromIdentityDifferentialModuleOfSurjective ψ hψ (universalDifferential (MonoidHom.id H) h) =
      headQuotientSectionOfSurjective ψ hψ h

The surjective-case map from the identity differential module has the stated value on the differential generator.

Show Lean proof
Theorem FoxDifferential.headQuotientToIdentityDiffModule_fromIdentityDiffModuleOfSurjective 
theorem headQuotientToIdentityDiffModule_fromIdentityDiffModuleOfSurjective
    (ψ : G →* H) (hψ : Function.Surjective ψ) :
    (headQuotientToIdentityDifferentialModule ψ hψ).comp
      (fromIdentityDifferentialModuleOfSurjective ψ hψ) =
        LinearMap.id

The maps between the head quotient and the identity differential module are inverse on the displayed side.

Show Lean proof
Theorem FoxDifferential.fromIdentityDifferentialModuleOfSurjective_comp_toIdentityDifferentialModule 
theorem fromIdentityDifferentialModuleOfSurjective_comp_toIdentityDifferentialModule
    (ψ : G →* H) (hψ : Function.Surjective ψ) :
    (fromIdentityDifferentialModuleOfSurjective ψ hψ).comp
      (toIdentityDifferentialModule ψ) =
        (kernelAbelianizationBoundaryRangeOfSurjective ψ hψ).mkQ

The map from the identity differential module is a left inverse to the identity-differential quotient map in the surjective case.

Show Lean proof
Definition FoxDifferential.headQuotientEquivIdentityDifferentialModuleOfSurjective 
def headQuotientEquivIdentityDifferentialModuleOfSurjective
    (ψ : G →* H) (hψ : Function.Surjective ψ) :
    HeadQuotientOfSurjective ψ hψ ≃ₗ[GroupRing H] DifferentialModule (MonoidHom.id H) where
  toLinearMap := headQuotientToIdentityDifferentialModule ψ hψ
  invFun := fromIdentityDifferentialModuleOfSurjective ψ hψ
  left_inv := by
    intro x
    have hcomp :
        (fromIdentityDifferentialModuleOfSurjective ψ hψ).comp
            (headQuotientToIdentityDifferentialModule ψ hψ) =
          LinearMap.id := by
      apply Submodule.linearMap_qext _
      apply LinearMap.ext
      intro y
      change fromIdentityDifferentialModuleOfSurjective ψ hψ
          (headQuotientToIdentityDifferentialModule ψ hψ
            ((kernelAbelianizationBoundaryRangeOfSurjective ψ hψ).mkQ y)) =
        (kernelAbelianizationBoundaryRangeOfSurjective ψ hψ).mkQ y
      rw [headQuotientToIdentityDifferentialModule_mkQ]
      exact LinearMap.congr_fun
        (fromIdentityDifferentialModuleOfSurjective_comp_toIdentityDifferentialModule ψ hψ) y
    exact LinearMap.congr_fun hcomp x
  right_inv := by
    intro x
    exact LinearMap.congr_fun
      (headQuotientToIdentityDiffModule_fromIdentityDiffModuleOfSurjective ψ hψ) x

The quotient \(A_{\psi} / im(head)\) is canonically identified with the derived module of \(id_H\).

Definition FoxDifferential.headQuotientEquivAugmentationIdealOfSurjective 
def headQuotientEquivAugmentationIdealOfSurjective
    (ψ : G →* H) (hψ : Function.Surjective ψ) :
    HeadQuotientOfSurjective ψ hψ ≃ₗ[GroupRing H] augmentationIdeal H :=
  by
    classical
    exact
      (headQuotientEquivIdentityDifferentialModuleOfSurjective ψ hψ).trans
        (FoxDifferential.identityDifferentialModuleEquivAugmentationIdeal (H := H))

For a surjective \(\psi\), the Crowell head quotient is the augmentation ideal.

Theorem FoxDifferential.headQuotientEquivAugmentationIdealOfSurjective_mkQ 
@[simp]
theorem headQuotientEquivAugmentationIdealOfSurjective_mkQ
    (ψ : G →* H) (hψ : Function.Surjective ψ) (x : DifferentialModule ψ) :
    headQuotientEquivAugmentationIdealOfSurjective ψ hψ
      ((kernelAbelianizationBoundaryRangeOfSurjective ψ hψ).mkQ x) =
        toAugmentationIdeal (H := H) ψ x

The head quotient is equivalent to the augmentation ideal and sends quotient classes to their augmentation representatives.

Show Lean proof
Theorem FoxDifferential.kernelAbelianizationBoundaryRangeOfSurjective_eq_ker_toAugmentationIdeal 
theorem kernelAbelianizationBoundaryRangeOfSurjective_eq_ker_toAugmentationIdeal
    (ψ : G →* H) (hψ : Function.Surjective ψ) :
    kernelAbelianizationBoundaryRangeOfSurjective ψ hψ =
      LinearMap.ker (toAugmentationIdeal (H := H) ψ)

The range of the surjective-case kernel-abelianization boundary is the kernel of the map to the augmentation ideal.

Show Lean proof
Theorem FoxDifferential.exact_kernelAbelianizationBoundaryLinearOfSurjective_toAugmentationIdeal 
theorem exact_kernelAbelianizationBoundaryLinearOfSurjective_toAugmentationIdeal
    (ψ : G →* H) (hψ : Function.Surjective ψ) :
    Function.Exact
      (kernelAbelianizationBoundaryLinearOfSurjective ψ hψ)
      (toAugmentationIdeal (H := H) ψ)

Exactness at \(A_{\psi}\), formulated against the augmentation ideal.

Show Lean proof
Theorem FoxDifferential.exact_kernelAbelianizationBoundaryLinearOfSurjective_toGroupRing 
theorem exact_kernelAbelianizationBoundaryLinearOfSurjective_toGroupRing
    (ψ : G →* H) (hψ : Function.Surjective ψ) :
    Function.Exact
      (kernelAbelianizationBoundaryLinearOfSurjective ψ hψ)
      (toGroupRing ψ)

Exactness at \(A_{\psi}\), against the usual map \(A_{\psi}\ \to \mathbb{Z}[H]\).

Show Lean proof