Theorems · Theorem · algebraic geometry

AlgebraicGeometry.StructureSheaf.isLocalizedModule_toPushforwardStalkAlgHom_aux

∀ (R S : CommRingCat) (p : PrimeSpectrum ↑R) [inst : Algebra ↑R ↑S]
  (y :
    ↑(((TopCat.Presheaf.pushforward CommRingCat
                (AlgebraicGeometry.Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
            (AlgebraicGeometry.Spec.structureSheaf ↑S).obj).stalk
        p)),
  ∃ x, x.2 • y = (AlgebraicGeometry.StructureSheaf.toPushforwardStalkAlgHom R S p) x.1

Defined in

Mathlib.AlgebraicGeometry.Spec

Cited by

0 results in Mathlib

Foundations

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

Assumes

Algebra