English
The equalizer condition for a presheaf P is equivalent to the assertion that the lift in the explicit equalizer diagram is an isomorphism for every pullback diagram.
Русский
Условие равнозначителя для префункторa P эквивалентно тому, что каноническое поднятие в явном равнозначителе является изоморфизмом в каждой диаграмме pullback.
LaTeX
$$EqualizerCondition P ↔ ∀ X B π [EffectiveEpi π] [HasPullback π π], IsIso (equalizer.lift (P.map π.op) (equalizerCondition_w' P π))$$
Lean4
/-- An alternative phrasing of the explicit equalizer condition, using more categorical language. -/
theorem equalizerCondition_iff_isIso_lift (P : Cᵒᵖ ⥤ Type*) :
EqualizerCondition P ↔
∀ (X B : C) (π : X ⟶ B) [EffectiveEpi π] [HasPullback π π],
IsIso (equalizer.lift (P.map π.op) (equalizerCondition_w' P π)) :=
by
constructor
· intro hP X B π _ _
have h := hP.bijective_mapToEqualizer_pullback _ X B π
rw [← isIso_iff_bijective, mapToEqualizer_eq_comp] at h
exact
IsIso.of_isIso_comp_right (equalizer.lift (P.map π.op) (equalizerCondition_w' P π)) (Types.equalizerIso _ _).hom
· intro hP
apply EqualizerCondition.mk
intro X B π _ _
rw [mapToEqualizer_eq_comp, ← isIso_iff_bijective]
infer_instance
