factors_congr — Mathlib

English

If f ≅ g are mono-over X, then through a fixed Y → X the property f.Factors h is equivalent to g.Factors h; i.e., factoring data is invariant under isomorphism of mono-over objects.

Русский

Если f и g являются изоморфнами как моно Over X, то свойство f.Factors h эквивалентно g.Factors h для фиксированного h: факторизационные данные сохраняются под изоморфизмами.

LaTeX

$$$f \\cong g \\Rightarrow (f.Factors h) \\iff (g.Factors h).$$$

Lean4

theorem factors_congr {X : C} {f g : MonoOver X} {Y : C} (h : Y ⟶ X) (e : f ≅ g) : f.Factors h ↔ g.Factors h :=
  ⟨fun ⟨u, hu⟩ => ⟨u ≫ ((MonoOver.forget _).map e.hom).left, by simp [hu]⟩, fun ⟨u, hu⟩ =>
    ⟨u ≫ ((MonoOver.forget _).map e.inv).left, by simp [hu]⟩⟩

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