equalizerConditionMap_iff_nonempty_isLimit

English

There is an equivalence between the SingleEqualizerCondition for P and the nonemptiness of an IsLimit for the cocone map cone over a sieve built from X and π.

Русский

Единственное условие равнозначителя для P эквивалентно непустости IsLimit для кокона над решетом, построенным из X и π.

LaTeX

$$SingleEqualizerCondition P π ↔ Nonempty (IsLimit (P.mapCone (Sieve.ofArrows (fun _ => X) (fun _ => π)).arrows.cocone.op))$$

Lean4

theorem equalizerConditionMap_iff_nonempty_isLimit (P : Cᵒᵖ ⥤ D) ⦃X B : C⦄ (π : X ⟶ B) [HasPullback π π] :
    SingleEqualizerCondition P π ↔
      Nonempty (IsLimit (P.mapCone (Sieve.ofArrows (fun (_ : Unit) => X) (fun _ => π)).arrows.cocone.op)) :=
  by
  constructor
  · intro h
    exact ⟨isLimit_forkOfι_equiv _ _ _ (pullbackIsPullback π π) (h _ (pullbackIsPullback π π)).some⟩
  · intro ⟨h⟩
    exact fun c hc ↦ ⟨(isLimit_forkOfι_equiv _ _ _ hc).symm h⟩

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