Simplifying H^n(0, G) = 0 proof

Stream: new members

[Gareth Ma]

Context: I am trying to show some of my friends about cohomology in Lean, instead I got stuck myself for a week. I tried proving $H^n(0, G) = 0$ for $G$ an abelian group and $n > 0$. This is trivial, as you have a projective resolution $0 \gets \mathbb{Z} \gets \mathbb{Z} \gets 0$ (whichever way you want) and so $H^n(0, G) = \operatorname{Ext}_{\mathbb{Z}}^n(\mathbb{Z}, G) = 0$. However, I can't figure out a clean way to do it in Lean. Can someone show me how to clean up this code and also show me around the API?

import Mathlib

open CategoryTheory Limits Representation groupCohomology HomologicalComplex
open scoped AddMonoidAlgebra
noncomputable section

universe u v
variable {R : Type}

def equivAux {k : Type u} [CommRing k] : k ≃+* k[Unit] where
  toFun := fun f ↦ MonoidAlgebra.single .unit f
  invFun := fun f ↦ f .unit
  left_inv := fun x ↦ by simp
  right_inv := fun x ↦ by ext; simp
  map_mul' := fun x y ↦ by rw [AddMonoidAlgebra.single_mul_single]
  map_add' := fun x y ↦ by simp

-- Due to unfortunate *skill issue*, I can't prove this for general trivial
-- representations, not even for k : Type u (replacing Unit with PUnit breaks
-- the proof)
theorem Rep.projective_trivial (k : Type) [CommRing k] :
    Projective (Rep.trivial k Unit k) := by
  apply Rep.equivalenceModuleMonoidAlgebra.toAdjunction.projective_of_map_projective _

  simp [Rep.equivalenceModuleMonoidAlgebra, Rep.toModuleMonoidAlgebra,
    Rep.trivial, Representation.trivial, Rep.of, Rep.ρ]
  rw [MonoidHom.comp_one, ← IsProjective.iff_projective]

  constructor
  simp_rw [Function.LeftInverse]
  use ?_, ?_
  · apply LinearMap.extendScalarsOfSurjective (R := k)
    · simp
      intro b
      use b PUnit.unit
      ext ⟨_⟩
      simp
    · use ⟨?_, ?_⟩, ?_
      · exact fun x ↦ Finsupp.single (1 : k) (equivAux x)
      · simp
      · intro m x
        ext y ⟨_⟩
        simp [asModule] at x y
        by_cases hy : y = 1
        · simp [hy, equivAux]
        · simp [hy, Finsupp.single]
  · intro x
    simp [equivAux, asModuleEquiv]
    simp [asModule] at x
    convert_to x * (1 : k) = x
    exact mul_one x

example (G : Type) [AddCommGroup G] (n : ℕ) :
    -- H^n(1, G) = 0 for n > 0
    groupCohomology (Rep.trivial ℤ Unit G) (n + 1) ≅ ModuleCat.of ℤ Unit := by
  -- idea: translate to Ext group first
  apply (groupCohomologyIsoExt _ _).trans
  convert (ProjectiveResolution.isoExt (ProjectiveResolution.self _) (n + 1) _).trans ?_
  · exact Rep.projective_trivial ℤ
  · -- Ext R C n | Ext
    apply IsZero.iso ?_ (ModuleCat.isZero_of_subsingleton _)
    -- To show homology at (n + 1) is 0, just show the (n + 1)th thing is 0 lol
    apply ShortComplex.isZero_homology_of_isZero_X₂
    simp [ChainComplex.single₀, single, linearYoneda]
    -- here
    convert ModuleCat.isZero_of_subsingleton _
    convert Unique.instSubsingleton
    simp
    exact HasZeroObject.uniqueTo (Rep.trivial ℤ Unit G)

[Gareth Ma]

My proof was first go through groupCohomologyIsoExt to turn the problem into computing an Ext group, from which I can use ProjectiveResolution.isoExt to compute it using any projective resolution, from which I choose ProjectiveResolution.self, and the rest is rather trivial.
However, proving that Rep.trivial ℤ Unit ℤ is projective (categorical / as ℤ[Unit]-module) is hard, which is what Rep.projective_trivial is doing, but it's 31 lines of ad-hoc code + random stuff above...

[Gareth Ma]

Maybe there is some trivial category theory proof, but ideally I want a proof of something like $\mathbb{Z}[Unit] \simeq \mathbb{Z}$ and then the representation is just $\mathbb{Z}$ with the nop/trivial action -> clearly projective or even free

[Gareth Ma]

(Should I ping relevant people? I don't know how many people actively work on these stuff or touch these stuff at all)

[Jz Pan]

Gareth Ma said:

as you have a projective resolution $0 \gets \mathbb{Z} \gets \mathbb{Z} \gets 0$ (whichever way you want)

Is $0 \gets 0 \gets 0 \gets 0$ a projective resolution? Can you use that?

[Gareth Ma]

I need a projective resolution of $\mathbb{Z}$

[Kevin Buzzard]

Here's various ways to prove this theorem none of which use projective resolutions. I feel like they would be more natural ways to prove the result.

If G is a finite group then multiplication by the order of G kills all cohomology in degree > 0, so if G has order 1 then an isomorphism kills cohomology so cohomology is trivial.

If G is a finite group then cohomology is known to be periodic with period 2. But it's trivial to check that every 1-cocycle is a 1-coboundary and that every 2-cocycle is a 2-coboundary so done.

Richard Hill and I are working on proving periodicity in lean. Did you apply for the Oxford workshop?

If you want to prove the result in lean using only what we have, do we not have that cohomology in degree n is isomorphic to n-cocycles over n-coboundaries? It would not surprise me if we had this and both of these groups are trivial. All you need really is the surjection from n-cocycles onto the cohomology.

[Gareth Ma]

I will have a look at all of these suggestions, thanks! FYI, I want to write and contribute something to the Mathematics in Lean page, which is why I went with the "textbook" proof of the fact, and asked for simplifications here. But now that I think about it, including different approaches such as yours is a good idea too :)

[Gareth Ma]

This can be found in Mathlib at isZero_groupCohomology_succ_of_subsingleton :D (By Amelia)