Theorems · Theorem · algebraic geometry

AlgebraicGeometry.StructureSheaf.comap_const

∀ {R : Type u} [inst : CommRing R] {S : Type u} [inst_1 : CommRing S] (f : R →+* S)
  (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R))
  (V : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top S))
  (hUV : V.carrier ⊆ PrimeSpectrum.comap f ⁻¹' U.carrier) (a b : R) (hb : ∀ x ∈ U, b ∈ x.asIdeal.primeCompl),
  (AlgebraicGeometry.StructureSheaf.comap f U V hUV) (AlgebraicGeometry.StructureSheaf.const a b U hb) =
    AlgebraicGeometry.StructureSheaf.const (f a) (f b) V ⋯

Defined in

Mathlib.AlgebraicGeometry.StructureSheaf

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingCommRing