AlgebraicGeometry.not_isAffine_of_isProper_of_smoothOfRelativeDimension_one
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace not_isAffine_of_isProper_of_smoothOfRelativeDimension_one
open AlgebraicGeometry TopologicalSpace CategoryTheory
universe uLean source · statement
theorem _root_.AlgebraicGeometry.not_isAffine_of_isProper_of_smoothOfRelativeDimension_one
{k : Type u} [Field k] {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of k))
[IsIntegral X] [IsProper f] [SmoothOfRelativeDimension 1 f] : ¬ IsAffine X