of_preserves_binary_and_terminal — Mathlib

English

This continues the construction showing that F preserves the shape of Fin n diagrams for all n, given the base preservation properties.

Русский

Продолжение показывает, что F сохраняет форму диаграмм Fin n для всех n, если выполнены базовые свойства сохранения.

LaTeX

$$$$ \text{PreservesFiniteProducts.of_preserves_binary_and_terminal}(F) \Rightarrow \text{PreservesLimitsOfShape}(\mathrm{Discrete}(\mathrm{Fin}\,n))\, F \text{ for all } n. $$$$

Lean4

/-- If `F` preserves the terminal object and binary products then it preserves finite products. -/
theorem of_preserves_binary_and_terminal : PreservesFiniteProducts F where
  preserves
    n := by
    refine ⟨fun {K} ↦ ?_⟩
    let that : (Discrete.functor fun n => K.obj ⟨n⟩) ≅ K := Discrete.natIso fun ⟨i⟩ => Iso.refl _
    haveI := preservesFinOfPreservesBinaryAndTerminal F n fun n => K.obj ⟨n⟩
    apply preservesLimit_of_iso_diagram F that

Похожие утверждения