Theorems · Theorem · algebraic geometry

AlgebraicGeometry.StructureSheaf.comap_comp

∀ {R : Type u} [inst : CommRing R] {S : Type u} [inst_1 : CommRing S] {P : Type u} [inst_2 : CommRing P] (f : R →+* S)
  (g : S →+* P) (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R))
  (V : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top S))
  (W : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top P)) (hUV : ∀ p ∈ V, PrimeSpectrum.comap f p ∈ U)
  (hVW : ∀ p ∈ W, PrimeSpectrum.comap g p ∈ V),
  AlgebraicGeometry.StructureSheaf.comap (g.comp f) U W ⋯ =
    (AlgebraicGeometry.StructureSheaf.comap g V W hVW).comp (AlgebraicGeometry.StructureSheaf.comap f U V hUV)

Defined in

Mathlib.AlgebraicGeometry.StructureSheaf

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingCommRingCommRing