Function.Exact.rangeFactorization

Stream: Is there code for X?

[Jz Pan]

If M → N → P is exact, then M' → N → P' is also exact, where M' and P' are images of M → N and N → P, respectively. The converse is also true.

import Mathlib.Algebra.Exact

namespace Function.Exact

variable {R M N P : Type*}

section Set

variable [Zero P] {f : M → N} {g : N → P}

theorem iff_rangeFactorization (hg : 0 ∈ Set.range g) :
    letI : Zero (Set.range g) := ⟨⟨0, hg⟩⟩
    Exact f g ↔ Exact ((↑) : Set.range f → N) (Set.rangeFactorization g) := by
  rw [Exact, Exact, Subtype.range_coe]
  congr! 2
  rw [Set.rangeFactorization]
  exact ⟨fun _ ↦ by rwa [Subtype.ext_iff], fun h ↦ by rwa [Subtype.ext_iff] at h⟩

theorem rangeFactorization (H : Exact f g) (hg : 0 ∈ Set.range g) :
    letI : Zero (Set.range g) := ⟨⟨0, hg⟩⟩
    Exact ((↑) : Set.range f → N) (Set.rangeFactorization g) :=
  (iff_rangeFactorization hg).1 H

end Set

section AddMonoidHom

variable [AddGroup M] [AddGroup N] [AddGroup P] {f : M →+ N} {g : N →+ P}

theorem iff_addMonoidHom_rangeRestrict :
    Exact f g ↔ Exact f.range.subtype g.rangeRestrict :=
  iff_rangeFactorization (zero_mem g.range)

alias ⟨addMonoidHom_rangeRestrict, _⟩ := iff_addMonoidHom_rangeRestrict

end AddMonoidHom

section LinearMap

variable [Semiring R] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P]
  [Module R M] [Module R N] [Module R P] {f : M →ₗ[R] N} {g : N →ₗ[R] P}

theorem iff_linearMap_rangeRestrict :
    Exact f g ↔ Exact f.range.subtype g.rangeRestrict :=
  iff_rangeFactorization (zero_mem (LinearMap.range g))

alias ⟨linearMap_rangeRestrict, _⟩ := iff_linearMap_rangeRestrict

end LinearMap

end Function.Exact

I think this result is used in homological algebra and commutative algebra extensively. Is it already stated in mathlib? If not, should it be added to mathlib?

[Joël Riou]

In the categorical context, I formalized the lemma docs#CategoryTheory.ShortComplex.exact_iff_of_epi_of_isIso_of_mono and its seems yours can be obtained by applying it twice. In the unbundled situation, I also formalized docs#AddMonoidHom.exact_iff_of_surjective_of_bijective_of_injective and docs#LinearMap.exact_iff_of_surjective_of_bijective_of_injective

[Jz Pan]

Thanks!

Joël Riou said:

its seems yours can be obtained by applying it twice

Yes it seems that it needs to apply twice, which is a little bit unfortunate:

M  → N → P
↓    ॥   ॥
M' → N → P
॥    ॥   ↑
M' → N → P'

So I prefer add this specialized version to mathlib. What's your opinion?

[Jz Pan]

PR created as #23446.