Module

UniversallyInjective_of_forall_isAlgClosed_points_eq.lean

Nyll.AlgebraicCurves.Geometry.Schemes.UniversallyInjective_of_forall_isAlgClosed_points_eq

1 declaration indexed from sourceView source ↗

Module documentation

Universally Injective of forall is Alg Closed points eq

Imports9

Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective
Mathlib.AlgebraicGeometry.Pullbacks
Mathlib.AlgebraicGeometry.ResidueField
Mathlib.AlgebraicGeometry.Scheme
Mathlib.CategoryTheory.Limits.Shapes.Diagonal
Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
Mathlib.RingTheory.LocalRing.Basic
Mathlib.RingTheory.Spectrum.Prime.Topology

Imported by2

theorem

of_forall_isAlgClosed_points_eq

L36 ↗

AlgebraicGeometry.UniversallyInjective.of_forall_isAlgClosed_points_eq

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace UniversallyInjective_of_forall_isAlgClosed_points_eq
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry

Lean source · statement

theorem _root_.AlgebraicGeometry.UniversallyInjective.of_forall_isAlgClosed_points_eq
    {X Y : Scheme.{u}} (f : X ⟶ Y)
    (h : ∀ (K : Type u) [Field K] [IsAlgClosed K] (x y : Spec (CommRingCat.of K) ⟶ X),
      x ≫ f = y ≫ f → x = y) :
    UniversallyInjective f

Module documentation

Universally Injective of forall is Alg Closed points eq

Declarations

of_forall_isAlgClosed_points_eq