Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

feat(AlgebraicGeometry): integral = universally closed + affine #19419

Open
wants to merge 4 commits into
base: master
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
35 changes: 35 additions & 0 deletions Mathlib/Algebra/Category/Ring/Constructions.lean
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,9 @@ Authors: Andrew Yang
import Mathlib.Algebra.Category.Ring.Instances
import Mathlib.Algebra.Category.Ring.Limits
import Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
import Mathlib.CategoryTheory.Limits.Shapes.Pullback.CommSq
import Mathlib.RingTheory.TensorProduct.Basic
import Mathlib.RingTheory.IsTensorProduct

/-!
# Constructions of (co)limits in `CommRingCat`
Expand Down Expand Up @@ -102,6 +104,39 @@ def pushoutCoconeIsColimit : Limits.IsColimit (pushoutCocone R A B) :=
rw [← h.map_mul, Algebra.TensorProduct.tmul_mul_tmul, mul_one, one_mul]
rfl

lemma isPushout_of_isPushout (R S A B) [CommRing R] [CommRing S]
[CommRing A] [CommRing B] [Algebra R S] [Algebra S B] [Algebra R A] [Algebra A B] [Algebra R B]
[IsScalarTower R A B] [IsScalarTower R S B] [Algebra.IsPushout R S A B] :
IsPushout (ofHom (algebraMap R S)) (ofHom (algebraMap R A))
(ofHom (algebraMap S B)) (ofHom (algebraMap A B)) := by
refine ⟨⟨?_⟩, ⟨Limits.PushoutCocone.IsColimit.mk _ ?_ ?_ ?_ ?_⟩⟩
· exact (IsScalarTower.algebraMap_eq R S B).symm.trans (IsScalarTower.algebraMap_eq R A B)
· intro s
letI := (s.inl.comp (algebraMap R S)).toAlgebra
refine (Algebra.pushoutDesc (R := R) (S := S) (R' := A) B ⟨s.inl, ?_⟩ ⟨s.inr, ?_⟩ ?_).toRingHom
· simp [RingHom.algebraMap_toAlgebra]
· simpa [RingHom.algebraMap_toAlgebra] using DFunLike.congr_fun s.condition.symm
· exact fun _ _ ↦ Commute.all _ _
· intro s
letI := (s.inl.comp (algebraMap R S)).toAlgebra
ext x
refine Algebra.pushoutDesc_left (H := ?_) ..
exact fun _ _ ↦ Commute.all _ _
· intro s
letI := (s.inl.comp (algebraMap R S)).toAlgebra
ext x
refine Algebra.pushoutDesc_right (H := ?_) ..
exact fun _ _ ↦ Commute.all _ _
· intro s m e₁ e₂
letI := (s.inl.comp (algebraMap R S)).toAlgebra
let m' : B →ₐ[R] s.pt := ⟨m, fun r ↦
by simpa [ofHom, ← IsScalarTower.algebraMap_apply] using congr($e₁ (algebraMap R S r))⟩
show m'.toRingHom = _
congr 1
apply Algebra.IsPushout.algHom_ext (S := S) (R' := A)
· ext x; simpa using congr($e₂ x)
· ext x; simpa using congr($e₁ x)

end Pushout

section Terminal
Expand Down
63 changes: 63 additions & 0 deletions Mathlib/AlgebraicGeometry/Morphisms/Integral.lean
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,9 @@ Authors: Andrew Yang
-/
import Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
import Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
import Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
import Mathlib.RingTheory.RingHom.Integral
import Mathlib.RingTheory.PolynomialAlgebra

/-!

Expand Down Expand Up @@ -57,8 +59,69 @@ instance : IsStableUnderBaseChange @IsIntegralHom :=
instance : ContainsIdentities @IsIntegralHom :=
⟨fun X ↦ ⟨fun _ _ ↦ by simpa using RingHom.isIntegral_of_surjective _ (Equiv.refl _).surjective⟩⟩

lemma iff_of_Spec {R S : CommRingCat} {φ : R ⟶ S} :
IsIntegralHom (Spec.map φ) ↔ φ.IsIntegral := by
have := RingHom.toMorphismProperty_respectsIso_iff.mp RingHom.isIntegral_respectsIso
rw [HasAffineProperty.iff_of_isAffine (P := @IsIntegralHom), and_iff_right]
exacts [MorphismProperty.arrow_mk_iso_iff (RingHom.toMorphismProperty RingHom.IsIntegral)
(arrowIsoΓSpecOfIsAffine φ).symm, inferInstance]

instance : IsMultiplicative @IsIntegralHom where

instance (priority := 100) {X Y : Scheme.{u}} (f : X ⟶ Y) [IsIntegralHom f] :
UniversallyClosed f := by
revert X Y f ‹IsIntegralHom f›
rw [universallyClosed_eq, ← IsStableUnderBaseChange.universally_eq (P := @IsIntegralHom)]
apply universally_mono
intro X Y f
wlog hY : ∃ R, Y = Spec R
· rw [IsLocalAtTarget.iff_of_openCover (P := @IsIntegralHom) Y.affineCover,
IsLocalAtTarget.iff_of_openCover (P := topologically _) Y.affineCover]
exact fun a i ↦ this _ ⟨_, rfl⟩ (a i)
obtain ⟨R, rfl⟩ := hY
wlog hX : ∃ S, X = Spec S
· intro H
have inst : IsAffine X := isAffine_of_isAffineHom f
rw [← cancel_left_of_respectsIso (P := topologically _) X.isoSpec.inv]
rw [← cancel_left_of_respectsIso (P := @IsIntegralHom) X.isoSpec.inv] at H
exact this _ _ ⟨_, rfl⟩ H
obtain ⟨S, rfl⟩ := hX
obtain ⟨φ, rfl⟩ : ∃ φ, Spec.map φ = f := ⟨_, Spec.map_preimage _⟩
rw [iff_of_Spec]
exact PrimeSpectrum.isClosedMap_comap_of_isIntegral _

lemma iff_universallyClosed_and_isAffineHom {X Y : Scheme.{u}} {f : X ⟶ Y} :
IsIntegralHom f ↔ UniversallyClosed f ∧ IsAffineHom f := by
refine ⟨fun _ ↦ ⟨inferInstance, inferInstance⟩, fun ⟨H₁, H₂⟩ ↦ ?_⟩
clear * -
wlog hY : ∃ R, Y = Spec R
· rw [IsLocalAtTarget.iff_of_openCover (P := @IsIntegralHom) Y.affineCover]
rw [IsLocalAtTarget.iff_of_openCover (P := @UniversallyClosed) Y.affineCover] at H₁
rw [IsLocalAtTarget.iff_of_openCover (P := @IsAffineHom) Y.affineCover] at H₂
exact fun _ ↦ this inferInstance inferInstance ⟨_, rfl⟩
obtain ⟨R, rfl⟩ := hY
wlog hX : ∃ S, X = Spec S
· have inst : IsAffine X := isAffine_of_isAffineHom f
rw [← cancel_left_of_respectsIso (P := @IsIntegralHom) X.isoSpec.inv]
exact this _ inferInstance inferInstance ⟨_, rfl⟩
obtain ⟨S, rfl⟩ := hX
obtain ⟨φ, rfl⟩ : ∃ φ, Spec.map φ = f := ⟨_, Spec.map_preimage _⟩
rw [iff_of_Spec]
apply PrimeSpectrum.isIntegral_of_isClosedMap_comap_mapRingHom
letI := φ.toAlgebra
letI := (Polynomial.mapRingHom φ).toAlgebra
haveI : IsScalarTower R (Polynomial R) (Polynomial S) :=
.of_algebraMap_eq' (Polynomial.mapRingHom_comp_C _).symm
refine H₁.out (Spec.map (CommRingCat.ofHom Polynomial.C))
(Spec.map (CommRingCat.ofHom Polynomial.C)) (Spec.map _)
(isPullback_Spec_map_isPushout _ _ _ _
(CommRingCat.isPushout_of_isPushout R S (Polynomial R) (Polynomial S))).flip

lemma eq_universallyClosed_inf_isAffineHom :
@IsIntegralHom = (@UniversallyClosed ⊓ @IsAffineHom : MorphismProperty Scheme) := by
ext
exact iff_universallyClosed_and_isAffineHom

end IsIntegralHom

end AlgebraicGeometry
19 changes: 15 additions & 4 deletions Mathlib/AlgebraicGeometry/Morphisms/Proper.lean
Original file line number Diff line number Diff line change
Expand Up @@ -4,15 +4,14 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Christian Merten, Andrew Yang
-/
import Mathlib.AlgebraicGeometry.Morphisms.Separated
import Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
import Mathlib.AlgebraicGeometry.Morphisms.FiniteType
import Mathlib.AlgebraicGeometry.Morphisms.Finite

/-!

# Proper morphisms

A morphism of schemes is proper if it is separated, universally closed and (locally) of finite type.
Note that we don't require quasi-compact, since this is implied by universally closed (TODO).
Note that we don't require quasi-compact, since this is implied by universally closed.

-/

Expand Down Expand Up @@ -51,7 +50,7 @@ instance : MorphismProperty.IsMultiplicative @IsProper := by
rw [isProper_eq]
infer_instance

instance (priority := 900) [IsClosedImmersion f] : IsProper f where
instance (priority := 900) [IsFinite f] : IsProper f where

instance isStableUnderBaseChange : MorphismProperty.IsStableUnderBaseChange @IsProper := by
rw [isProper_eq]
Expand All @@ -63,4 +62,16 @@ instance : IsLocalAtTarget @IsProper := by

end IsProper

lemma IsFinite.eq_isProper_inf_isAffineHom :
@IsFinite = (@IsProper ⊓ @IsAffineHom : MorphismProperty _) := by
have : (@IsAffineHom ⊓ @IsSeparated : MorphismProperty _) = @IsAffineHom :=
inf_eq_left.mpr fun _ _ _ _ ↦ inferInstance
rw [inf_comm, isProper_eq, inf_assoc, ← inf_assoc, this, eq_inf,
IsIntegralHom.eq_universallyClosed_inf_isAffineHom, inf_assoc, inf_left_comm]

lemma IsFinite.iff_isProper_and_isAffineHom :
IsFinite f ↔ IsProper f ∧ IsAffineHom f := by
rw [eq_isProper_inf_isAffineHom]
rfl

end AlgebraicGeometry
14 changes: 14 additions & 0 deletions Mathlib/RingTheory/PolynomialAlgebra.lean
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@ import Mathlib.Algebra.Polynomial.AlgebraMap
import Mathlib.Data.Matrix.Basis
import Mathlib.Data.Matrix.DMatrix
import Mathlib.RingTheory.MatrixAlgebra
import Mathlib.RingTheory.IsTensorProduct

/-!
# Algebra isomorphism between matrices of polynomials and polynomials of matrices
Expand Down Expand Up @@ -285,3 +286,16 @@ theorem support_subset_support_matPolyEquiv (m : Matrix n n R[X]) (i j : n) :
intro hk
rw [← matPolyEquiv_coeff_apply, hk]
rfl

instance {R S} [CommRing R] [CommRing S] [Algebra R S] :
letI := (mapRingHom (algebraMap R S)).toAlgebra
haveI : IsScalarTower R R[X] S[X] := .of_algebraMap_eq' (mapRingHom_comp_C _).symm
Algebra.IsPushout R S R[X] S[X] := by
letI := (mapRingHom (algebraMap R S)).toAlgebra
haveI : IsScalarTower R R[X] S[X] := .of_algebraMap_eq' (mapRingHom_comp_C _).symm
constructor
let e : S[X] ≃ₐ[S] TensorProduct R S R[X] := { __ := polyEquivTensor R S, commutes' := by simp }
convert (TensorProduct.isBaseChange R R[X] S).comp (.ofEquiv e.symm.toLinearEquiv) using 1
ext : 2
refine Eq.trans ?_ (polyEquivTensor_symm_apply_tmul R S _ _).symm
simp [RingHom.algebraMap_toAlgebra]