AlgebraicGeometry.isIntegral_of_smooth_of_geometricallyConnected
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs.isIntegral_of_smooth_of_geometricallyConnected
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometryLean source · statement
theorem _root_.AlgebraicGeometry.isIntegral_of_smooth_of_geometricallyConnected
(k : Type u) [Field k] [IsAlgClosed k] {X : Scheme.{u}} (t : X ⟶ Spec (CommRingCat.of k))
(hsm : Smooth t) (hgc : GeometricallyConnected t)
(e : Spec (CommRingCat.of k) ⟶ X) (_he : e ≫ t = 𝟙 _) :
IsIntegral X