Theorems · Theorem · algebraic geometry

AlgebraicGeometry.StructureSheaf.toOpen_comp_comap

∀ {R : Type u} [inst : CommRing R] {S : Type u} [inst_1 : CommRing S] (f : R →+* S)
  (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)),
  CategoryTheory.CategoryStruct.comp
      (CommRingCat.ofHom (algebraMap R ↑((AlgebraicGeometry.Spec.structureSheaf R).obj.obj (Opposite.op U))))
      (CommRingCat.ofHom
        (AlgebraicGeometry.StructureSheaf.comap f U
          ((TopologicalSpace.Opens.comap { toFun := PrimeSpectrum.comap f, continuous_toFun := ⋯ }) U) ⋯)) =
    CategoryTheory.CategoryStruct.comp (CommRingCat.ofHom f)
      (CommRingCat.ofHom
        (algebraMap S
          ↑((AlgebraicGeometry.Spec.structureSheaf S).obj.obj
              (Opposite.op
                ((TopologicalSpace.Opens.comap { toFun := PrimeSpectrum.comap f, continuous_toFun := ⋯ }) U)))))

Defined in

Mathlib.AlgebraicGeometry.StructureSheaf

Cited by

3 results in Mathlib

Foundations

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

Assumes

CommRingCommRing