pushforwardIso

Mathlib.AlgebraicGeometry.Cover.MorphismProperty

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

Lean4

/-- The pushforward of a cover along an isomorphism. -/
@[simps! I₀ X f]
def pushforwardIso [P.RespectsIso] [P.ContainsIdentities] [P.IsStableUnderComposition] {X Y : Scheme.{u}}
    (𝒰 : Cover.{v} (precoverage P) X) (f : X ⟶ Y) [IsIso f] : Cover.{v} (precoverage P) Y :=
  Cover.copy ((coverOfIsIso.{v, u} f).bind fun _ => 𝒰) 𝒰.I₀ _ _
    ((Equiv.punitProd _).symm.trans (Equiv.sigmaEquivProd PUnit 𝒰.I₀).symm) (fun _ => Iso.refl _) fun _ =>
    (Category.id_comp _).symm

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

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

Разделы

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

Аффилиация

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