Demo of Ringhom Properties to Scheme Morphism Properties

demo.lean

import Mathlib.RingTheory.RingHom.FinitePresentation
import Mathlib.RingTheory.Flat.Algebra
import Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation

/-!
Authors: Judith Ludwig, Christian Merten

Note: This only works on the mathlib branch chrisflav/finpres.2
-/

open Function Algebra AlgebraicGeometry TopologicalSpace CategoryTheory Limits

namespace Hidden

/-
Let `A` be an `R`-algebra.
-/
variable (R A : Type) [CommRing R] [CommRing A] [Algebra R A]

/-
First, define the notion for `Algebra`s
-/

/-- An algebra over a commutative semiring is `Algebra.FinitePresentation` if it is the quotient of
a polynomial ring in `n` variables by a finitely generated ideal. -/
class Algebra.FinitePresentation : Prop where
  out : ∃ (n : ℕ) (f : MvPolynomial (Fin n) R →ₐ[R] A), Surjective f ∧ f.toRingHom.ker.FG

/-
We tend to show results in this algebra form, for example:
-/

/-
Given an `A`-algebra `B`, that we also consider as an `R`-algebra.
-/
variable (B : Type) [CommRing B] [Algebra A B] [Algebra R B] [IsScalarTower R A B]

/-
If `A` is `R`-finitely presented and `B` is `A`-finitely presented, then `B` is also `R`-finitely
presented.
-/
theorem Algebra.FinitePresentation.trans [FinitePresentation R A] [FinitePresentation A B] :
    FinitePresentation R B := by
  sorry


/-
A reason for this is that for properties that are deduced from module properties, this is
very convenient, e.g.
-/
/-- An `R`-algebra `A` is flat if it is flat as `R`-module. -/
class Algebra.Flat : Prop where
  out : Module.Flat R A

end Hidden

namespace Hidden2


/-
So now, let's see how this translates to the corresponding property of morphisms
of schemes.
-/
variable {X Y : Scheme} (f : X ⟶ Y)


/-
Thanks to the framework developed by Andrew Yang, there is a convenient construction.
-/

/-
Given a property of ring homomorphisms `P : ∀ {R S} [CommRing R] [CommRing S], (R →+* S)`
-/
variable (P : ∀ {R S} [CommRing R] [CommRing S], (R →+* S) → Prop)

/-
Let's assume that `P` is invariant under composing with ring isomorphisms.
-/
variable (hP : RingHom.RespectsIso P)

/-
Then `affineLocally P` provides us with the corresponding property of morphisms of schemes.
-/
example : MorphismProperty Scheme := affineLocally P


/-
`affineLocally P` holds for `f` if and only if for each pair of affine open `U = Spec A ⊆ Y` and
`V = Spec B ⊆ f ⁻¹' U`, the ring hom `A ⟶ B` satisfies `P`.
-/
example : (affineLocally P) f ↔
    ∀ (U : Y.affineOpens) (V : X.affineOpens) (e : V.1 ≤ (Opens.map f.1.base).obj U.1),
      P (Scheme.Hom.appLe f e) :=
  affineLocally_iff_affineOpens_le hP f



/-
To use this to define finitely presented morphisms of schemes,
we need the ring hom property `P` corresponding to finitely presented algebras.
-/
variable {R A : Type} [CommRing R] [CommRing A]


/-- A ring morphism `R →+* A` is of `RingHom.FinitePresentation` if `A` is finitely presented as
`A`-algebra. -/
abbrev RingHom.FinitePresentation (f : R →+* A) : Prop :=
  @Algebra.FinitePresentation R A _ _ f.toAlgebra


/-- A morphism of schemes `f : X ⟶ Y` is locally of finite presentation if for each affine `U ⊆ Y`
and `V ⊆ f ⁻¹' U`, the induced map `Γ(Y, U) ⟶ Γ(X, V)` is of finite presentation.
-/
@[mk_iff]
class IsLocallyOfFinitePresentation (f : X ⟶ Y) : Prop where
  affineLocally_finitePresentation : (affineLocally RingHom.FinitePresentation) f

lemma isLocallyOfFinitePresentation_eq :
    @IsLocallyOfFinitePresentation = affineLocally @RingHom.FinitePresentation := by
  ext X Y f
  rw [isLocallyOfFinitePresentation_iff]

/-
indeed, `IsLocallyOfFinitePresentation` is what we think
-/
example (f : X ⟶ Y) : IsLocallyOfFinitePresentation f ↔
    ∀ (U : Y.affineOpens) (V : X.affineOpens) (e : V.1 ≤ (Opens.map f.1.base).obj U.1),
      (Scheme.Hom.appLe f e).FinitePresentation := by
  rw [isLocallyOfFinitePresentation_eq]
  rw [← affineLocally_iff_affineOpens_le RingHom.finitePresentation_respectsIso f]
  rfl

/-
And now the general API on `affineLocally` provides for example, that
we may check locally of finite presentation on an open cover:
-/
lemma IsLocallyOfFinitePresentation.openCover_iff (𝒰 : Scheme.OpenCover.{0} Y) :
    IsLocallyOfFinitePresentation f ↔
      ∀ i, IsLocallyOfFinitePresentation (pullback.snd : pullback f (𝒰.map i) ⟶ _) :=
  isLocallyOfFinitePresentation_eq.symm ▸
    RingHom.finitePresentation_is_local.is_local_affineLocally.openCover_iff f 𝒰

/-
Of course this only holds, because being finitely-presented is a sufficiently local property.
-/

/-- A property of ring homs is local if it is preserved by localizations and compositions, and for
each `{ r }` that spans `S`, we have `P (R →+* S) ↔ ∀ r, P (R →+* Sᵣ)`. -/
structure RingHom.PropertyIsLocal : Prop where
  LocalizationPreserves : RingHom.LocalizationPreserves @P
  OfLocalizationSpanTarget : RingHom.OfLocalizationSpanTarget @P
  StableUnderComposition : RingHom.StableUnderComposition @P
  HoldsForLocalizationAway : RingHom.HoldsForLocalizationAway @P

/-
This notion is about ring homs, but remember: We like to state and prove
things for `Algebra`s, not for `RingHom`s.
-/

/-
For example, we had:
-/

section

/-
Given a ring `R`, an `R`-algebra `A` and an `A`-algebra `B` ...
-/
variable (R A B : Type) [CommRing R] [CommRing A] [CommRing B] [Algebra R A]
  [Algebra A B] [Algebra R B] [IsScalarTower R A B]

/-
... and assume that `A` is `R`-finitely presented and `B` is `A`-finitely presented ...
-/
variable [FinitePresentation R A] [FinitePresentation A B]

/-
..., then `B` is also `R`-finitely presented.
-/
example : FinitePresentation R B := Algebra.FinitePresentation.trans R A B

end

/-
But we need it for ring homomorphisms! This should be straightforward, right? ...
-/

/-
Well ...
-/

/-- Being finitely-presented is stable under composition. -/
theorem finitePresentation_stableUnderComposition :
    RingHom.StableUnderComposition @RingHom.FinitePresentation := by
  introv R hf hg
  letI ins1 := RingHom.toAlgebra f
  letI ins2 := RingHom.toAlgebra g
  letI ins3 := RingHom.toAlgebra (g.comp f)
  letI ins4 : IsScalarTower R S T :=
    { smul_assoc := fun a b c => by simp [Algebra.smul_def, mul_assoc]; rfl }
  letI : Algebra.FinitePresentation R S := hf
  letI : Algebra.FinitePresentation S T := hg
  rw [RingHom.FinitePresentation]
  exact Algebra.FinitePresentation.trans R S T

/-
# Summary

To go from a commutative algebra property `Pₐ` defined for `Algebra`s, we need to take the
following steps:

- define the analogous property `Pᵣ` for `RingHom`s in terms of `Pᵣ f := Pₐ f.toAlgebra`.
- prove that `Pᵣ` is local in the sense of `RingHom.PropertyIsLocal`.
  - translate from `Pᵣ` to `Pₐ`
  - prove something meaningful about `Pₐ`
  - translate from `Pₐ` to `Pᵣ`
- define the corresponding property `Pₛ` of scheme morphisms via `AlgebraicGeometry.affineLocally`.


# Discussion

- can we go straight from `Pₐ` to `Pₛ`?
- alternatively: can we automate the translation from `Pₐ` to `Pₛ` (and back)?
- should we instead ignore the issues for now, go on and refactor later?

-/