Unable to prove seemingly trivial naturality

Stream: lean4

[Leorasz]

Hi guys, I'm a beginner to Lean4 and category theory and was trying to contribute to an existing project but I'm stuck at a certain point trying to prove naturality between product (with extra structure) and coproduct. Here's my code right now :

import Mathlib.Algebra.Category.ModuleCat.Abelian
import Mathlib.Algebra.Category.ModuleCat.Biproducts
import Mathlib.RingTheory.Artinian.Module
import Mathlib.LinearAlgebra.FreeModule.Finite.Basic
import Mathlib.LinearAlgebra.Dimension.StrongRankCondition
import Mathlib.LinearAlgebra.FiniteDimensional.Basic

open CategoryTheory Filter Module

universe u

def ZeroSubmod (K : Type u) [DivisionRing K] : ModuleCat.{u} K := .of _ PUnit.{u+1}

def ZeroModule (C K : Type*) [Category C] [DivisionRing K] : C ⥤ ModuleCat K where
  obj _ := ZeroSubmod K
  map _ := 𝟙 (ZeroSubmod K)

--Pointwise finite persistence modules over some small category C.
structure PtwiseFinitePersMod (C : Type*) [Category C] (K : Type*)
  [DivisionRing K] where
  to_functor : C ⥤ ModuleCat K
  finite_cond (X : C) : Module.Finite K (to_functor.obj X)

--Below : product of persistence modules
--Given R a field, C a category, X ∈ Obj(C) and F, G two functors
--C ⥤ Modules over R, this defines the product F(X) × G(X).
@[simp]
def ProductModule (R : Type) [DivisionRing R] (C : Type) [Category C]
  (F : C ⥤ ModuleCat R) (G : C ⥤ ModuleCat R) (X : C): ModuleCat R :=
  ModuleCat.of R ((F.obj X) × (G.obj X))

--Given R a field, C a category, X, Y ∈ Obj(C), f : X ⟶ Y a linear map
--and F, G two functors C ⥤ Modules over R, this defines the product map
--(F f, G f) : (F X × G X) ⟶ (F Y × G Y)
@[simp]
def ProductMapFunc (R : Type) [DivisionRing R] (C : Type) [Category C]
  {X Y : C} (f : (X ⟶ Y)) (F : C ⥤ ModuleCat R) (G : C ⥤ ModuleCat R)
  : ((F.obj X × G.obj X) →ₗ[R] (F.obj Y × G.obj Y)) where
  toFun x := by
    let x₁ := x.1
    let x₂ := x.2
    exact ⟨F.map f x₁, G.map f x₂⟩
  map_add' x y := by
    dsimp
    rw [LinearMap.map_add, LinearMap.map_add]
  map_smul' c x := by
    dsimp
    rw [LinearMap.map_smul, LinearMap.map_smul]

--Same as above, but written with the ProductModule objects for simplicity
@[simp]
def ProductModuleMap (R : Type) [DivisionRing R] (C : Type) [Category C]
  {X Y : C} (f : (X ⟶ Y)) (F : C ⥤ ModuleCat R) (G : C ⥤ ModuleCat R) :
  ((ProductModule R C F G X) ⟶ (ProductModule R C F G Y)) :=
  ModuleCat.ofHom <| ProductMapFunc R C f F G

--The direct sum of the functors F and G.
@[simp]
noncomputable def FunctorDirSum (R : Type) [DivisionRing R] (C : Type) [Category C]
  (F : C ⥤ ModuleCat R) (G : C ⥤ ModuleCat R) : C ⥤ ModuleCat R where
  obj X := ProductModule R C F G X
  map f := ProductModuleMap R C f F G
  map_id := by
    intro X
    simp
    rfl
  map_comp := by
    intro X Y Z f g
    simp
    rfl
set_option maxHeartbeats 0

noncomputable def componentIso (R : Type) [DivisionRing R] (C : Type) [Category C]
  (F : C ⥤ ModuleCat R) (G : C ⥤ ModuleCat R) (X : C) :
  ProductModule R C F G X ≅ (F ⨿ G).obj X := by
  let iso1 := (ModuleCat.biprodIsoProd (F.obj X) (G.obj X)).symm
  let iso2 := Limits.biprod.isoCoprod (F.obj X) (G.obj X)
  let iso3 : F.obj X ⨿ G.obj X ≅ (F ⨿ G).obj X := by
    have h := preservesColimitIso ((evaluation C (ModuleCat R)).obj X) (Limits.pair F G)
    have h2 := Limits.HasColimit.isoOfNatIso
      (Limits.pairComp F G ((evaluation C (ModuleCat R)).obj X))
    exact h2.symm ≪≫ h.symm
  exact iso1 ≪≫ iso2 ≪≫ iso3

lemma ModuleCat.eq_of_hom_eq (R : Type) [DivisionRing R] (M N : ModuleCat R) (f g : M ⟶ N) (h : f.hom = g.hom) : f = g := by
  exact hom_ext h

--The above-defined direct sum of persistence modules corresponds to the
--coproduct inherited from the fact that ModuleCat is abelian.
noncomputable def DirSumIsoCoprod (R : Type) [DivisionRing R] (C : Type) [Category C]
  (F : C ⥤ ModuleCat R) (G : C ⥤ ModuleCat R) :
  (FunctorDirSum R C F G) ≅ (F ⨿ G) :=
  NatIso.ofComponents (fun X => componentIso R C F G X)
  (fun {Y Z} f => by

    --other option
    apply ModuleCat.eq_of_hom_eq
    ext ⟨x₁, x₂⟩

    sorry
  )

As you can see I've proven the basic isomorphism but I'm stuck at naturality, I have the start of something with the hom and maybe doing linear algebra stuff there but I couldn't get anywhere with it. I've been working probably a dozen hours at this point trying to figure out how to do this one part of the proof but so far I've come up with nothing. I've tried all kinds of simps and then rfl but it never gets anywhere, and I still can't figure out a way to break the problem down at all to prove smaller pieces. It seems like there should be some tactic or theorem that can simplify this and I just don't have the experience to know to use it, so I was wondering if someone could even just give me a start on the problem. Any help would be greatly appreciated

[Robert Maxton]

Minor things, conveniences and general good practice:

• First, just as a matter of convenience/clarity, you can combine adjacent variable declarations of the same type, so e.g. you can just write `(F G : C ⥤ ModuleCat R)
• Similarly, you can 'factor out' variable declarations that are repeated across many definitions by putting e.g. variable (R : Type) [DivisionRing R] (C : Type) [Category C] on its own line, and it'll persist until the end of the section, namespace, or file.
• Especially when starting out, you should usually avoid building data (anything that isn't a proving a Prop) using tactics. Sometimes there's no real other option, but you should generally try without tactics first, then try using by? which tries to turn what you've built using tactics into a non-tactic term, and only then leave by in the final result. ProductMapFunc.toFun is simple enough that you're getting away with it, but it's also simple enough that it can be easily replaced with just toFun x := (F.map f x.1, G.map f x.2).
• Finally, you probably should be using the simps attribute instead of simp on most of these definitions; simps attempts to automatically provide a set of simp lemmas for e.g. applications of funlikes and projections/fields of types, which is usually better than a single simp lemma equating just the name of the definition with its body. This is particularly true in category theory where we try even harder than normal not to unfold definitions

[Robert Maxton]

With regards to your actual question: The category theory library is built heavily on abstractly defined constructions. By this I mean that, for example, F ⨿ G isn't really a concrete type, but rather the result of a nonconstructive proof of HasBinaryCoproduct F G, which essentially means ∃ M : C ⥤ ModuleCat R, M satisfies the universal property of the binary coproduct for the functors F and G.

You may already know that if you extract the witness x from an existential ∃ x, p x using choice, you know nothing about x except p x. It follows that you know nothing about, say, the biproduct F.obj X ⊞ G.obj X except for its universal properties, and that you know nothing about the various morphisms that involve it except their universal properties -- you can't "unwrap" them into a concrete definition, because there is no concrete definition.

This means that, even more so than in the rest of Mathlib, definitions should usually be followed by as much of the relevant API lemmas as you can think of, because there's otherwise no good way to interact with your definition.

[Robert Maxton]

While in your case, ProductModule and fellows are concretely defined, the rest of the category theory library is expecting various categorical projections and lemmas about how those projections behave when composed that you haven't defined yet, so it's hard to make use of.

Specifically, you need:

• The universal property of the product: the type of homs out of ProductModule F G X are in bijection with pairs of homs out of F.obj X and G.obj X. In particular, it follows that

@[ext]
lemma ProductModule.hom_ext {R : Type} [DivisionRing R] {C : Type} [Category C]
    {F G : C ⥤ ModuleCat R} {X : C} {M : ModuleCat R} {f g : ProductModule R C F G X ⟶ M}
    (h₁ : ModuleCat.ofHom (LinearMap.fst R (F.obj X) (G.obj X)) ≫ f =
      ModuleCat.ofHom (LinearMap.fst R (F.obj X) (G.obj X)) ≫ g)
    (h₂ : ModuleCat.ofHom (LinearMap.snd R (F.obj X) (G.obj X)) ≫ f =
      ModuleCat.ofHom (LinearMap.snd R (F.obj X) (G.obj X)) ≫ g) : f = g := by
  sorry

(Registering this lemma as ext lets ext take apart all such homs for you automatically, so you shouldn't even need to explicitly invoke this in DirSumIsoCoprod.)

• Similarly, ProductModuleMap commutes with the projections: ProductModuleMap F G f ≫ ofHom (fst R (F.obj Y) (G.obj Y) ) = ofHom (fst R (F.obj X) (G.obj X)) and similarly for snd.

Once you have that, you should be able to make progress on DirSumIsoCoprod.