toSigma

Mathlib.AlgebraicGeometry.Cover.Sigma

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

Lean4

/-- `𝒰` refines the single object cover defined by `𝒰`. -/
@[simps]
noncomputable def toSigma (𝒰 : Cover.{v} (precoverage P) S) : 𝒰 ⟶ 𝒰.sigma
    where
  idx _ := default
  app i := Sigma.ι _ i
  app_prop _ := IsZariskiLocalAtSource.of_isOpenImmersion _

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

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

Разделы

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

Аффилиация

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