Refactor AlgebraicGeometry.Scheme.Cover

Stream: maths

[Kenny Lau]

https://github.com/leanprover-community/mathlib4/blob/ed41206fa0675952165c80b990c9fbd0f7394c85/Mathlib/AlgebraicGeometry/Cover/MorphismProperty.lean#L38-L62

structure Cover (P : MorphismProperty Scheme.{u}) (X : Scheme.{u}) where
  /-- index set of a cover of a scheme `X` -/
  J : Type v
  /-- the components of a cover -/
  obj (j : J) : Scheme
  /-- the components map to `X` -/
  map (j : J) : obj j ⟶ X
  /-- given a point of `x : X`, `f x` is the index of the component which contains `x` -/
  f (x : X) : J
  /-- the components cover `X` -/
  covers (x : X) : x ∈ Set.range (map (f x)).base
  /-- the component maps satisfy `P` -/
  map_prop (j : J) : P (map j) := by infer_instance

I think the f here being data is a bit suboptimal. Why don't we just have an exists statement? If we want the function afterwards, we can just choose it afterwards? I feel like having f be data here doesn't harmonise well with Lean's general philosophy.

[Kenny Lau]

I think a "middle road" would be an alternative constructor that doesn't need f to be data

[Kenny Lau]

aha, it already exists as Cover.mkOfCovers!

[Kenny Lau]

So it suffices for my purposes, but I won't resolve this thread yet, because I still think mk (the default constructor) and mkOfCovers should switch places.

[Kenny Lau]

Demonstration:

import Mathlib.AlgebraicGeometry.Cover.Open

universe u

open CategoryTheory

namespace AlgebraicGeometry.Scheme

/-- Given a cover of a scheme `X` by open immersions, we take the refinement which consists of
cover by affine open immersions. -/
noncomputable def Cover.affineRefinement {X : Scheme.{u}} (c : X.Cover IsOpenImmersion) :
    X.OpenCover :=
  mkOfCovers
    (J := (j : c.J) × c.obj j)
    (obj := fun j ↦ (c.obj j.fst).affineCover.obj j.snd)
    (map := fun j ↦ (c.obj j.fst).affineCover.map j.snd ≫ c.map j.fst) <| fun x ↦ by
      obtain ⟨j, x, rfl⟩ := c.exists_eq x
      obtain ⟨U, x, rfl⟩ := (c.obj j).affineCover.exists_eq x
      exact ⟨⟨j, _⟩, x, rfl⟩

end AlgebraicGeometry.Scheme

[Joël Riou]

I do not have a particular opinion on this. I believe @Christian Merten has a plan to refactor (open) coverings; he may have thought more about this.

[Christian Merten]

The original idea (due to Andrew) behind the f field of Scheme.OpenCover (which I later refactored to Scheme.Cover @IsOpenImmersion) is some more definitional control. Both Andrew and I have agreed that this never really mattered, but never went through with a refactor.

I have a different plan to refactor Scheme.Cover P though: It will soon be replaced by docs#CategoryTheory.Coverage.ZeroHypercover for the coverage induced by jointly surjective morphisms satisfying P (this will allow to unify the cover API with other geometric spaces, e.g., adic spaces and prepare for a more general notion of covers to work with topologies on schemes that are not of the form P + jointly surjective). In particular, this will get rid of the definitional f field.

So I would suggest to not touch the current Scheme.Cover API for now, because most likely it will not last long.

[Christian Merten]

Kenny Lau said:

Demonstration:

import Mathlib.AlgebraicGeometry.Cover.Open

universe u

open CategoryTheory

namespace AlgebraicGeometry.Scheme

/-- Given a cover of a scheme `X` by open immersions, we take the refinement which consists of
cover by affine open immersions. -/
noncomputable def Cover.affineRefinement {X : Scheme.{u}} (c : X.Cover IsOpenImmersion) :
    X.OpenCover :=
  mkOfCovers
    (J := (j : c.J) × c.obj j)
    (obj := fun j ↦ (c.obj j.fst).affineCover.obj j.snd)
    (map := fun j ↦ (c.obj j.fst).affineCover.map j.snd ≫ c.map j.fst) <| fun x ↦ by
      obtain ⟨j, x, rfl⟩ := c.exists_eq x
      obtain ⟨U, x, rfl⟩ := (c.obj j).affineCover.exists_eq x
      exact ⟨⟨j, _⟩, x, rfl⟩

end AlgebraicGeometry.Scheme

This exists as docs#AlgebraicGeometry.Scheme.OpenCover.affineRefinement. More generally we have docs#AlgebraicGeometry.Scheme.Cover.bind.

[Kenny Lau]

Ok, I've closed #27218, but I thought I would link it here in case it might ever be useful in the future

[Kenny Lau]

Christian Merten said:

some more definitional control

I did run into some slightly non-trivial issues due to using the definition of f (particularly defined in affineCover), which I quickly fixed by changing x to U.f x, and my impression is that any proof that uses the explicit definition of f can be "improved" to a proof not using it