Rewriting `f ∈ groupCohomology.(one|two)Coboundaries`

Stream: Is there code for X?

[Yudai Yamazaki]

Do we already have these in Mathlib?

What I would like to have are mem_oneCoboundaries_iff and mem_twoCoboundaries_iff in the snippet below, with the use cases being to rewrite f ∈ groupCohomology.(one|two)Coboundaries (Rep.ofMulDistribMulAction G A) into existential statements where f is a cocycle. I could find groupCohomology.Is(One|Two)Coboundary, but I could not find relevant lemmas when you have [MulDistribMulAction G A].

import Mathlib.RepresentationTheory.GroupCohomology.LowDegree

namespace groupCohomology

universe u
variable {k : Type u} {G : Type u} [CommRing k] [Group G] {A : Rep k G}

lemma oneCocycles_ext_iff (f₁ f₂ : oneCocycles A) :
    f₁ = f₂ ↔ ∀ g : G, (f₁ : G → A) g = (f₂ : G → A) g :=
  ⟨fun h g ↦ congrFun (congrArg Subtype.val h) g, fun h ↦ Subtype.ext (funext fun g ↦ h g)⟩

lemma mem_oneCoboundaries_iff (f : oneCocycles A) :
    f ∈ oneCoboundaries A ↔
    ∃ x : A, ∀ g : G, A.ρ g x - x = (f : G → A) g := by
  apply exists_congr
  intro x
  simp only [LinearMap.codRestrict, dZero, LinearMap.coe_mk, AddHom.coe_mk, oneCocycles_ext_iff]

lemma twoCocycles_ext_iff (f₁ f₂ : twoCocycles A) :
    f₁ = f₂ ↔
    ∀ g h : G, (f₁ : G × G → A) (g, h) = (f₂ : G × G → A) (g, h) :=
  ⟨fun hf g h ↦ congrFun (congrArg Subtype.val hf) (g, h),
    fun hf ↦ Subtype.ext (funext fun ⟨g, h⟩ ↦ hf g h)⟩

lemma mem_twoCoboundaries_iff (f : twoCocycles A) :
    f ∈ twoCoboundaries A ↔
    ∃ x : G → A, ∀ g h : G, A.ρ g (x h) - x (g * h) + x g = f.val (g, h) := by
  apply exists_congr
  intro x
  simp only [LinearMap.codRestrict, dOne, LinearMap.coe_mk, AddHom.coe_mk, twoCocycles_ext_iff]

end groupCohomology

-- A use case
example {G A : Type} [Group G] [CommGroup A] [MulDistribMulAction G A]
    {f f' : groupCohomology.twoCocycles (Rep.ofMulDistribMulAction G A)}
    (h : f - f' ∈ groupCohomology.twoCoboundaries (Rep.ofMulDistribMulAction G A)) :
    ∃ x : G → A, ∀ g₁ g₂ : G, Additive.toMul (α := A) (f.val (g₁, g₂)) *
    (Additive.toMul (α := A) (f'.val (g₁, g₂)))⁻¹ = g₁ • x g₂ * (x (g₁ * g₂))⁻¹ * x g₁ := by
  rw [groupCohomology.mem_twoCoboundaries_iff] at h
  obtain ⟨x, hx⟩ := h
  use fun g ↦ Additive.toMul (x g)
  intro g₁ g₂
  simpa only [Rep.ofMulDistribMulAction_ρ_apply_apply, ← div_eq_mul_inv]
    using Additive.toMul.injective (hx g₁ g₂).symm

[Joël Riou]

If it is not in Mathlib.RepresentationTheory.GroupCohomology.LowDegree, then it is not in mathlib!

[Kevin Buzzard]

These look like very sensible API for low degree cohomology. Please feel free to PR!

[Yudai Yamazaki]

I am happy to open a PR, but I am now thinking this implementation below may be more consistent with other APIs in Mathlib.
Should we introduce FunLike on cocycles and coboundaries?

import Mathlib.RepresentationTheory.GroupCohomology.LowDegree

namespace groupCohomology

universe u
variable {k : Type u} {G : Type u} [CommRing k] [Group G] {A : Rep k G}

instance : FunLike (oneCocycles A) G A := ⟨(·.val), Subtype.val_injective⟩
instance : FunLike (twoCocycles A) (G × G) A := ⟨(·.val), Subtype.val_injective⟩
instance : FunLike (oneCoboundaries A) G A :=
  ⟨(·.val), Function.Injective.comp Subtype.val_injective Subtype.val_injective⟩
instance : FunLike (twoCoboundaries A) (G × G) A :=
  ⟨(·.val), Function.Injective.comp Subtype.val_injective Subtype.val_injective⟩

@[ext]
theorem oneCocycles_ext {f₁ f₂ : oneCocycles A} (h : ∀ g : G, f₁ g = f₂ g) : f₁ = f₂ :=
  DFunLike.ext _ _ h

theorem mem_oneCoboundaries_iff (f : oneCocycles A) : f ∈ oneCoboundaries A ↔
    ∃ x : A, ∀ g : G, A.ρ g x - x = f g := by
  apply exists_congr
  intro x
  simpa only [LinearMap.codRestrict, dZero, LinearMap.coe_mk, AddHom.coe_mk] using
    groupCohomology.oneCocycles_ext_iff

@[ext]
theorem twoCocycles_ext {f₁ f₂ : twoCocycles A} (h : ∀ g h : G, f₁ (g, h) = f₂ (g, h)) : f₁ = f₂ :=
  DFunLike.ext _ _ (Prod.forall.mpr h)

theorem mem_twoCoboundaries_iff (f : twoCocycles A) : f ∈ twoCoboundaries A ↔
    ∃ x : G → A, ∀ g h : G, A.ρ g (x h) - x (g * h) + x g = f (g, h) := by
  apply exists_congr
  intro x
  simpa only [LinearMap.codRestrict, dOne, LinearMap.coe_mk, AddHom.coe_mk] using
    groupCohomology.twoCocycles_ext_iff

end groupCohomology

The FunLike instances can be generalised to any Subtype of a function or FunLike types, but I am hesitating to take this approach as it may trigger too many instances throughout Mathlib.

import Mathlib.RepresentationTheory.GroupCohomology.LowDegree

instance {α β : Sort*} (p : (α → β) → Prop) : FunLike (Subtype p) α β where
  coe := (·.val)
  coe_injective' := Subtype.val_injective

instance {F α β : Sort*} (p : F → Prop) [FunLike F α β] : FunLike (Subtype p) α β where
  coe := (·.val)
  coe_injective' := Function.Injective.comp DFunLike.coe_injective Subtype.val_injective

namespace groupCohomology

universe u
variable {k : Type u} {G : Type u} [CommRing k] [Group G] {A : Rep k G}

#synth FunLike (oneCocycles A) G A
#synth FunLike (twoCocycles A) (G × G) A
#synth FunLike (oneCoboundaries A) G A
#synth FunLike (twoCoboundaries A) (G × G) A

end groupCohomology

[Yudai Yamazaki]

I've just opened a PR: https://github.com/leanprover-community/mathlib4/pull/17934. I would appreciate your comments.

[Amelia Livingston]

These additions look good to me, thank you for making them! I had similar hesitations about a Subtype FunLike instance when making the one/two cocycle API but the cocycle-specific FunLike instances seem good.

[Yudai Yamazaki]

The PR is merged as commit 24ecc2adb768d0db30080861f91a14287fb13067. Thank you for your comments.