AlgebraicGeometry.finite_setOf_pullback_fst_eq_of_isClosed_singleton
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.finite_setOf_pullback_fst_eq_of_isClosed_singleton
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open scoped TensorProductLean source · statement
theorem _root_.AlgebraicGeometry.finite_setOf_pullback_fst_eq_of_isClosed_singleton
{κ Ω : Type u} [Field κ] [Field Ω] [Algebra κ Ω]
{X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of κ)) [LocallyOfFiniteType f]
(z : X) (hz : IsClosed ({z} : Set X)) :
{w : ↥(Limits.pullback f (Spec.map (CommRingCat.ofHom (algebraMap κ Ω)))) |
(Limits.pullback.fst f (Spec.map (CommRingCat.ofHom (algebraMap κ Ω)))) w = z}.Finite