Theorems · Theorem · algebraic geometry

AlgebraicGeometry.exists_affineOpens_le_appLE_of_appLE

∀ {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₁ : Y.Opens) (U₂ : ↑Y.affineOpens) (V₁ : X.Opens) (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₁.carrier →
                  ∃ U' V',
                    ∃ (_ : ↑U' ≤ U₁) (_ : ↑V' ≤ V₁) (_ : x ∈ ↑V') (e :
                      ↑V' ≤ (TopologicalSpace.Opens.map f.base).obj ↑U'),
                      P (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appLE f (↑U') (↑V') e))

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

Defined in

Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Cited by

0 results in Mathlib

Foundations

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