English
If a functor preserves equalizers and products, it preserves limits of shape J.
Русский
Если функтор сохраняет равноселители и произведения, он сохраняет пределы формы J.
LaTeX
$$$PreservesLimitsOfShape J G$$
Lean4
/-- If a functor preserves equalizers and the appropriate products, it preserves limits. -/
theorem preservesLimit_of_preservesEqualizers_and_product : PreservesLimitsOfShape J G where
preservesLimit
{K} := by
let P := ∏ᶜ K.obj
let Q := ∏ᶜ fun f : Σ p : J × J, p.fst ⟶ p.snd => K.obj f.1.2
let s : P ⟶ Q := Pi.lift fun f => limit.π (Discrete.functor K.obj) ⟨_⟩ ≫ K.map f.2
let t : P ⟶ Q := Pi.lift fun f => limit.π (Discrete.functor K.obj) ⟨f.1.2⟩
let I := equalizer s t
let i : I ⟶ P := equalizer.ι s t
apply
preservesLimit_of_preserves_limit_cone
(buildIsLimit s t (by simp [P, s]) (by simp [P, t]) (limit.isLimit _) (limit.isLimit _) (limit.isLimit _))
apply IsLimit.ofIsoLimit (buildIsLimit _ _ _ _ _ _ _) _
· exact Fan.mk _ fun j => G.map (Pi.π _ j)
· exact Fan.mk (G.obj Q) fun f => G.map (Pi.π _ f)
· apply G.map s
· apply G.map t
· intro f
dsimp [P, Q, s, Fan.mk]
simp only [← G.map_comp, limit.lift_π]
congr
· intro f
dsimp [P, Q, t, Fan.mk]
simp only [← G.map_comp, limit.lift_π]
apply congrArg G.map
dsimp
· apply Fork.ofι (G.map i)
rw [← G.map_comp, ← G.map_comp]
apply congrArg G.map
exact equalizer.condition s t
· apply isLimitOfHasProductOfPreservesLimit
· apply isLimitOfHasProductOfPreservesLimit
· apply isLimitForkMapOfIsLimit
apply equalizerIsEqualizer
· refine Cones.ext (Iso.refl _) ?_
intro j; dsimp [P, Q, I, i]; simp
