pullbackCoverAffineRefinementObjIso

Mathlib.AlgebraicGeometry.Cover.Open

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

Lean4

/-- The pullback of the affine refinement is the pullback of the affine cover. -/
def pullbackCoverAffineRefinementObjIso (f : X ⟶ Y) (𝒰 : Y.OpenCover) (i) :
    (𝒰.affineRefinement.openCover.pullback₁ f).X i ≅ ((𝒰.X i.1).affineCover.pullback₁ (𝒰.pullbackHom f i.1)).X i.2 :=
  pullbackSymmetry _ _ ≪≫
    (pullbackRightPullbackFstIso _ _ _).symm ≪≫
      pullbackSymmetry _ _ ≪≫
        asIso (pullback.map _ _ _ _ (pullbackSymmetry _ _).hom (𝟙 _) (𝟙 _) (by simp [Cover.pullbackHom]) (by simp))

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

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

Разделы

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

Аффилиация

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