instOverCoverOfIsIsoOfIsOver

Mathlib.AlgebraicGeometry.Cover.Over

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

Lean4

instance [P.ContainsIdentities] [P.RespectsIso] {X Y : Scheme.{u}} (f : X ⟶ Y) [X.Over S] [Y.Over S] [f.IsOver S]
    [IsIso f] : (coverOfIsIso (P := P) f).Over S
    where
  over _ := inferInstanceAs <| X.Over S
  isOver_map _ := inferInstanceAs <| f.IsOver S

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

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

Разделы

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

Аффилиация

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