ulift

Mathlib.AlgebraicGeometry.Cover.MorphismProperty

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

Lean4

/-- Any `v`-cover `𝒰` induces a `u`-cover indexed by the points of `X`. -/
@[simps!]
def ulift (𝒰 : Cover.{v} (precoverage P) X) : Cover.{u} (precoverage P) X
    where
  I₀ := X
  X x := 𝒰.X (𝒰.exists_eq x).choose
  f x := 𝒰.f _
  mem₀ := by
    rw [presieve₀_mem_precoverage_iff]
    refine ⟨fun x ↦ ?_, fun i ↦ 𝒰.map_prop _⟩
    use x, (𝒰.exists_eq x).choose_spec.choose, (𝒰.exists_eq x).choose_spec.choose_spec

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

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

Разделы

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

Аффилиация

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