equalizerCondition_w' — Mathlib

English

The equality of the two composites P.map π.op ∘ P.map (pullback.fst π π).op and P.map π.op ∘ P.map (pullback.snd π π).op holds in the explicit setting.

Русский

Существует равенство двух композиционных отображений P.map π.op и P.map (pullback.fst π π).op vs P.map (pullback.snd π π).op.

LaTeX

$$P.map π.op ≫ P.map (pullback.fst π π).op = P.map π.op ≫ P.map (pullback.snd π π).op$$

Lean4

theorem equalizerCondition_w' (P : Cᵒᵖ ⥤ Type*) {X B : C} (π : X ⟶ B) [HasPullback π π] :
    P.map π.op ≫ P.map (pullback.fst π π).op = P.map π.op ≫ P.map (pullback.snd π π).op := by
  simp only [← Functor.map_comp, ← op_comp, pullback.condition]

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