instEssSurjOppositeRightOp — Mathlib

English

For F : Cᵒᵖ ⥤ D, if F is essentially surjective then F.rightOp is essentially surjective.

Русский

Для F : Cᵒᵖ ⥤ D, если F является фактически сюръективным, то F.rightOp тоже essSurj.

LaTeX

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

Lean4

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

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