Quotient.lean

abbrev HeadQuotientOfSurjective (ψ : G →* H) (hψ : Function.Surjective ψ) : Type _

def toIdentityDifferentialModule (ψ : G →* H) :
    DifferentialModule ψ →ₗ[GroupRing H] DifferentialModule (MonoidHom.id H)

theorem toIdentityDifferentialModule_d (ψ : G →* H) (g : G) :
    toIdentityDifferentialModule ψ (universalDifferential ψ g) = universalDifferential
        (MonoidHom.id H) (ψ g)

theorem toAugmentationIdeal_id_comp_toIdentityDifferentialModule
    (ψ : G →* H) :
    (toAugmentationIdeal (H := H) (MonoidHom.id H)).comp (toIdentityDifferentialModule ψ) =
      toAugmentationIdeal (H := H) ψ

theorem toIdentityDifferentialModule_kernelAbelianizationBoundaryLinearOfSurjective
    (ψ : G →* H) (hψ : Function.Surjective ψ) (x : KernelAbelianizationAdd ψ) :
    toIdentityDifferentialModule ψ
      (kernelAbelianizationBoundaryLinearOfSurjective ψ hψ x) = 0

theorem kernelAbelianizationBoundaryRangeOfSurjective_le_ker_toIdentityDiffModule
    (ψ : G →* H) (hψ : Function.Surjective ψ) :
    kernelAbelianizationBoundaryRangeOfSurjective ψ hψ ≤
      LinearMap.ker (toIdentityDifferentialModule ψ)

def headQuotientToIdentityDifferentialModule
    (ψ : G →* H) (hψ : Function.Surjective ψ) :
    HeadQuotientOfSurjective ψ hψ →ₗ[GroupRing H] DifferentialModule (MonoidHom.id H)

theorem headQuotientToIdentityDifferentialModule_mkQ
    (ψ : G →* H) (hψ : Function.Surjective ψ) (x : DifferentialModule ψ) :
    headQuotientToIdentityDifferentialModule ψ hψ
      ((kernelAbelianizationBoundaryRangeOfSurjective ψ hψ).mkQ x) =
        toIdentityDifferentialModule ψ x

def headQuotientSectionOfSurjective
    (ψ : G →* H) (hψ : Function.Surjective ψ) (h : H) :
    HeadQuotientOfSurjective ψ hψ

theorem headQuotientSectionOfSurjective_map_mul
    (ψ : G →* H) (hψ : Function.Surjective ψ) (h₁ h₂ : H) :
    headQuotientSectionOfSurjective ψ hψ (h₁ * h₂) =
      headQuotientSectionOfSurjective ψ hψ h₁ +
        groupRingScalar (MonoidHom.id H) h₁ •
          headQuotientSectionOfSurjective ψ hψ h₂

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₂

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

theorem fromIdentityDifferentialModuleOfSurjective_d
    (ψ : G →* H) (hψ : Function.Surjective ψ) (h : H) :
    fromIdentityDifferentialModuleOfSurjective ψ hψ (universalDifferential (MonoidHom.id H) h) =
      headQuotientSectionOfSurjective ψ hψ h

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

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

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

def headQuotientEquivAugmentationIdealOfSurjective
    (ψ : G →* H) (hψ : Function.Surjective ψ) :
    HeadQuotientOfSurjective ψ hψ ≃ₗ[GroupRing H] augmentationIdeal H

theorem headQuotientEquivAugmentationIdealOfSurjective_mkQ
    (ψ : G →* H) (hψ : Function.Surjective ψ) (x : DifferentialModule ψ) :
    headQuotientEquivAugmentationIdealOfSurjective ψ hψ
      ((kernelAbelianizationBoundaryRangeOfSurjective ψ hψ).mkQ x) =
        toAugmentationIdeal (H := H) ψ x

theorem kernelAbelianizationBoundaryRangeOfSurjective_eq_ker_toAugmentationIdeal
    (ψ : G →* H) (hψ : Function.Surjective ψ) :
    kernelAbelianizationBoundaryRangeOfSurjective ψ hψ =
      LinearMap.ker (toAugmentationIdeal (H := H) ψ)

theorem exact_kernelAbelianizationBoundaryLinearOfSurjective_toAugmentationIdeal
    (ψ : G →* H) (hψ : Function.Surjective ψ) :
    Function.Exact
      (kernelAbelianizationBoundaryLinearOfSurjective ψ hψ)
      (toAugmentationIdeal (H := H) ψ)

theorem exact_kernelAbelianizationBoundaryLinearOfSurjective_toGroupRing
    (ψ : G →* H) (hψ : Function.Surjective ψ) :
    Function.Exact
      (kernelAbelianizationBoundaryLinearOfSurjective ψ hψ)
      (toGroupRing ψ)