English
In a general categorical setting with pullbacks and preserved limits, if two maps agree after pulling back along f and g, then the map factors through the pullback arrow.
Русский
В обобщённой категориальной обстановке с pullback и сохранением пределов, если два отображения согласуются после вытягивания через f и g, то отображение факторизуется через стрелу pullback.
LaTeX
$$$\text{FactorsThrough}(a, G.map(\pi))$ under pullback conditions$$
Lean4
/-- If `G` preserves the relevant pullbacks and every effective epi in `C` is a quotient map (which is
the case when `C` is `CompHaus` or `Profinite`), then `yonedaPresheaf` satisfies the equalizer
condition which is required to be a sheaf for the regular topology.
-/
theorem equalizerCondition_yonedaPresheaf [∀ (Z B : C) (π : Z ⟶ B) [EffectiveEpi π], PreservesLimit (cospan π π) G]
(hq : ∀ (Z B : C) (π : Z ⟶ B) [EffectiveEpi π], IsQuotientMap (G.map π)) :
EqualizerCondition (yonedaPresheaf G X) :=
by
apply EqualizerCondition.mk
intro Z B π _ _
refine ⟨fun a b h ↦ ?_, fun ⟨a, ha⟩ ↦ ?_⟩
· simp only [yonedaPresheaf, unop_op, Quiver.Hom.unop_op, Set.coe_setOf, MapToEqualizer, Set.mem_setOf_eq,
Subtype.mk.injEq, comp, ContinuousMap.mk.injEq] at h
simp only [yonedaPresheaf, unop_op]
ext x
obtain ⟨y, hy⟩ := (hq Z B π).surjective x
rw [← hy]
exact congr_fun h y
· simp only [yonedaPresheaf, comp, unop_op, Quiver.Hom.unop_op, Set.mem_setOf_eq, ContinuousMap.mk.injEq] at ha
simp only [yonedaPresheaf, comp, unop_op, Quiver.Hom.unop_op, Set.coe_setOf, MapToEqualizer, Set.mem_setOf_eq,
Subtype.mk.injEq]
simp only [yonedaPresheaf, unop_op] at a
refine ⟨(hq Z B π).lift a (factorsThrough_of_pullbackCondition G X ha), ?_⟩
congr 1
exact DFunLike.ext'_iff.mp ((hq Z B π).lift_comp a (factorsThrough_of_pullbackCondition G X ha))
