equalizerCondition_iff_of_equivalence

English

The equalizer condition is preserved and reflected by precomposition with an equivalence. If P has the equalizer condition, then so does e.op.inverse ⋙ P, and conversely.

Русский

Условие равнозначителя сохраняется и отражается при предкомпозиции с эквинелентностью. Если у P есть условие равнозначителя, то и у e.op.inverse ⋙ P есть оно, и наоборот.

LaTeX

$$EqualizerCondition P ↔ EqualizerCondition (e.op.inverse ⋙ P)$$

Lean4

/-- `P` satisfies the equalizer condition iff its precomposition by an equivalence does. -/
theorem equalizerCondition_iff_of_equivalence (P : Cᵒᵖ ⥤ D) (e : C ≌ E) :
    EqualizerCondition P ↔ EqualizerCondition (e.op.inverse ⋙ P) :=
  ⟨fun h ↦ equalizerCondition_precomp_of_preservesPullback P e.inverse h, fun h ↦
    equalizerCondition_of_natIso (e.op.funInvIdAssoc P)
      (equalizerCondition_precomp_of_preservesPullback (e.op.inverse ⋙ P) e.functor h)⟩

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