𝒰D₀

Mathlib.AlgebraicGeometry.AffineTransitionLimit

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.ExistsHomHomCompEqCompAux.𝒰D₀

Lean4

/-- (Implementation)
The covering of `D(i')` by the pullback of the diagonal components of `X ×ₛ X`.
See the section docstring. -/
noncomputable def 𝒰D₀ : Scheme.OpenCover.{u} (D.obj A.i') :=
  Scheme.Cover.mkOfCovers (Σ i : A.𝒰S.I₀, (A.𝒰X i).I₀) _
    (fun i ↦ ((Scheme.Pullback.diagonalCover f A.𝒰S A.𝒰X).pullback₁ A.g).f ⟨i.1, i.2, i.2⟩)
    (fun x ↦ by
      simpa [← Set.mem_range, Scheme.Pullback.range_fst, Scheme.Pullback.diagonalCoverDiagonalRange] using
        A.range_g_subset ⟨x, rfl⟩)

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

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

Разделы

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

Аффилиация

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