mathlib4 feat(AlgebraicGeometry/Limits): Coproducts of Schemes

trafficstars

Jul 04 '24 21:07 erdOne

PR summary b016b187bd

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ IsOpenImmersion.of_isLocalization + disjointGlueData + disjointGlueData' + disjoint_opensRange_sigmaι + exists_sigmaι_eq + iSup_opensRange_sigmaι + instance (i) : IsOpenImmersion (Sigma.ι f i) := by + instance : CreatesColimit (Discrete.functor f) Scheme.forgetToLocallyRingedSpace + instance : CreatesColimitsOfShape (Discrete ι) Scheme.forgetToLocallyRingedSpace := by + instance : HasCoproducts.{0} Scheme.{u} := has_smallest_coproducts_of_hasCoproducts + instance : HasCoproducts.{u} Scheme.{u} + instance : PreservesColimitsOfShape (Discrete ι) Scheme.forgetToTop + instance {R} [CommRing R] (f : R) : + instance {ι : Type} : PreservesColimitsOfShape (Discrete ι) Scheme.forgetToLocallyRingedSpace + instance {ι : Type} : PreservesColimitsOfShape (Discrete ι) Scheme.forgetToTop + sigmaIsoGlued + sigmaMk + sigmaMk_mk + sigmaOpenCover + sigmaι_eq_iff + toLocallyRingedSpaceCoproductCofan + toLocallyRingedSpaceCoproductCofanIsColimit + ι_sigmaIsoGlued_hom + ι_sigmaIsoGlued_inv

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

Jul 04 '24 21:07 github-actions[bot]

What do you think of including something like the following, to golf the disjoint union proof?

structure GlueData' where
  J : Type v
  U : J → C
  V : J × J → C
  f : ∀ i j, V (i, j) ⟶ U i
  f_mono : ∀ i j, Mono (f i j) := by infer_instance
  f_hasPullback : ∀ i j k, HasPullback (f i j) (f i k) := by infer_instance
  f_id : ∀ i, IsIso (f i i) := by infer_instance
  t : ∀ i j, V (i, j) ⟶ V (j, i)
  t_id : ∀ i, t i i = 𝟙 _
  t' : ∀ i j k, pullback (f i j) (f i k) ⟶ pullback (f j k) (f j i)
  t_fac : ∀ i j k, t' i j k ≫ pullback.snd = pullback.fst ≫ t i j
  t_inv' : ∀ i j, i ≠ j → t i j ≫ t j i = 𝟙 _
  cocycle : ∀ i j k, i ≠ j → j ≠ k → k ≠ i → t' i j k ≫ t' j k i ≫ t' k i j = 𝟙 _

namespace GlueData'

attribute [simp] t_id
attribute [instance] f_id f_mono f_hasPullback
attribute [reassoc] t_fac cocycle

variable {C}
variable (D : GlueData' C)

@[simp]
theorem t'_iij (i j : D.J) : D.t' i i j = (pullbackSymmetry _ _).hom := by
  have eq₁ := D.t_fac i i j
  have eq₂ := (IsIso.eq_comp_inv (D.f i i)).mpr (@pullback.condition _ _ _ _ _ _ (D.f i j) _)
  rw [D.t_id, Category.comp_id, eq₂] at eq₁
  have eq₃ := (IsIso.eq_comp_inv (D.f i i)).mp eq₁
  rw [Category.assoc, ← pullback.condition, ← Category.assoc] at eq₃
  exact
    Mono.right_cancellation _ _
      ((Mono.right_cancellation _ _ eq₃).trans (pullbackSymmetry_hom_comp_fst _ _).symm)

theorem t'_jii (i j : D.J) : D.t' j i i = pullback.fst ≫ D.t j i ≫ inv pullback.snd := by
  rw [← Category.assoc, ← D.t_fac]
  simp

theorem t'_iji (i j : D.J) : D.t' i j i = pullback.fst ≫ D.t i j ≫ inv pullback.snd := by
  rw [← Category.assoc, ← D.t_fac]
  simp

@[reassoc, elementwise (attr := simp)]
theorem t_inv (i j : D.J) : D.t i j ≫ D.t j i = 𝟙 _ := by
  by_cases h : i = j
  · subst h
    simp
  · exact D.t_inv' _ _ h

theorem t'_inv (i j k : D.J) :
    D.t' i j k ≫ (pullbackSymmetry _ _).hom ≫ D.t' j i k ≫ (pullbackSymmetry _ _).hom = 𝟙 _ := by
  rw [← cancel_mono (pullback.fst : pullback (D.f i j) (D.f i k) ⟶ _)]
  simp [t_fac, t_fac_assoc]

instance t_isIso (i j : D.J) : IsIso (D.t i j) :=
  ⟨⟨D.t j i, D.t_inv _ _, D.t_inv _ _⟩⟩

-- instance t'_isIso (i j k : D.J) : IsIso (D.t' i j k) :=
--   ⟨⟨D.t' j k i ≫ D.t' k i j, D.cocycle _ _ _, by simpa using D.cocycle _ _ _⟩⟩

def glueData (D : GlueData' C) : GlueData C where
  __ := D
  cocycle i j k := by
    dsimp
    by_cases hij : i = j
    · subst hij
      rw [D.t'_iij, D.t'_jii, D.t'_iji]
      ext
      · simp [fst_eq_snd_of_mono_eq, t_inv_assoc]
      · simp [fst_eq_snd_of_mono_eq]
    by_cases hjk : j = k
    · subst hjk
      rw [D.t'_iij, D.t'_jii, D.t'_iji]
      ext
      · simp [fst_eq_snd_of_mono_eq, t_inv_assoc]
      · simp [fst_eq_snd_of_mono_eq]
    by_cases hki : k = i
    · subst hki
      rw [D.t'_iij, D.t'_jii, D.t'_iji]
      ext
      · simp [fst_eq_snd_of_mono_eq, t_inv_assoc]
      · rw [← cancel_mono (D.f k k)]
        simp [fst_eq_snd_of_mono_eq, t_inv_assoc, pullback.condition]
    exact D.cocycle i j k hij hjk hki

end GlueData'

Jul 05 '24 07:07 jcommelin

GlueData' is indeed useful; my GlueData.mk₂ is a baby version of it. But maybe we can add the i ≠ j conditions to V, f, f_mono, f_hasPullback, t, t', t_fac and get rid of f_id and t_id?

Jul 05 '24 15:07 alreadydone

Hmmm, then the data becomes a dependent function... and we would get even more if then elses everywhere. I suppose it could work...

At least, I think we can consider splitting the data into a structure (maybe this can be called GlueData?) and then different kinds of ways to check the axioms can be put on top of that.

Jul 05 '24 16:07 jcommelin

I'll try out the approach Johan mentioned. GlueData.mk₂ is definitely useful, but I don't think we should introduce if then else everywhere.

Jul 06 '24 02:07 erdOne

After some more thought, I think GlueData' is only useful when i = j and i =/= j need different approaches, so maybe adding i ≠ j in the data makes sense as well.

Jul 06 '24 02:07 erdOne

There is quite a lot going on in this PR. I see at least four contributions:

GlueData'
Disjoint unions of schemes.
Disjoint unions of prime spectra.
General API about pullbacks/pushouts/strict initials.

It would be much easier to review this important work if you could break up this PR into smaller pieces.

Jul 08 '24 16:07 adamtopaz

This PR/issue depends on:

~~leanprover-community/mathlib4#14548~~
~~leanprover-community/mathlib4#14549~~
~~leanprover-community/mathlib4#14550~~
~~leanprover-community/mathlib4#14551~~ By Dependent Issues (🤖). Happy coding!