instEssSurjOppositeLeftOp — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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