coverOfIsIso

Mathlib.AlgebraicGeometry.Cover.MorphismProperty

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

Lean4

/-- An isomorphism `X ⟶ Y` is a `P`-cover of `Y`. -/
@[simps! I₀ X f]
def coverOfIsIso [P.ContainsIdentities] [P.RespectsIso] {X Y : Scheme.{u}} (f : X ⟶ Y) [IsIso f] :
    Cover.{v} (precoverage P) Y :=
  .mkOfCovers PUnit (fun _ ↦ X) (fun _ ↦ f) (fun x ↦ ⟨⟨⟩, (inv f).base x, by simp [← comp_base_apply]⟩)
    (fun _ ↦ P.of_isIso f)

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

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

Разделы

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

Аффилиация

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