AlgebraicGeometry.FormallyUnramified.eq_of_comp_eq_of_isLocalRing
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.FormallyUnramified_eq_of_comp_eq_of_isLocalRing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometryLean source · statement
theorem _root_.AlgebraicGeometry.FormallyUnramified.eq_of_comp_eq_of_isLocalRing
{X Y : Scheme.{u}} (f : X ⟶ Y) [FormallyUnramified f] [LocallyOfFiniteType f]
{O : Type u} [CommRing O] [IsLocalRing O]
(a b : Spec (CommRingCat.of O) ⟶ X) (hf : a ≫ f = b ≫ f)
{T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of O))
(ht : IsLocalRing.closedPoint O ∈ Set.range t.base)
(hab : t ≫ a = t ≫ b) : a = b