AlgebraicGeometry.ext_of_forall_comp_eq_of_isAlgClosed
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.ext_of_forall_comp_eq_of_isAlgClosed
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe uLean source · statement
theorem _root_.AlgebraicGeometry.ext_of_forall_comp_eq_of_isAlgClosed
{κ : Type u} [Field κ] [IsAlgClosed κ] {X Y : Scheme.{u}}
(fX : X ⟶ Spec (CommRingCat.of κ)) (fY : Y ⟶ Spec (CommRingCat.of κ))
[LocallyOfFiniteType fX] [IsReduced X] [IsSeparated fY]
{f g : X ⟶ Y} (hf : f ≫ fY = fX) (hg : g ≫ fY = fX)
(h : ∀ x : Spec (CommRingCat.of κ) ⟶ X, x ≫ fX = 𝟙 _ → x ≫ f = x ≫ g) :
f = g