Basic.lean

abbrev KernelAbelianizationAdd (ψ : G →* H) : Type _

theorem augmentation_toGroupRing_eq_zero (ψ : G →* H) (x : DifferentialModule ψ) :
    augmentation H (toGroupRing ψ x) = 0

theorem augmentation_surjective : Function.Surjective (augmentation H)

theorem exact_toGroupRing_augmentation (ψ : G →* H) (hψ : Function.Surjective ψ) :
    Function.Exact (fun x => toGroupRing ψ x) (augmentation H) := by
  intro y
  constructor
  · intro hy
    have hy_mem : y ∈ augmentationIdeal H := (mem_augmentationIdeal_iff (H := H) (x := y)).2 hy
    let y' : augmentationIdeal H := ⟨y, hy_mem⟩
    rcases toAugmentationIdeal_surjective (H := H) ψ hψ y' with ⟨x, hx⟩
    refine ⟨x, ?_⟩
    exact congrArg Subtype.val hx
  · rintro ⟨x, rfl⟩
    exact augmentation_toGroupRing_eq_zero (H := H) ψ x

def kernelBoundary (ψ : G →* H) : ψ.ker →* Multiplicative (DifferentialModule ψ) where
  toFun g := Multiplicative.ofAdd (universalDifferential ψ g.1)
  map_one' := by
    apply congrArg Multiplicative.ofAdd
    simp only [OneMemClass.coe_one, universalDifferential_one]
  map_mul' g₁ g₂ := by
    apply congrArg Multiplicative.ofAdd
    have h := universalDifferential_mul ψ g₁.1 g₂.1
    have hψ : (MonoidAlgebra.of ℤ H (ψ g₁.1) : GroupRing H) = 1 := by
      rw [g₁.2, groupRing_of_one (H := H)]
    rw [hψ, one_smul] at h
    simpa using h

def kernelAbelianizationBoundary (ψ : G →* H) :
    Abelianization ψ.ker →* Multiplicative (DifferentialModule ψ)

def kernelAbelianizationBoundaryAdd (ψ : G →* H) :
    Additive (Abelianization ψ.ker) →+ DifferentialModule ψ where
  toFun x := Multiplicative.toAdd (kernelAbelianizationBoundary ψ (Additive.toMul x))
  map_zero' := by
    simp only [toMul_zero, map_one, toAdd_one]
  map_add' x y := by
    simp only [toMul_add, map_mul, toAdd_mul]

theorem kernelAbelianizationBoundaryAdd_of (ψ : G →* H) (g : ψ.ker) :
    kernelAbelianizationBoundaryAdd ψ (Additive.ofMul (Abelianization.of g)) =
        universalDifferential ψ g.1

def kernelAbelianizationConj (ψ : G →* H) :
    G →* MulAut (Abelianization ψ.ker) where
  toFun g := (MulAut.conjNormal (H := ψ.ker) g).abelianizationCongr
  map_one' := by
    ext x
    refine QuotientGroup.induction_on x ?_
    intro n
    have hconj : MulAut.conjNormal (H := ψ.ker) (1 : G) = 1 := by
      ext m
      simp only [map_one, MulAut.one_apply]
    rw [hconj]
    rfl
  map_mul' g₁ g₂ := by
    ext x
    refine QuotientGroup.induction_on x ?_
    intro n
    let e₁ : MulAut ψ.ker := MulAut.conjNormal (H := ψ.ker) g₁
    let e₂ : MulAut ψ.ker := MulAut.conjNormal (H := ψ.ker) g₂
    have hconj : MulAut.conjNormal (H := ψ.ker) (g₁ * g₂) = e₁ * e₂ := by
      ext m
      simp only [map_mul, MulAut.mul_apply, MulAut.conjNormal_apply, mul_assoc, e₁, e₂]
    rw [hconj]
    calc
      (e₁ * e₂).abelianizationCongr (Abelianization.of n)
          = Abelianization.of ((e₁ * e₂) n) := by
              exact abelianizationCongr_of (e := e₁ * e₂) n
      _ = e₁.abelianizationCongr (Abelianization.of (e₂ n)) := by
            exact (abelianizationCongr_of (e := e₁) (e₂ n)).symm
      _ = e₁.abelianizationCongr (e₂.abelianizationCongr (Abelianization.of n)) := by
            rw [abelianizationCongr_of (e := e₂) n]
      _ = (e₁.abelianizationCongr * e₂.abelianizationCongr) (Abelianization.of n) := by
            rfl

theorem kernelAbelianizationConj_of (ψ : G →* H) (g : G) (n : ψ.ker) :
    kernelAbelianizationConj ψ g (Abelianization.of n) =
      Abelianization.of (MulAut.conjNormal (H := ψ.ker) g n)

theorem kernelAbelianizationConj_eq_one_of_mem_ker (ψ : G →* H) (n : ψ.ker) :
    kernelAbelianizationConj ψ n = 1

theorem ker_le_kernelAbelianizationConj_ker (ψ : G →* H) :
    ψ.ker ≤ (kernelAbelianizationConj ψ).ker

def quotientKernelAbelianizationConj (ψ : G →* H) :
    G ⧸ ψ.ker →* MulAut (Abelianization ψ.ker)

def kernelAbelianizationConjOfSurjective
    (ψ : G →* H) (hψ : Function.Surjective ψ) :
    H →* MulAut (Abelianization ψ.ker)

theorem kernelAbelianizationConjOfSurjective_eq_surjInv
    (ψ : G →* H) (hψ : Function.Surjective ψ) (h : H) :
    kernelAbelianizationConjOfSurjective ψ hψ h =
      kernelAbelianizationConj ψ (Function.surjInv hψ h)

def kernelAbelianizationAddAutOfSurjective
    (ψ : G →* H) (hψ : Function.Surjective ψ) :
    H →* Multiplicative (AddAut (KernelAbelianizationAdd ψ))

def kernelAbelianizationAddAutToModuleEnd (ψ : G →* H) :
    Multiplicative (AddAut (KernelAbelianizationAdd ψ)) →*
      Module.End ℤ (KernelAbelianizationAdd ψ) where
  toFun e := e.toAdd.toIntLinearEquiv.toLinearMap
  map_one' := by
    ext x
    change (0 : AddAut (KernelAbelianizationAdd ψ)) x = x
    rfl
  map_mul' e₁ e₂ := by
    ext x
    change (e₁.toAdd + e₂.toAdd) x = e₁.toAdd (e₂.toAdd x)
    rfl

def kernelAbelianizationModuleEndOfSurjective
    (ψ : G →* H) (hψ : Function.Surjective ψ) :
    H →* Module.End ℤ (KernelAbelianizationAdd ψ) where
  toFun h := kernelAbelianizationAddAutToModuleEnd (ψ := ψ)
    (kernelAbelianizationAddAutOfSurjective ψ hψ h)
  map_one' := by
    rw [(kernelAbelianizationAddAutOfSurjective ψ hψ).map_one]
    ext x
    rfl
  map_mul' h₁ h₂ := by
    rw [(kernelAbelianizationAddAutOfSurjective ψ hψ).map_mul]
    ext x
    rfl

theorem kernelAbelianizationModuleEndOfSurjective_apply
    (ψ : G →* H) (hψ : Function.Surjective ψ) (h : H) (x : KernelAbelianizationAdd ψ) :
    kernelAbelianizationModuleEndOfSurjective ψ hψ h x =
      Additive.ofMul (kernelAbelianizationConjOfSurjective ψ hψ h (Additive.toMul x))

def kernelAbelianizationActionRingHomOfSurjective
    (ψ : G →* H) (hψ : Function.Surjective ψ) :
    GroupRing H →+* Module.End ℤ (KernelAbelianizationAdd ψ)

theorem kernelAbelianizationActionRingHomOfSurjective_of
    (ψ : G →* H) (hψ : Function.Surjective ψ) (h : H) :
    kernelAbelianizationActionRingHomOfSurjective ψ hψ (MonoidAlgebra.of ℤ H h) =
      kernelAbelianizationModuleEndOfSurjective ψ hψ h

def kernelAbelianizationModuleOfSurjective
    (ψ : G →* H) (hψ : Function.Surjective ψ) :
    Module (GroupRing H) (KernelAbelianizationAdd ψ)

theorem kernelAbelianizationBoundaryAdd_conjOfSurjective
    (ψ : G →* H) (hψ : Function.Surjective ψ) (h : H) (x : Abelianization ψ.ker) :
    kernelAbelianizationBoundaryAdd ψ
        (Additive.ofMul (kernelAbelianizationConjOfSurjective ψ hψ h x)) =
      (MonoidAlgebra.of ℤ H h : GroupRing H) •
        kernelAbelianizationBoundaryAdd ψ (Additive.ofMul x)

theorem kernelAbelianizationBoundaryAdd_commOfSurjective
    (ψ : G →* H) (hψ : Function.Surjective ψ) (h : H) (x : KernelAbelianizationAdd ψ) :
    letI := kernelAbelianizationModuleOfSurjective ψ hψ
    kernelAbelianizationBoundaryAdd ψ ((MonoidAlgebra.of ℤ H h : GroupRing H) • x) =
      (MonoidAlgebra.of ℤ H h : GroupRing H) • kernelAbelianizationBoundaryAdd ψ x := by
  let := kernelAbelianizationModuleOfSurjective ψ hψ
  change kernelAbelianizationBoundaryAdd ψ
      ((kernelAbelianizationActionRingHomOfSurjective ψ hψ (MonoidAlgebra.of ℤ H h)) x) =
    (MonoidAlgebra.of ℤ H h : GroupRing H) • kernelAbelianizationBoundaryAdd ψ x
  rw [kernelAbelianizationActionRingHomOfSurjective_of,
    kernelAbelianizationModuleEndOfSurjective_apply]
  simpa using
    kernelAbelianizationBoundaryAdd_conjOfSurjective ψ hψ h (Additive.toMul x)

def kernelAbelianizationBoundaryLinearOfSurjective
    (ψ : G →* H) (hψ : Function.Surjective ψ) :
    letI := kernelAbelianizationModuleOfSurjective ψ hψ
    KernelAbelianizationAdd ψ →ₗ[GroupRing H] DifferentialModule ψ := by
  letI := kernelAbelianizationModuleOfSurjective ψ hψ
  let f : KernelAbelianizationAdd ψ →ₗ[ℤ] DifferentialModule ψ :=
    (kernelAbelianizationBoundaryAdd ψ).toIntLinearMap
  exact MonoidAlgebra.equivariantOfLinearOfComm f
    (fun h x => by
      exact kernelAbelianizationBoundaryAdd_commOfSurjective (ψ := ψ) hψ h x)

theorem kernelAbelianizationBoundaryLinearOfSurjective_of
    (ψ : G →* H) (hψ : Function.Surjective ψ) (n : ψ.ker) :
    kernelAbelianizationBoundaryLinearOfSurjective ψ hψ
        (Additive.ofMul (Abelianization.of n)) = universalDifferential ψ n.1

theorem kernelAbelianizationBoundaryLinearOfSurjective_apply
    (ψ : G →* H) (hψ : Function.Surjective ψ) (x : KernelAbelianizationAdd ψ) :
    kernelAbelianizationBoundaryLinearOfSurjective ψ hψ x =
      kernelAbelianizationBoundaryAdd ψ x

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

abbrev kernelAbelianizationBoundaryRangeOfSurjective
    (ψ : G →* H) (hψ : Function.Surjective ψ) :
    Submodule (GroupRing H) (DifferentialModule ψ)