instIsIsoSheafZariskiTopologyTypeYonedaGluedToSheaf

Mathlib.AlgebraicGeometry.Sites.Representability

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.Scheme.LocalRepresentability.instIsIsoSheafZariskiTopologyTypeYonedaGluedToSheaf

English

The glued-to-sheaf morphism is an isomorphism.

Русский

Отображение glued-to-sheaf является изоморфизмом.

LaTeX

$$IsIso (yonedaGluedToSheaf hf)$$

Lean4

instance : IsIso (yonedaGluedToSheaf hf) :=
  by
  rw [← Sheaf.isLocallyBijective_iff_isIso (yonedaGluedToSheaf hf)]
  constructor <;> infer_instance

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru