openCoverOfRight

Mathlib.AlgebraicGeometry.Pullbacks

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

Lean4

/-- Given an open cover `{ Yᵢ }` of `Y`, then `X ×[Z] Y` is covered by `X ×[Z] Yᵢ`. -/
@[simps! I₀ X f]
def openCoverOfRight (𝒰 : OpenCover Y) (f : X ⟶ Z) (g : Y ⟶ Z) : OpenCover (pullback f g) :=
  by
  fapply
    ((openCoverOfLeft 𝒰 g f).pushforwardIso (pullbackSymmetry _ _).hom).copy 𝒰.I₀ (fun i => pullback f (𝒰.f i ≫ g))
      (fun i => pullback.map _ _ _ _ (𝟙 _) (𝒰.f i) (𝟙 _) (by simp) (Category.comp_id _)) (Equiv.refl _) fun i =>
      pullbackSymmetry _ _
  intro i
  dsimp
  apply pullback.hom_ext <;> simp

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

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

Разделы

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

Аффилиация

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