instEssSurjOppositeOp — Mathlib

English

If F : C ⥤ D is essentially surjective, then the opposite functor F.op is essentially surjective as well.

Русский

Если F : C ⥤ D является фактически сюръективным, то противоположный функтор F.op также фактически сюръективен.

LaTeX

$$$\text{If } F:\, \mathcal{C} \to \mathcal{D} \text{ is EssSurj, then } F.op:\, \mathcal{C}^{op} \to \mathcal{D}^{op} \text{ is EssSurj}$$$

Lean4

instance {F : C ⥤ D} [EssSurj F] : EssSurj F.op where mem_essImage X := ⟨op _, ⟨(F.objObjPreimageIso X.unop).op.symm⟩⟩

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