instIsIsoFunctorOppositeTypeιTop

English

The inclusion morphism ι from the top subpresheaf is an isomorphism.

Русский

Включение ι верхнего подпрешафa является изоморфизмом.

LaTeX

$$$\\text{IsIso}\\big(\\text{Subpresheaf.ι}(\\top : \\text{Subpresheaf } F)\\big)$$$

Lean4

instance : IsIso (Subpresheaf.ι (⊤ : Subpresheaf F)) :=
  by
  refine @NatIso.isIso_of_isIso_app _ _ _ _ _ _ _ ?_
  intro X
  rw [isIso_iff_bijective]
  exact ⟨Subtype.coe_injective, fun x => ⟨⟨x, _root_.trivial⟩, rfl⟩⟩

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