map_eq_iff_precomp — Mathlib

English

For Y,Z in C and f1,f2 : Y ⟶ Z, L.map f1 = L.map f2 iff there exists X, s : X ⟶ Y with W s and s ≫ f1 = s ≫ f2.

Русский

Для Y,Z в C и f1,f2: Y ⟶ Z, L.map f1 = L.map f2 тогда и только тогда, когда существует X, s: X ⟶ Y такие что W s и s ∘ f1 = s ∘ f2.

LaTeX

$$$L.map f_1 = L.map f_2 \iff \exists X\; \exists s:\, X \to Y\; (W\; s) \;\land\; s \circ f_1 = s \circ f_2$$$

Lean4

theorem map_eq_iff_precomp {Y Z : C} (f₁ f₂ : Y ⟶ Z) :
    L.map f₁ = L.map f₂ ↔ ∃ (X : C) (s : X ⟶ Y) (_ : W s), s ≫ f₁ = s ≫ f₂ :=
  by
  constructor
  · intro h
    rw [← RightFraction.map_ofHom W _ L (Localization.inverts _ _), ←
      RightFraction.map_ofHom W _ L (Localization.inverts _ _), RightFraction.map_eq_iff] at h
    obtain ⟨Z, t₁, t₂, hst, hft, ht⟩ := h
    dsimp at t₁ t₂ hst hft ht
    grind
  · rintro ⟨Z, s, hs, fac⟩
    simp only [← cancel_epi (Localization.isoOfHom L W s hs).hom, Localization.isoOfHom_hom, ← L.map_comp, fac]

Похожие утверждения