Theorems · Theorem · algebraic geometry

AlgebraicGeometry.HasAffineProperty.diagonal_of_openCover

∀ (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) {Q : AlgebraicGeometry.AffineTargetMorphismProperty}
  [AlgebraicGeometry.HasAffineProperty P Q] {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (𝒰 : Y.OpenCover)
  [inst : ∀ (i : 𝒰.I₀), AlgebraicGeometry.IsAffine (𝒰.X i)]
  (𝒰' : (i : 𝒰.I₀) → (CategoryTheory.Limits.pullback f (𝒰.f i)).OpenCover)
  [inst_1 : ∀ (i : 𝒰.I₀) (j : (𝒰' i).I₀), AlgebraicGeometry.IsAffine ((𝒰' i).X j)],
  (∀ (i : 𝒰.I₀) (j k : (𝒰' i).I₀),
      Q
        (CategoryTheory.Limits.pullback.mapDesc ((𝒰' i).f j) ((𝒰' i).f k)
          (AlgebraicGeometry.Scheme.Cover.pullbackHom 𝒰 f i))) →
    P.diagonal f

Defined in

Mathlib.AlgebraicGeometry.Morphisms.Constructors

Cited by

2 results in Mathlib

Foundations

Depth 178 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AlgebraicGeometry.HasAffinePropertyAlgebraicGeometry.IsAffineAlgebraicGeometry.IsAffine