English
If P satisfies the equalizer condition, then for any X, B, a morphism π: X → B with EffectiveEpi π and HasPullback π with itself, the canonical MapToEqualizer map for the pullback data is bijective.
Русский
Если P удовлетворяет условию равнозначителя, то для любых X, B и морфизма π: X → B с эффективной эпиморфией π и существованием кривой притяжения pullback π π, каноническое отображение MapToEqualizer по данным про источник из сопряжённого диаграммы является биекция.
LaTeX
$$Function.Bijective (MapToEqualizer P π (pullback.fst π π) (pullback.snd π π) pullback.condition)$$
Lean4
theorem bijective_mapToEqualizer_pullback (P : Cᵒᵖ ⥤ Type*) (hP : EqualizerCondition P) :
∀ (X B : C) (π : X ⟶ B) [EffectiveEpi π] [HasPullback π π],
Function.Bijective (MapToEqualizer P π (pullback.fst π π) (pullback.snd π π) pullback.condition) :=
by
intro X B π _ _
specialize hP π _ (pullbackIsPullback π π)
rw [Types.type_equalizer_iff_unique] at hP
rw [Function.bijective_iff_existsUnique]
intro ⟨b, hb⟩
obtain ⟨a, ha₁, ha₂⟩ := hP b hb
refine ⟨a, ?_, ?_⟩
· simpa [MapToEqualizer] using ha₁
· simpa [MapToEqualizer] using ha₂
