isIso_adjunction_counit

Mathlib.AlgebraicGeometry.GammaSpecAdjunction

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.ΓSpec.isIso_adjunction_counit

← MathLib Explorer

English

The counit of the Γ-Spec adjunction is an isomorphism.

Русский

Каути Γ-Spec-адъункции является изоморфизмом.

LaTeX

$$⟦ΓSpec.adjunction.counit⟧ is an isomorphism$$

Lean4

instance isIso_adjunction_counit : IsIso ΓSpec.adjunction.counit :=
  by
  apply (config := { allowSynthFailures := true }) NatIso.isIso_of_isIso_app
  intro R
  rw [adjunction_counit_app]
  infer_instance

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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