mapToEqualizer_eq_comp — Mathlib

English

The explicit map to the equalizer coincides with the standard equalizer lift composed with an isomorphism from the equalizer object.

Русский

Явная карта к равнозначителю совпадает с обычной подъемкой равнозначителя, композиционной с изоморфизмом равнозначителя.

LaTeX

$$MapToEqualizer P π (pullback.fst π π) (pullback.snd π π) pullback.condition = equalizer.lift (P.map π.op) (equalizerCondition_w' P π) ≫ (Types.equalizerIso _ _).hom$$

Lean4

theorem mapToEqualizer_eq_comp (P : Cᵒᵖ ⥤ Type*) {X B : C} (π : X ⟶ B) [HasPullback π π] :
    MapToEqualizer P π (pullback.fst π π) (pullback.snd π π) pullback.condition =
      equalizer.lift (P.map π.op) (equalizerCondition_w' P π) ≫ (Types.equalizerIso _ _).hom :=
  by
  rw [← Iso.comp_inv_eq (α := Types.equalizerIso _ _)]
  apply equalizer.hom_ext
  aesop

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