feat(AlgebraicGeometry/AffineSpace): affine space is smooth

Mathlib/AlgebraicGeometry/AffineSpace.lean

@@ -5,11 +5,8 @@ Authors: Andrew Yang
 -/
 module
 
-public import Mathlib.Algebra.MvPolynomial.Monad
 public import Mathlib.AlgebraicGeometry.Morphisms.Finite
-public import Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
-public import Mathlib.RingTheory.Spectrum.Prime.Polynomial
-public import Mathlib.AlgebraicGeometry.PullbackCarrier
+public import Mathlib.AlgebraicGeometry.Morphisms.Smooth
 
 /-!
 # Affine space
@@ -370,14 +367,26 @@ instance : Surjective (𝔸(n; S) ↘ S) := MorphismProperty.pullback_fst _ _ <|
     MorphismProperty.cancel_right_of_respectsIso (P := @Surjective)]
   exact ⟨MvPolynomial.comap_C_surjective⟩
 
-instance [Finite n] : LocallyOfFinitePresentation (𝔸(n; S) ↘ S) :=
+variable (n) in
+/-- The affine `n`-space over `S` is smooth of relative dimension `Nat.card n`. -/
+instance smoothOfRelativeDimension [Finite n] :
+    SmoothOfRelativeDimension (Nat.card n) (𝔸(n; S) ↘ S) :=
   MorphismProperty.pullback_fst _ _ <| by
   have := isIso_of_isTerminal specULiftZIsTerminal.{max u v} terminalIsTerminal (terminal.from _)
   rw [← terminal.comp_from (Spec.map (CommRingCat.ofHom C)),
-    MorphismProperty.cancel_right_of_respectsIso (P := @LocallyOfFinitePresentation),
-    HasRingHomProperty.Spec_iff (P := @LocallyOfFinitePresentation), RingHom.FinitePresentation]
-  convert! (inferInstance : Algebra.FinitePresentation (ULift ℤ) ℤ[n])
-  exact Algebra.algebra_ext _ _ fun _ ↦ rfl
+    MorphismProperty.cancel_right_of_respectsIso (P := @SmoothOfRelativeDimension _),
+    HasRingHomProperty.Spec_iff (P := @SmoothOfRelativeDimension _)]
+  apply RingHom.locally_of RingHom.isStandardSmoothOfRelativeDimension_respectsIso
+  simp_rw [ConcreteCategory.hom_ofHom, ← MvPolynomial.algebraMap_eq,
+    RingHom.isStandardSmoothOfRelativeDimension_algebraMap]
+  exact Algebra.IsStandardSmoothOfRelativeDimension.mvPolynomial _ _
+
+/-- The affine `n`-space (indexed by `Fin n`) over `S` is smooth of relative dimension `n`. -/
+instance smoothOfRelativeDimension_fin {S : Scheme.{u}} (n : ℕ) :
+    SmoothOfRelativeDimension n (𝔸(Fin n; S) ↘ S) := by
+  simpa using smoothOfRelativeDimension (Fin n) S
+
+instance [Finite n] : Smooth (𝔸(n; S) ↘ S) := (smoothOfRelativeDimension n S).smooth
 
 lemma isOpenMap_over : IsOpenMap (𝔸(n; S) ↘ S) := by
   change topologically @IsOpenMap _

Mathlib/AlgebraicGeometry/Morphisms/Smooth.lean

@@ -163,7 +163,7 @@ instance : HasRingHomProperty (@SmoothOfRelativeDimension n)
     grind [Scheme.affineOpens]
 
 /-- Smooth of relative dimension `n` is stable under base change. -/
-lemma smoothOfRelativeDimension_isStableUnderBaseChange :
+instance smoothOfRelativeDimension_isStableUnderBaseChange :
     MorphismProperty.IsStableUnderBaseChange (@SmoothOfRelativeDimension n) :=
   HasRingHomProperty.isStableUnderBaseChange <| locally_isStableUnderBaseChange
     isStandardSmoothOfRelativeDimension_respectsIso

Mathlib/RingTheory/Extension/Presentation/Basic.lean

@@ -198,6 +198,20 @@ noncomputable def id : Presentation R R PEmpty.{w + 1} PEmpty.{t + 1} :=
 lemma id_dimension : (Presentation.id R).dimension = 0 :=
   ofBijectiveAlgebraMap_dimension (R := R) Function.bijective_id
 
+variable (R ι) in
+/-- The canonical `R`-presentation of the polynomial algebra `MvPolynomial ι R`,
+with generators `X` indexed by `ι` and no relations. -/
+@[simps -fullyApplied relation]
+noncomputable def mvPolynomial : Presentation R (MvPolynomial ι R) ι PEmpty.{t + 1} where
+  relation := PEmpty.elim
+  span_range_relation_eq_ker := by
+    simpa only [Generators.ker_mvPolynomial, Set.range_eq_empty] using Ideal.span_empty
+  __ := Generators.mvPolynomial R ι
+
+@[simp]
+lemma dimension_mvPolynomial : (mvPolynomial R ι).dimension = Nat.card ι := by
+  simp [dimension]
+
 section Localization
 
 variable (r : R) [IsLocalization.Away r S]

Mathlib/RingTheory/Extension/Presentation/Submersive.lean

@@ -223,6 +223,20 @@ lemma ofBijectiveAlgebraMap_jacobian (h : Function.Bijective (algebraMap R S)) :
     contradiction
   rw [jacobian_eq_jacobiMatrix_det, RingHom.map_det, this, Matrix.det_one]
 
+variable (R ι) in
+/-- The canonical pre-submersive `R`-presentation of the polynomial algebra `MvPolynomial ι R`,
+with generators `X` indexed by `ι` and no relations. -/
+@[simps -fullyApplied map]
+noncomputable def mvPolynomial :
+    PreSubmersivePresentation R (MvPolynomial ι R) ι PEmpty.{t + 1} where
+  map := PEmpty.elim
+  map_inj := PEmpty.elim.injective_of_subsingleton
+  __ := Presentation.mvPolynomial R ι
+
+@[simp]
+lemma jacobian_mvPolynomial : (mvPolynomial R ι).jacobian = 1 := by
+  rw [jacobian_eq_jacobiMatrix_det, Matrix.det_isEmpty, map_one]
+
 section Localization
 
 variable (r : R) [IsLocalization.Away r S]
@@ -530,6 +544,11 @@ noncomputable def ofBijectiveAlgebraMap (h : Function.Bijective (algebraMap R S)
 noncomputable def id : SubmersivePresentation R R PEmpty.{w + 1} PEmpty.{t + 1} :=
   ofBijectiveAlgebraMap Function.bijective_id
 
+/-- The canonical submersive `R`-presentation of the polynomial algebra `MvPolynomial ι R`. -/
+noncomputable def mvPolynomial : SubmersivePresentation R (MvPolynomial ι R) ι PEmpty.{t + 1} where
+  __ := PreSubmersivePresentation.mvPolynomial R ι
+  jacobian_isUnit := by simp
+
 section Composition
 variable {R S ι σ}
 variable {T ι' σ' : Type*} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T]

Mathlib/RingTheory/Smooth/Basic.lean

@@ -111,8 +111,6 @@ lemma FormallySmooth.comp_surjective [FormallySmooth R A] (I : Ideal B) (hI : I
     simpa using! (Function.surjInv_eq _ _).symm
   exact ⟨l.comp g, by rw [← AlgHom.comp_assoc, ← this, AlgHom.comp_assoc, hg, AlgHom.comp_id]⟩
 
-set_option backward.defeqAttrib.useBackward true in
-set_option backward.isDefEq.respectTransparency false in
 instance instFormallySmoothMvPolynomial (σ : Type*) : FormallySmooth R (MvPolynomial σ R) := by
   let P := Generators.mvPolynomial R σ
   have : Subsingleton ↥P.toExtension.ker :=

Mathlib/RingTheory/Smooth/StandardSmooth.lean

@@ -115,6 +115,20 @@ instance IsStandardSmoothOfRelativeDimension.id :
     IsStandardSmoothOfRelativeDimension 0 R R :=
   IsStandardSmoothOfRelativeDimension.of_algebraMap_bijective Function.bijective_id
 
+variable (R) in
+/-- The polynomial algebra `MvPolynomial ι R` is standard smooth over `R` of relative
+dimension `Nat.card ι`. -/
+lemma IsStandardSmoothOfRelativeDimension.mvPolynomial [Finite ι] :
+    IsStandardSmoothOfRelativeDimension (Nat.card ι) R (MvPolynomial ι R) :=
+  (SubmersivePresentation.mvPolynomial.{0} R ι).isStandardSmoothOfRelativeDimension
+    (Presentation.dimension_mvPolynomial)
+
+/-- The polynomial algebra `MvPolynomial (Fin n) R` is standard smooth over `R` of relative
+dimension `n`. -/
+instance IsStandardSmoothOfRelativeDimension.mvPolynomial_fin {n : ℕ} :
+    IsStandardSmoothOfRelativeDimension n R (MvPolynomial (Fin n) R) := by
+  simpa using IsStandardSmoothOfRelativeDimension.mvPolynomial R (Fin n)
+
 instance (priority := 100) IsStandardSmooth.finitePresentation [IsStandardSmooth R S] :
     FinitePresentation R S := by
   obtain ⟨_, _, _, _, ⟨P⟩⟩ := ‹IsStandardSmooth R S›