Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.Hom.ext

∀ {X Y : AlgebraicGeometry.Scheme} {f g : X ⟶ Y} (h_base : f.base = g.base),
  (∀ (U : Y.Opens),
      CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.app f U)
          (X.presheaf.map (CategoryTheory.eqToHom ⋯).op) =
        AlgebraicGeometry.Scheme.Hom.app g U) →
    f = g

Defined in

Mathlib.AlgebraicGeometry.Scheme

Cited by

0 results in Mathlib

Foundations

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