pullbackCompatible_iff — Mathlib

English

With HasPairwisePullbacks, hx. PullbackCompatible is equivalent to hx.Compatible.

Русский

При наличии HasPairwisePullbacks hx. PullbackCompatible эквивалентен hx.Compatible.

LaTeX

$$hx.PullbackCompatible ≡ hx.Compatible$$

Lean4

theorem pullbackCompatible_iff (x : (i : I) → P.obj (op (X i))) : Compatible P π x ↔ PullbackCompatible P π x :=
  by
  refine ⟨fun t i j ↦ ?_, fun t i j Z gi gj comm ↦ ?_⟩
  · apply t
    exact pullback.condition
  ·
    rw [← pullback.lift_fst _ _ comm, op_comp, FunctorToTypes.map_comp_apply, t i j, ← FunctorToTypes.map_comp_apply, ←
      op_comp, pullback.lift_snd]

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