Theorems · Theorem · algebraic geometry

AlgebraicGeometry.StructureSheaf.comap_id

∀ {R : Type u} [inst : CommRing R] {U V : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)}
  (hUV : U = V),
  AlgebraicGeometry.StructureSheaf.comap (RingHom.id R) U V ⋯ = CommRingCat.Hom.hom (CategoryTheory.eqToHom ⋯)

The comap of the identity is the identity. In this variant of the lemma, two open subsets U and V are given as arguments, together with a proof that U = V. This is useful when U and V are not definitionally equal.

Defined in

Mathlib.AlgebraicGeometry.StructureSheaf

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRing