English
From preservation of binary products and terminal, obtain preservation of shape Discrete Fin n for any n.
Русский
Из сохранения бинарных произведений и терминального объекта вытекает сохранение формы Discrete Fin n для любого n.
LaTeX
$$$$ \text{preservesShape\_fin\_of\_preserves\_binary\_and\_terminal}(F,n) \;:\; \text{PreservesLimitsOfShape } (\mathrm{Discrete}(\mathrm{Fin}\,n))\, F. $$$$
Lean4
/-- If `F` preserves the terminal object and binary products, then it preserves products indexed by
`Fin n` for any `n`.
-/
theorem preservesFinOfPreservesBinaryAndTerminal : ∀ (n : ℕ) (f : Fin n → C), PreservesLimit (Discrete.functor f) F
| 0 => fun f =>
by
letI : PreservesLimitsOfShape (Discrete (Fin 0)) F :=
preservesLimitsOfShape_of_equiv.{0, 0} (Discrete.equivalence finZeroEquiv'.symm) _
infer_instance
| n + 1 => by
haveI := preservesFinOfPreservesBinaryAndTerminal n
intro f
apply preservesLimit_of_preserves_limit_cone (extendFanIsLimit f (limit.isLimit _) (limit.isLimit _)) _
apply (isLimitMapConeFanMkEquiv _ _ _).symm _
let this :=
extendFanIsLimit (fun i => F.obj (f i)) (isLimitOfHasProductOfPreservesLimit F _)
(isLimitOfHasBinaryProductOfPreservesLimit F _ _)
refine IsLimit.ofIsoLimit this ?_
apply Cones.ext _ _
· apply Iso.refl _
rintro ⟨j⟩
refine Fin.inductionOn j ?_ ?_
· apply (Category.id_comp _).symm
· rintro i _
dsimp [extendFan_π_app, Iso.refl_hom, Fan.mk_π_app]
change F.map _ ≫ _ = 𝟙 _ ≫ _
simp only [id_comp, ← F.map_comp]
rfl
