Theorems · Theorem · algebraic geometry

AlgebraicGeometry.LocallyOfFinitePresentation.finitePresentation_of_affine_subset

Deprecated since 2026-01-20Use AlgebraicGeometry.Scheme.Hom.finitePresentation_appLE instead.

∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [self : AlgebraicGeometry.LocallyOfFinitePresentation f] {U : Y.Opens},
  AlgebraicGeometry.IsAffineOpen U →
    ∀ {V : X.Opens},
      AlgebraicGeometry.IsAffineOpen V →
        ∀ (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U),
          (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appLE f U V e)).FinitePresentation

Alias of AlgebraicGeometry.Scheme.Hom.finitePresentation_appLE. Alias of AlgebraicGeometry.LocallyOfFinitePresentation.finitePresentation_appLE.

Defined in

Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation

Cited by

0 results in Mathlib

Foundations

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

Assumes

AlgebraicGeometry.LocallyOfFinitePresentation