pullbackHom

Mathlib.AlgebraicGeometry.Cover.MorphismProperty

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

Lean4

/-- The family of morphisms from the pullback cover to the original cover. -/
def pullbackHom [P.IsStableUnderBaseChange] [IsJointlySurjectivePreserving P] {X W : Scheme.{u}}
    (𝒰 : X.Cover (precoverage P)) (f : W ⟶ X) (i) [∀ x, HasPullback f (𝒰.f x)] : (𝒰.pullback₁ f).X i ⟶ 𝒰.X i :=
  pullback.snd f (𝒰.f i)

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

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

Разделы

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

Аффилиация

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