English
Let hpq and hqr be submodule relations; the exactness of the induced maps p.mapQ q f hpq and q.mapQ r g hqr is equivalent to range(g) ∩ r ≤ map(g,q).
Русский
Пусть hpq и hqr задают отношения подмодулов; точность отображений p.mapQ q f hpq и q.mapQ r g hqr эквивалентна условию range(g) ∩ r ≤ map(g,q).
LaTeX
$$$$ \\operatorname{Exact}(p.mapQ q f hpq, q.mapQ r g hqr) \\iff \\operatorname{range}(g) \\cap r \\le \\operatorname{map} g q. $$$$
Lean4
/-- A necessary and sufficient condition for an exact sequence to descend to a quotient. -/
theorem exact_mapQ_iff (hfg : Exact f g) {p q r} (hpq : p ≤ comap f q) (hqr : q ≤ comap g r) :
Exact (mapQ p q f hpq) (mapQ q r g hqr) ↔ range g ⊓ r ≤ map g q :=
by
rw [exact_iff, ← (comap_injective_of_surjective (mkQ_surjective _)).eq_iff]
dsimp only [mapQ]
rw [← ker_comp, range_liftQ, liftQ_mkQ, ker_comp, range_comp, comap_map_eq, ker_mkQ, ker_mkQ, ← hfg.linearMap_ker_eq,
sup_comm, ← (sup_le hqr (ker_le_comap g)).ge_iff_eq', ← comap_map_eq, ← map_le_iff_le_comap, map_comap_eq]
