feat: make projective space #635
Conversation
kbuzzard
left a comment
kbuzzard
left a comment
There was a problem hiding this comment.
This is fine for FLT but for mathlib I suspect we want the (correct, not Hartshorne) concept of a projective morphism, which is explained in https://stacks.math.columbia.edu/tag/01W7 and which needs a slightly more general construction.
| ## Main definitions | ||
|
|
||
| - `AlgebraicGeometry.ProjectiveSpace`: `ℙ(n; S)` is the projective `n`-space over `S`. | ||
| - `AlgebraicGeometry.ProjectiveSpace.SpecIso`: `ℙ(n; Spec R) ≅ Proj R[n]` |
There was a problem hiding this comment.
Whatever the notation R[n] is supposed to mean, it's very hard to guess that it means something like "multivariable polynomials in n+1 variables"
| {CC : C → Type w} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory C FC] | ||
| {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (x : CC X) : | ||
| (f ≫ g) x = g (f x) := | ||
| congr_fun (hom_comp f g) x |
There was a problem hiding this comment.
This is ConcreteCategory.comp_apply f g x
| IsLocalization.Away ((contract R i) (expand R i p)) (Localization.Away p) := by | ||
| rw [contract_expand]; infer_instance | ||
|
|
||
| /-- The isomorphism between the natural `R[n](1/XᵢXⱼ)₀` and our model `R[{Xₖ // k ≠ i}, 1/Xⱼ]`. -/ |
There was a problem hiding this comment.
| /-- The isomorphism between the natural `R[n](1/XᵢXⱼ)₀` and our model `R[{Xₖ // k ≠ i}, 1/Xⱼ]`. -/ | |
| /-- The ring isomorphism between the natural `R[n](1/XᵢXⱼ)₀` and our model `R[{Xₖ // k ≠ i}, 1/Xⱼ]`. | |
| See also `MvPolynomial.algEquivAwayMul` for the `R`-algebra isomorphism. -/ |
| IsLocalization.Away (dehomogenise j (X (R:=R) i)) (away₂ R i j) := | ||
| IsLocalization.isLocalization_of_algEquiv _ (away₂CommAlgEquiv R i j).symm | ||
|
|
||
| end MvPolynomial |
There was a problem hiding this comment.
Whilst this is clearly a tour de force, I feel like all of this stuff could be avoided if you instead make P(vector space) and cover it by affines indexed by elements phi in the dual space, where the affine parametrises lines which are not in the kernel of phi, and then just apply it to a vector space with a basis if you want usual P^n.
| /- open CategoryTheory.Limits TensorProduct | ||
|
|
||
| /-- `Spec R ⨯ Spec S ≅ Spec (R ⊗[ℤ] S)`, using pullback to replace product. -/ | ||
| noncomputable def pullbackTerminalSpecIso (R S : Type u) [CommRing R] [CommRing S] : | ||
| pullback (terminal.from (Spec (.of R))) (terminal.from (Spec (.of S))) ≅ | ||
| Spec (.of (R ⊗[ℤ] S)) := | ||
| pullback.iso' (Iso.refl _) (Iso.refl _) (specULiftZIsTerminal.uniqueUpToIso terminalIsTerminal) | ||
| (terminal.hom_ext ..) (terminal.hom_ext ..) ≪≫ | ||
| pullbackSpecIso (ULift.{u} ℤ) R S ≪≫ | ||
| Scheme.Spec.mapIso (RingEquiv.toCommRingCatIso <| RingEquivClass.toRingEquiv <| | ||
| Algebra.TensorProduct.equivOfCompatibleSMul ..).op -/ |
There was a problem hiding this comment.
Do you want this or should we delete it?
| /- GOALS | ||
| * Subspace cut out by a polynomial | ||
| * Locally (i.e. at stalk) points given by [x₀ : ... : xₙ] | ||
| -/ |
There was a problem hiding this comment.
If these are TODO then can you put them in the module docstrincg?
|
awaiting-author |
2 participants
Projective space
Main definitions
AlgebraicGeometry.ProjectiveSpace:ℙ(n; S)is the projectiven-space overS.AlgebraicGeometry.ProjectiveSpace.SpecIso:ℙ(n; Spec R) ≅ Proj R[n]AlgebraicGeometry.ProjectiveSpace.openCover: the canonical cover ofℙ(n; S)bynaffinecharts. The
iᵗʰ chart is𝔸({k // k ≠ i}; S) ⟶ ℙ(n; S), and represents the open set wherethe function
Xᵢdoes not vanish.(This is not perfect, but I'm happy for this to be merged first, and then I'll take a short break and start cleaning up stuffs)
Note: the main file starts as L890; the things before that are things to be moved to other files (I'll split them into PR's into mathlib)