Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Flat.flat_of_affine_subset

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

∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [self : AlgebraicGeometry.Flat 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)).Flat

Alias of AlgebraicGeometry.Scheme.Hom.flat_appLE. Alias of AlgebraicGeometry.Flat.flat_appLE.

Defined in

Mathlib.AlgebraicGeometry.Morphisms.Flat

Cited by

0 results in Mathlib

Foundations

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

Assumes

AlgebraicGeometry.Flat