wellPowered_opposite — Mathlib

English

A well-powered abelian category is also well-copowered (in the opposite direction).

Русский

У абелевой категории с хорошей мощностью есть аналогичная свойство в противоположной категории.

LaTeX

$$$\text{WellPowered}(C^{op})$$$

Lean4

/-- A well-powered abelian category is also well-copowered. -/
instance wellPowered_opposite [Abelian C] [LocallySmall.{w} C] [WellPowered.{w} C] : WellPowered.{w} Cᵒᵖ where
  subobject_small X := (small_congr (subobjectIsoSubobjectOp (unop X)).toEquiv).1 inferInstance

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