of_equivalence — Mathlib

English

If J is a small category that is κ-filtered for a regular cardinal κ, then the κ-filteredness is preserved under equivalence of categories. In particular, for any equivalence e: J ≌ J', we have IsCardinalFiltered J' κ from IsCardinalFiltered J κ.

Русский

Если J — малая категория, являющаяся κ-фильтрованной при регулярном кардинале κ, то это свойство сохраняется при эквивалентности категорий. То есть для любой эквивалентности e: J ≌ J' имеем IsCardinalFiltered J' κ от IsCardinalFiltered J κ.

LaTeX

$$$\\text{If } J \\simeq J' \\text{ and } κ \\text{ is regular with } [\\text{IsCardinalFiltered } J κ], \\; \\text{then } IsCardinalFiltered(J', κ).$$$

Lean4

theorem of_equivalence {J' : Type u'} [Category.{v'} J'] (e : J ≌ J') : IsCardinalFiltered J' κ where
  nonempty_cocone F hA := ⟨e.inverse.mapCoconeInv (cocone (F ⋙ e.inverse) hA)⟩

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