left exactness of hom

Stream: Is there code for X?

[Wang Jingting]

Hi! Do we have the left exactness of hom in Mathlib? I tried searching (loogle) for LinearMap.comp, |- Function.Exact _ _ but found nothing.

[Kenny Lau]

@Wang Jingting is CategoryTheory.coyoneda_preservesLimit ok? what is the context of this question?

[Wang Jingting]

Sorry, the context is the same as @Nailin Guan described in the Gorenstein ring thread. Thanks for the category version anyway. :)

[Kenny Lau]

it should be formally equivalent to LinearMap.cancel_right and LinearMap.cancel_left right?

[Kenny Lau]

as in, if not, we would missing some huge API

[Kenny Lau]

as in the theorem that says a functor is left exact iff it sends injective maps (surjective if dualized) to injective maps

[Wang Jingting]

Actually I didn't know this theorem before, is there something I can refer to? Thanks!

[Andrew Yang]

You haven't heard of it is probably because it is not true? e.g. the constant functor _ => Z preserves injective maps but is far from being left exact.

[Andrew Yang]

Probably you could just prove this by hand.

[Christian Merten]

You probably at least need the functor to be additive.

[Kenny Lau]

image.png

I was referring to this theorem, I probably left out some important assumptions

[Joël Riou]

@Jujian Zhang and I formalized characterizations of (additive) left/right exact functors https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Homology/ShortComplex/ExactFunctor.html

[Aaron Liu]

Well that's because you can replace C with coker(A --> B) ...probably

[Wang Jingting]

Kenny Lau said:

image.png

I was referring to this theorem, I probably left out some important assumptions

Yeah, that theorem is certainly true, but I think we still need more than the injectivity of $F(A) \rightarrow F(B)$? The exactness at $F(B)$ also needs to be verified. The corresponding theorems for tensor product are:

theorem lTensor_exact {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4}
    [CommRing R] [AddCommGroup M] [AddCommGroup N] [AddCommGroup P]
    [Module R M] [Module R N] [Module R P] {f : M →ₗ[R] N} {g : N →ₗ[R] P}
    (Q : Type u_5) [AddCommGroup Q] [Module R Q]
    (hfg : Function.Exact ⇑f ⇑g) (hg : Function.Surjective ⇑g) :
    Function.Exact ⇑(LinearMap.lTensor Q f) ⇑(LinearMap.lTensor Q g)

theorem LinearMap.lTensor_surjective {R : Type u_1} [CommSemiring R]
    {N : Type u_3} {P : Type u_4} (Q : Type u_5)
    [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q]
    [Module R N] [Module R P] [Module R Q] {g : N →ₗ[R] P} (hg : Function.Surjective ⇑g) :
    Function.Surjective ⇑(lTensor Q g)

So the theorems you mentioned just now shows the injectivity of $F(A) \rightarrow F(B)$, similar to LinearMap.lTensor_surjective, but we still want the theorem that the sequence is exact at $F(B)$, which should be similar to lTensor_exact.

But the good news is that they are both not hard to show for Hom, so @Nailin Guan just proved them yesterday and made a separate PR.