Theorems · Theorem · algebraic geometry

AlgebraicGeometry.isAffineHom_diagonal_iff

∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y},
  AlgebraicGeometry.IsAffineHom (CategoryTheory.Limits.pullback.diagonal f) ↔
    ∀ (U : Y.Opens),
      AlgebraicGeometry.IsAffineOpen U →
        ∀ V₁ ≤ (TopologicalSpace.Opens.map f.base).obj U,
          ∀ V₂ ≤ (TopologicalSpace.Opens.map f.base).obj U,
            AlgebraicGeometry.IsAffineOpen V₁ →
              AlgebraicGeometry.IsAffineOpen V₂ → AlgebraicGeometry.IsAffineOpen (V₁ ⊓ V₂)

Defined in: Mathlib.AlgebraicGeometry.Morphisms.Affine
Cited by: 1 results in Mathlib
Foundations: Depth 182 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites37

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Quiver.Homstatement and proof · cited by 32,603
CategoryTheory.Functor.objstatement and proof · cited by 19,642
Set.Elemproof · cited by 7,166
Set.ofPredproof · cited by 6,101
TopCat.carrierstatement · cited by 3,184
LE.le.transproof · cited by 3,151
AlgebraicGeometry.Schemestatement and proof · cited by 2,540
CommRingCatstatement · cited by 2,333
TopologicalSpace.Opensstatement · cited by 2,040
AlgebraicGeometry.PresheafedSpace.carrierstatement · cited by 2,020
AlgebraicGeometry.SheafedSpace.toPresheafedSpacestatement · cited by 1,988
AlgebraicGeometry.LocallyRingedSpace.toSheafedSpacestatement · cited by 1,892

Cited by1

Results whose statement or proof uses this declaration.

AlgebraicGeometry.IsAffineOpen.infproof · cited by 2