Theorems · Theorem · algebraic geometry

AlgebraicGeometry.exists_basicOpen_le_appLE_of_appLE_of_isAffine

∀ {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} {X Y : AlgebraicGeometry.Scheme}
  {f : X ⟶ Y},
  (RingHom.StableUnderCompositionWithLocalizationAwayTarget fun {R S} [CommRing R] [CommRing S] => P) →
    (RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] => P) →
      ∀ (x : ↥X) (U₁ U₂ : ↑Y.affineOpens) (V₁ V₂ : ↑X.affineOpens),
        x ∈ ↑V₁ →
          x ∈ ↑V₂ →
            ∀ (e₂ : ↑V₂ ≤ (TopologicalSpace.Opens.map f.base).obj ↑U₂),
              P (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) →
                f x ∈ ↑U₁ →
                  ∃ r s,
                    ∃ (_ : x ∈ X.basicOpen s) (e :
                      X.basicOpen s ≤ (TopologicalSpace.Opens.map f.base).obj (Y.basicOpen r)),
                      P (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appLE f (Y.basicOpen r) (X.basicOpen s) e))

If P holds for f over affine opens U₂ of Y and V₂ of X and U₁ (resp. V₁) are open affine neighborhoods of x (resp. f.base x), then P also holds for f over some basic open of U₁ (resp. V₁).

Defined in

Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Cited by

1 results in Mathlib

Foundations

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