Oddities with functors

Stream: new members

[VayusElytra]

Hi, I noticed lately some very odd behaviour from Lean regarding functors and am curious to hear why it works the way it does.

noncomputable def IntervalModule (a b : ℝ) (F : Type) [DivisionRing F]

  : (PersistenceModule ℝ F) where

  obj := fun (x : ℝ) ↦ IntervalModuleObject a b x F

  map := by

    dsimp

    intro x y h'

    have h : x ≤ y := leOfHom h'

    use (IntervalModuleMorphism a b x y h F)

    --Here lean asks me to prove linearity again.

For our purposes: PersistenceModule ℝ F is the category of functors from ℝ (as a partial order) to F-vector spaces. IntervalModuleObject is a specific assignment of a vector space for each x in ℝ depending on the parameters a and b, and IntervalModuleMorphism is a map between these vector spaces.

In particular, I have proven in its definition that the IntervalModuleMorphism is indeed a morphism (that is to say, it's a linear map between vector spaces). But here when I try to use it in this definition, I am asked to prove that it is linear all over again. Why so? This seems like a colossal waste of time to me...

[Andrew Yang]

I cannot be sure without a #mwe but does changing use to exact work?

[VayusElytra]

(deleted)

[VayusElytra]

OK, that was fine. Still not sure why I am asked to prove that a linear map is indeed linear, but a simple rw[map_smul] solved it.

[Andrew Yang]

Looking at the mwe, I don't think you are asked to provide the proof that IntervalModuleMorphism is linear. Sure aesop fails, but this is because functors should preserve identities and compositions and lean cannot figure out this by itself (we need better error messages here...). This makes the error go away.

noncomputable def IntervalModule (a b : ℝ) (F : Type) [DivisionRing F]
  : (PersistenceModule ℝ F) where
  obj := fun (x : ℝ) ↦ IntervalModuleObject a b x F
  map := by
    dsimp
    intro x y h'
    have h : x ≤ y := leOfHom h'
    exact (IntervalModuleMorphism a b x y h F)
  map_id := sorry
  map_comp := sorry

[VayusElytra]

You are correct, thank you! I just realised this myself. I just need to prove map_id and map_comp manually with this now, which sounds very tedious but doable.