AlgebraicGeometry.OpenImmersion.Basic

Stream: mathlib4

[Damiano Testa]

This is my first AG port. To get me started with universes, I changed PresheafedSpace.{v} to PresheafedSpace.{_,v}: is this ok? Below is more context.

universe v v₁ v₂ u

variable {C : Type u} [Category.{v} C]

/-- An open immersion of PresheafedSpaces is an open embedding `f : X ⟶ U ⊆ Y` of the underlying
spaces, such that the sheaf map `Y(V) ⟶ f _* X(V)` is an iso for each `V ⊆ U`.
-/
class PresheafedSpace.IsOpenImmersion {X Y : PresheafedSpace.{v} C} (f : X ⟶ Y) : Prop where
/-
Lean complains about the `C` in PresheafedSpace:
argument
  C
has type
  Type u : Type (u + 1)
but is expected to have type
  Type v : Type (v + 1)
-/

[Damiano Testa]

(Just to be explicit: Lean is happy with the change, I just hope that I have not changed the meaning of the class.)

[Mario Carneiro]

I think it would be better to reorder the universe args of PresheafedSpace so that this code works

[Damiano Testa]

Ok, I'll try that and see what breaks!

[Damiano Testa]

Also, there are a lot of LocallyRinged in mathlib3 with uppercase. Would it make sense to add them to the nolinting in mathport?

[Mario Carneiro]

you mean uppercaseLean3 linter?

[Mario Carneiro]

yes, use that whenever you know the original is uppercase

[Mario Carneiro]

set_option linter.uppercaseLean3 false around individual defs, sections or a whole file

[Damiano Testa]

Yes, that linter, but I did not think that you could use it in a whole file. Thanks!

[Mario Carneiro]

search for examples in mathlib

[Johan Commelin]

Before porting more AG, I think we should discuss/merge @Jujian Zhang's refactor of concrete categories

[Johan Commelin]

Or was that already done?

[Johan Commelin]

This one

feat: change ConcreteCategory.hasCoeToFun to FunLike !4#4693

[Damiano Testa]

Sure, I'll wait!

[Johan Commelin]

please review that PR if you feel like it :smiley:

[Damiano Testa]

I can try, but I have never really worked with categories in mathlib: I was hoping that working on some partly ported file with hints from neighbouring ported files would be a good entry point...

[Johan Commelin]

hmm, unfortunately AG seems not to be such a place right now. Hopefully it will be after (some form of) that PR is merged

[Joël Riou]

There are three universes involved in PresheafedSpace.{u, v, w} C, the universes u and v of the category C, and the universe w where the carrier topological space lives. In mathlib3, some definitions unnecessarily assumed w=v; it is no longer so after AlgebraicGeometry.PresheafedSpace was ported. In the mathlib4 version of this file, there are no longer any explicit universe parameters. I would think we may get rid of them also in files like OpenImmersion.Basic. Anyway, placing v explicitly in PresheafedSpace.{_, v} C just does nothing if we have declared [Category.{v} C].

[Jujian Zhang]

I have opened !4#5047 for relaxing universe constrains

[Jujian Zhang]

RingedSpace in mathlib3 only has one universe variable, so it assumed that the underlying topological space and the rings have the same universe level, should we relax this as well? If so, how can I do it without bad universe level linter complaining

[Jujian Zhang]

Probably LocallyRingedSpace couldn't be relaxed as it depends on colimit

[Joël Riou]

Yes, I think you are right: one universe parameter is enough for LocallyRingedSpace.