English
Precomposing with a pullback-preserving functor preserves the equalizer condition in a coherent regular topology context.
Русский
Пре-композиция с функтором, сохраняющим пулбек, сохраняет равнитель при когерентной нормальной топологии.
LaTeX
$$$EqualizerCondition (F.op \circ P)$ given $EqualizerCondition P$$$
Lean4
/-- Precomposing with a pullback-preserving functor preserves the equalizer condition. -/
theorem equalizerCondition_precomp_of_preservesPullback (P : Cᵒᵖ ⥤ D) (F : E ⥤ C)
[∀ {X B} (π : X ⟶ B) [EffectiveEpi π], PreservesLimit (cospan π π) F] [F.PreservesEffectiveEpis]
(hP : EqualizerCondition P) : EqualizerCondition (F.op ⋙ P) :=
by
intro X B π _ c hc
have h : P.map (F.map π).op = (F.op ⋙ P).map π.op := by simp
refine ⟨(IsLimit.equivIsoLimit (ForkOfι.ext ?_ _ h)) ?_⟩
· simp only [Functor.comp_map, op_map, Quiver.Hom.unop_op, ← map_comp, ← op_comp, c.condition]
· refine (hP (F.map π) (PullbackCone.mk (F.map c.fst) (F.map c.snd) ?_) ?_).some
· simp only [← map_comp, c.condition]
·
exact
(isLimitMapConePullbackConeEquiv F c.condition)
(isLimitOfPreserves F (hc.ofIsoLimit (PullbackCone.ext (Iso.refl _) (by simp) (by simp))))
