equalizerCondition_of_natIso — Mathlib

English

The equalizer condition is preserved by natural isomorphism: if i: P ≅ P' and P satisfies EqualizerCondition, then P' does as well.

Русский

Условие равнителя сохраняется при натуральном изоморфизме: если i: P ≅ P' и P удовлетворяет EqualizerCondition, то и P' удовлетворяет.

LaTeX

$$$i: P \\cong P' \\quad\\text{and}\\quad EqualizerCondition(P) \\Rightarrow EqualizerCondition(P')$$$

Lean4

/-- The equalizer condition is preserved by natural isomorphism. -/
theorem equalizerCondition_of_natIso {P P' : Cᵒᵖ ⥤ D} (i : P ≅ P') (hP : EqualizerCondition P) :
    EqualizerCondition P' := fun X B π _ c hc ↦ ⟨Fork.isLimitOfIsos _ (hP π c hc).some _ (i.app _) (i.app _) (i.app _)⟩

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