diagonal

Mathlib.AlgebraicGeometry.Morphisms.Constructors

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.AffineTargetMorphismProperty.diagonal

Lean4

/-- The `AffineTargetMorphismProperty` associated to `(targetAffineLocally P).diagonal`.
See `diagonal_targetAffineLocally_eq_targetAffineLocally`.
-/
def diagonal (P : AffineTargetMorphismProperty) : AffineTargetMorphismProperty := fun {X _} f _ =>
  ∀ ⦃U₁ U₂ : Scheme⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [IsAffine U₁] [IsAffine U₂] [IsOpenImmersion f₁] [IsOpenImmersion f₂],
    P (pullback.mapDesc f₁ f₂ f)

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

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

Разделы

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

Аффилиация

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