fullyFaithful — Mathlib

English

The inclusion functor, on the opposite category, is fully faithful.

Русский

С другой стороны, включение является полнофидным в противоположной категории.

LaTeX

$$$$ (\\mathrm{inclusion}(n))^{op}.FullyFaithful $$$$

Lean4

/-- A proof that the full subcategory inclusion is fully faithful -/
noncomputable def fullyFaithful (n : ℕ) : (inclusion n : Truncated n ⥤ _).op.FullyFaithful :=
  Functor.FullyFaithful.ofFullyFaithful _

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