instFullOppositeIdealSheafDataOverSubschemeFunctor

English

There is a fullness instance for the opposite of the subscheme functor on Y.

Русский

Существуют полноты для противоположенного подсхемного функторa над Y.

LaTeX

$$$(IdealSheafData.subschemeFunctor Y).Full$$$

Lean4

instance : (IdealSheafData.subschemeFunctor Y).Full :=
  have : IsIso Y.kerAdjunction.rightOp.counit := by simp [NatTrans.isIso_iff_isIso_app, CategoryTheory.instIsIsoEqToHom]
  Y.kerAdjunction.rightOp.fullyFaithfulROfIsIsoCounit.full

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