instPreservesLimitsOfShapeOppositeLightProfiniteDiscreteCarrier

English

If F preserves finite products, then for every finite X, F preserves all limits of shape Discrete X (i.e., limits over the discrete category on X).

Русский

Если F сохраняет конечные произведения, то для каждого конечного множества X F сохраняет все пределы формы Discrete X (то есть пределы диаграмм, индексируемых дискретной категорией на X).

LaTeX

$$$\forall X,\ \text{PreservesLimitsOfShape}(\text{Discrete}(X), F)$$$

Lean4

noncomputable instance (X : FintypeCat.{u}) : PreservesLimitsOfShape (Discrete X) F :=
  let X' := (Countable.toSmall.{0} X).equiv_small.choose
  let e : X ≃ X' := (Countable.toSmall X).equiv_small.choose_spec.some
  have : Fintype X' := Fintype.ofEquiv X e
  preservesLimitsOfShape_of_equiv (Discrete.equivalence e.symm) F

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