Theorems · Theorem · algebraic geometry

AlgebraicGeometry.IsAffineOpen.appLE_eq_away_map

∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {U : Y.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) {V : X.Opens}
  (hV : AlgebraicGeometry.IsAffineOpen V) (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U)
  (r : ↑(Y.presheaf.obj (Opposite.op U))),
  AlgebraicGeometry.Scheme.Hom.appLE f (Y.basicOpen r)
      (X.basicOpen ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appLE f U V e)) r)) ⋯ =
    CommRingCat.ofHom
      (IsLocalization.Away.map (↑(Y.presheaf.1 (Opposite.op (Y.basicOpen r))))
        (↑(X.presheaf.1
            (Opposite.op
              (X.basicOpen ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appLE f U V e)) r)))))
        (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appLE f U V e)) r)

Defined in

Mathlib.AlgebraicGeometry.AffineScheme

Cited by

2 results in Mathlib

Foundations

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