English
If P is equipped with a family of bijections MapToEqualizer for all pullback situations, then P has the equalizer condition.
Русский
Если для всех ситуаций pullback имеется отображение, удовлетворяющее условиям равнозначителя, то у P есть условие равнозначителя.
LaTeX
$$EqualizerCondition P$$
Lean4
theorem mk (P : Cᵒᵖ ⥤ Type*)
(hP :
∀ (X B : C) (π : X ⟶ B) [EffectiveEpi π] [HasPullback π π],
Function.Bijective (MapToEqualizer P π (pullback.fst π π) (pullback.snd π π) pullback.condition)) :
EqualizerCondition P := by
intro X B π _ c hc
have : HasPullback π π := ⟨c, hc⟩
specialize hP X B π
rw [Types.type_equalizer_iff_unique]
rw [Function.bijective_iff_existsUnique] at hP
intro b hb
have h₁ : ((pullbackIsPullback π π).conePointUniqueUpToIso hc).hom ≫ c.fst = pullback.fst π π := by simp
have hb' : P.map (pullback.fst π π).op b = P.map (pullback.snd _ _).op b :=
by
rw [← h₁, op_comp, FunctorToTypes.map_comp_apply, hb]
simp [← FunctorToTypes.map_comp_apply, ← op_comp]
obtain ⟨a, ha₁, ha₂⟩ := hP ⟨b, hb'⟩
refine ⟨a, ?_, ?_⟩
· simpa [MapToEqualizer] using ha₁
· simpa [MapToEqualizer] using ha₂
