AlgebraicGeometry.Scheme.Hom.mem_smoothLocus_of_flat_of_smoothOfRelativeDimension_pullback_snd
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicGeometry.Scheme.Hom
universe u
open _root_.AlgebraicCurves.Geometry.Schemes.Proofs in
open Scheme_Hom_mem_smoothLocus_of_flat_of_smoothOfRelativeDimension_pullback_snd in
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry inLean source · statement
theorem mem_smoothLocus_of_flat_of_smoothOfRelativeDimension_pullback_snd
{R : Type u} [CommRing R] {X : Scheme.{u}} (c : X ⟶ Spec (CommRingCat.of R))
[LocallyOfFinitePresentation c]
(U : X.Opens) [Flat (U.ι ≫ c)] {k : Type u} [Field k] (x : Spec (CommRingCat.of k) ⟶ Spec
(CommRingCat.of R))
(h : SmoothOfRelativeDimension 1 (pullback.snd (U.ι ≫ c) x))
(y : X) (hy : y ∈ U) (hyx : (⟨y, hy⟩ : (U : Scheme.{u})) ∈ Set.range (pullback.fst (U.ι ≫ c)
x).base) :
y ∈ c.smoothLocus