Status of algebraic geometry

Stream: general

[Andrew Yang]

I'm a newcomer to lean, and a student studying in maths with interests towards algebraic geometry.
As the current mathlib is quite short on algebraic geometry, I am wondering what the current status is, and if there are TODOs that i can contribute to so that i can practice lean hands-on at the same time.

[Johan Commelin]

@Justus Springer currently has the most active plans for developing AG.

[Justus Springer]

@Andrew Yang that's basically how I started out as well :)
A significant part of my contributions so far have been to solve TODOs in algebraic geometry. Currently I'm trying to formalize the adjunction between Spec and the global sections functor (from locally ringed spaces). I'm following stacks. I hope I can finish this in September, after that, I probably won't have as much time for Lean as I do now.
When that's done, there are some obvious follow-ups: Defining the category of affine schemes, showing it to be contravariantly equivalent to CommRing and showing that it has products and fibre products. Then there is some gluing construction to show that schemes have fibre products as well.
Besides that, maybe it would be time to define and play around with basic properties of schemes (integral, reduced, normal, notherian,...) and morphisms (flat, smooth, affine,...). But I don't know how accessible that is. See also this discussion.

[Kevin Buzzard]

One thing I'd like to see is the definition of Proj R for R a graded ring (or, as we say here, an internally graded commutative ring). If you're more variety-y than schemey then there's always the possibility of setting up a theory of algebraic varieties too, although I'm still not really sure how it would look. Perhaps restrict to a separably closed field and define quasi-projective algebraic varieties as subspaces of projective n-space? Morphisms of quasi-projective varieties probably need to be handled via sheaves though, otherwise things get quite nasty.

[Kevin Buzzard]

A completely different idea would be to develop the concept of finite locally free group schemes over a base scheme (otherwise known as finite flat group schemes, if the base is Noetherian). This is a globalisation of group theory and there are lots of surprises, e.g. in characteristic p there is more than one group of order p, even if your base is a point. We'll need these for the proof of Fermat's Last Theorem ;-)

[Andrew Yang]

I could start trying to define Proj R by probably copying Spec.lean and modifying it.
After that, porting the definitions and the basic properties in Hartshorne II.3 also seems like an interesting
task that I could try. Though gluing schemes seems like quite a challenge to formalise.

[Andrew Yang]

Oh and may I have the write access to the mathlib repo? My username is erdOne.

[Johan Commelin]

Hmm, Proj R depends on a theory of graded rings, which I wouldn't recommend to a beginner.

[Johan Commelin]

Justus was talking about fibre products, which is a nice target, I think. So, for starters, we'll need to know that CommRing has fibred coproducts. Tensor products are defined, but I don't think this category is aware yet that is has these coproducts.

[Johan Commelin]

So that might be a nice place to start.

[Johan Commelin]

After that, define the subcategory of affine schemes, and deduce that it has fibre products.

[Adam Topaz]

docs#CommRing.colimits.has_colimits_CommRing

[Johan Commelin]

ooh, of course :smiley:

[Adam Topaz]

But of course it would be nice to have an explicit cocone for the fibered coproducts which is defeq to the tensor product

[Adam Topaz]

In my opinion, a good place to start is in constructing a gluing construction for topological spaces, which will then be useful for a gluing constrution for schemes.

[Adam Topaz]

docs#Top is the category of topological spaces, which we know has colimits (so we can glue in some sense), but we probably need an explicit construction of gluing spaces along open subsets which will be useful for gluing schemes.

[Andrew Yang]

Sure, I will start there then.
I am thinking of implementing the underlying set as the quotient set of the disjoint union, and then specifying the open sets.
Is this a good idea?

[Adam Topaz]

Yes, I think that's reasonable. But one should think carefully how to set this up. My inclination is to use the general formalism of descent data, and to use open immersions instead of open subsets. This is probably worth further discussion (maybe in the #maths stream)

[Johan Commelin]

So again, I'm not sure if this is a good "first project"

[Adam Topaz]

Johan Commelin said:

So again, I'm not sure if this is a good "first project"

You're right.

[Johan Commelin]

Defining the category of affine schemes is probably a lot easier to get started with.

[Adam Topaz]

We have the following ingredients for this:
docs#algebraic_geometry.Scheme.Spec and docs#category_theory.functor.ess_image

[Andrew Yang]

I will start working on the category of affine schemes then.
Should I assume the adjointness of Spec, or prove independently that Spec is fully faithful?

[Johan Commelin]

It would be best to coordinate with @Justus Springer, but I imagine that for affine schemes you don't need the Gamma-Spec adjunction, right?

[Johan Commelin]

Or do you mean that you want to know that $\mathcal O(\mathrm{Spec} A) \cong A$?

[Johan Commelin]

I think Justus proved that a while ago.

[Andrew Yang]

I think that need $\operatorname{Hom}(A, B) \simeq \operatorname{Hom}(\operatorname{Spec} B, \operatorname{Spec} A)$ in order to say that the category of affine schemes is equivalent to CommRing^op.
The equivalence is a direct consequence of the adjunction, but there may be a more elementary proof to it.

[Adam Topaz]

I thought we had that Spec is fully faithful in mathlib. @Justus Springer?

[Bryan Gin-ge Chen]

Andrew Yang said:

Oh and may I have the write access to the mathlib repo? My username is erdOne.

I've sent you an invite: https://github.com/leanprover-community/mathlib/invitations

[Justus Springer]

Affine schemes can definitely be defined without the Gamma-spec adjunction. It should be pretty straightforward with docs#category_theory.functor.ess_image. Still, we would need some infrastructure, like defining Spec.to_AffineScheme and also AffineScheme.Γ.

[Justus Springer]

Adam Topaz said:

I thought we had that Spec is fully faithful in mathlib. Justus Springer?

Unfortunately not. But since this follows immediately from the adjunction, I think we should wait for that.

[Andrew Yang]

Bryan Gin-ge Chen said:

Andrew Yang said:

Oh and may I have the write access to the mathlib repo? My username is erdOne.

I've sent you an invite: https://github.com/leanprover-community/mathlib/invitations

Thanks!

[Adam Topaz]

Justus Springer said:

Adam Topaz said:

I thought we had that Spec is fully faithful in mathlib. Justus Springer?

Unfortunately not. But since this follows immediately from the adjunction, I think we should wait for that.

Wouldn't proving that $\mathcal{O}(Spec(A)) = A$ be one of the steps in proving the adjunction? Full-faithfulness would follow easily from that.

[Andrew Yang]

Justus Springer said:

Adam Topaz said:

I thought we had that Spec is fully faithful in mathlib. Justus Springer?

Unfortunately not. But since this follows immediately from the adjunction, I think we should wait for that.

Sure! I will start the definitions and the infrastructures then. The equivalence to CommRing can wait.

[Justus Springer]

Adam Topaz said:

Wouldn't proving that $$\mathcal{O}(Spec(A)) = A$$ be one of the steps in proving the adjunction? Full-faithfulness would follow easily from that.

Yes. That part is more or less done, I proved the more general statement $\mathcal{O}_X(D(f))\cong A_f$ a while ago (where $X=Spec(A)$). See docs#algebraic_geometry.structure_sheaf.basic_open_iso. I never got around to specializing this to $\mathcal{O}_X(X)\cong A$ though. This seems trivial, but involves knowing that localizing a ring at units doesn't change it. This could be a nice project too @Andrew Yang .

[Justus Springer]

The reason the adjunction is taking so long by the way is that I want to do the more general version for locally ringed spaces: I.e. ${\rm Hom}(X,Spec R)\cong{\rm Hom}(R,\Gamma(X))$ for any locally ringed space $X$, not just (affine) schemes. For this, I need this lemma, which requires some generalizations to the sheaves library. Also, I had to prove that the forgetful functor CommRing ⥤ Type preserves filtered colimits (#9191). So that's the state of affairs as of now. I hope the road is clear now for the Gamma-Spec adjunction.

[Justus Springer]

@Andrew Yang If you want you could play around with proving ${\rm Hom}(A,B)\cong{\rm Hom}(Spec B, Spec A)$ as you suggested. Then you can use the things you've learned to help me with the general version :sweat_smile:

[Justus Springer]

So there is definitely enough work to do...

[Adam Topaz]

Just for fun:

import group_theory.monoid_localization
import ring_theory.localization

variables (M : Type*) [comm_ring M]

def foo (u : M) (hu : is_unit u) : is_localization.away u M :=
{ map_units := begin
    rintro ⟨v,n,rfl⟩,
    erw (algebra_map M M).map_pow,
    exact is_unit.pow _ hu,
  end,
  surj := begin
    intros m,
    use ⟨m,1⟩,
    simp,
  end,
  eq_iff_exists := begin
    intros a b,
    refine ⟨λ h, ⟨1, by simpa⟩, _⟩,
    rintro ⟨⟨c,n,rfl⟩,hc⟩,
    simp at hc,
    have : is_unit (u^n) := is_unit.pow _ hu,
    rw this.mul_left_inj at hc,
    rw hc,
  end }

noncomputable
example (u : M) (hu : is_unit u) : localization.away u ≃ₐ[M] M :=
by haveI := foo _ u hu; exact is_localization.alg_equiv (submonoid.powers u) (localization.away u) M

[Adam Topaz]

I'm a little surprised we don't have this in mathlib somewhere...

[Adam Topaz]

Also, it looks like is_localization.away is only defined for commutative rings while localization.away for any monoid. Why is that?

[Justus Springer]

I asked about this before here, but then never PR'd it. Now things have changed again since the localization map refactor.

[Justus Springer]

Adam Topaz said:

Also, it looks like is_localization.away is only defined for commutative rings while localization.away for any monoid. Why is that?

Maybe @Anne Baanen ?

[Eric Wieser]

(docs#is_localization.away vs docs#localization.away for reference)

[Eric Wieser]

I think this is because in turn docs#is_localization requires a full algebra structure while docs#localization does not

[Anne Baanen]

The monoid version of is_localization.away is called something like docs#submonoid.localization_map.away_map

[Andrew Yang]

Since Schemes and consequently AffineSchemes have hidden universe variables, I cannot simply coerce X : AffineScheme into Scheme without explicitly stating the universe levels.
Is the paradigm to tuck .{u}'s everywhere, or to not use coerces, or there is some other solution to this?

[Justus Springer]

I don't think providing universe levels explicitly is considered a bad thing. But I'm not sure we would even want a coercion, maybe it would suffice to have AffineScheme.to_Scheme?

[Adam Topaz]

The AffineScheme.to_Scheme would presumably just be an alias for docs#category_theory.functor.ess_image_inclusion

[Andrew Yang]

I've finished the 'faithful' part of the fully-faithful-ness, but the 'full' part seems to need some more definition unfolding to make it work.
The file.
I'm wondering if there are any advices about the code or such before I continue.

[Justus Springer]

Thanks for working on this! I think it looks very good. I have a few comments:

• I don't think we even need the extra definition to_Spec_Γ. Maybe we can just use structure_sheaf.to_open R ⊤? As a second step, we could have the actual isomorphism R ≅ (structure_sheaf R).presheaf.obj (op ⊤) as an extra definition, making use of as_iso. This should also help with defining Spec_Γ_identity, making use of nat_iso.of_components.
• Spec_Γ_identity should be a def, not a lemma (you can also see this warning yourself by typing #lint at the end of the file).
• Everything leading up to R ≅ (structure_sheaf R).presheaf.obj (op ⊤) should probably go into structure_sheaf.lean I would say. Maybe right below basic_open_iso?
• About op_iso: I remember I needed the same thing when playing around with something else. I have it on the old branch branch#is_iso_op, but never PR'd it. Should I PR it, so that that's out of the way?

You could probably PR the isomorphism R ≅ (structure_sheaf R).presheaf.obj (op ⊤) very soon (as soon as the localization-at-units thing jas been done)

[Andrew Yang]

(deleted)

[Andrew Yang]

I've finished the fully faithful ness of Spec. Though it is just a draft and the proof is quite ugly.
This file contains R ≅ (structure_sheaf R).presheaf.obj (op ⊤) and Spec ⋙ Γ ≅ 𝟭.
This file proves the fact that two morphisms into affine schemes are equal if their underlying topological map and the map at the global sections are both equal.
This file contains the fully-faithful ness of Spec.

• I've tried to remove to_Spec_Γ, but lean complains about R not equal to CommRing.of ↥R. I moved it out from the part that should go into structure_sheaf.lean though. I'm not sure what the better solution is.
• I need the fact that two maps of sheaves (of CommRing) coincide iff they coincide on stalks, and that elements of stalks are all germs. These are proved in Top.presheaves for Type-valued sheaves, but not for CommRing valued sheaves. I could just mirror the proof, but maybe there is a better way to prove that these all hold in good enough concrete categories.
• The eq_to_hom is quite annoying and the proof seems unnecessarily long because of it. Is there a better general approach to it?
• About op_iso: Yeah, please do PR it. Also it would be great if there is also (inv f).op = inv f.op.
• For the localization-at-units thing, is anyone currently working on it? Or should I finish that up.

[Johan Commelin]

branch#affine_schemes for those looking for a branch name (-;

[Johan Commelin]

@Andrew Yang great job! Seems like you managed to do a lot in a few days.

[Kevin Buzzard]

These are all steps in the right direction. Many thanks Andrew!

[Justus Springer]

Great! Maybe we should make a new directory algebraic_geometry/Spec? Then we could have one file for fully faithfulness and one file for the adjunction.

[Justus Springer]

Andrew Yang said:

• About op_iso: Yeah, please do PR it. Also it would be great if there is also (inv f).op = inv f.op.

Done: #9319. I'm afraid we can't prove (inv f).op = inv f.op, as docs#category_theory.inv is defined using choice. But we do have docs#category_theory.iso.op_inv.

[Scott Morrison]

A new directory is a good idea.

[Andrew Yang]

Justus Springer said:

Done: #9319. I'm afraid we can't prove (inv f).op = inv f.op, as docs#category_theory.inv is defined using choice. But we do have docs#category_theory.iso.op_inv.

Hmm, is there a place for non-computable lemmas about category theory to go then?
And also things like instance [e : is_equivalence F] : is_equivalence F.op.

[Reid Barton]

It can be proved, it just won't be a definitional equality.

[Reid Barton]

Andrew Yang said:

• The eq_to_hom is quite annoying and the proof seems unnecessarily long because of it. Is there a better general approach to it?

You're talking about this one, right?

def top_map_of : Top_obj R ⟶ Top_obj S := by {
  refine (eq_to_hom _) ≫ f.val.base ≫ (eq_to_hom _);
  dsimp only [to_LocallyRingedSpace, LocallyRingedSpace_obj, opposite.unop_op];
  refl
}

[Reid Barton]

Just looking at it, I'm not sure why the eq_to_homs should be necessary at all since the equalities involved are definitional. What happens if you leave them out? Does Lean just take a long time?

[Justus Springer]

Reid Barton said:

It can be proved, it just won't be a definitional equality.

Oh of course, inverses are unique!

[Justus Springer]

Andrew Yang said:

And also things like instance [e : is_equivalence F] : is_equivalence F.op.

We only have the bundled version: docs#category_theory.equivalence.op.

[Justus Springer]

Andrew Yang said:

• I need the fact that two maps of sheaves (of CommRing) coincide iff they coincide on stalks, and that elements of stalks are all germs. These are proved in Top.presheaves for Type-valued sheaves, but not for CommRing valued sheaves. I could just mirror the proof, but maybe there is a better way to prove that these all hold in good enough concrete categories.

Indeed, I've just generalized this (and other stuff in topology/sheaves/stalks) on branch#spec_gamma_adjunction. It should now be applicable to any concrete category, whose forgetful functor reflects isomorphisms, preserves limits and filtered colimits. This is exactly why I needed this whole filtered colimits stuff.

[Justus Springer]

@Andrew Yang I think it's promising that we are discovering the same sorts of issues here. We should probably coordinate our efforts closely :)

[Justus Springer]

May I use this occasion to mention that I am still waiting for reviews on #9101. I know it's a big one, but it seems like this is crucial for further development :)

[Johan Commelin]

@Justus Springer you should have pinged earlier! I'll try to take a look today!

[Justus Springer]

@Johan Commelin Thanks! I just noticed yesterday that some tests were getting canceled for some reason, which is why it didn't show up on #queue. I merged master again, now it succeeds.

[Andrew Yang]

Reid Barton said:

It can be proved, it just won't be a definitional equality.

Oh I thought there were some constructivist concerns or such. I'll add it somewhere.

[Andrew Yang]

Reid Barton said:

Just looking at it, I'm not sure why the eq_to_homs should be necessary at all since the equalities involved are definitional. What happens if you leave them out? Does Lean just take a long time?

Lean complains that the types don't match. If I don't write out the eq_to_hom explicitly, they be come _.mpr's, which are also a pain to work with.

The more tricky one is the coerce from f _* O(X) to g _*O(X). I can understand that it is needed, but my goal becomes a mess, and I needed stuff like

let F := λ (x : U), (structure_sheaf R).presheaf.germ x,
  have : ∀ (a b) (H : a = b), F a = F b ≫ eq_to_hom (by rw H) := λ _ _ H, by subst H; simp,
  apply this,

to solve it, since simply rw H says that the motive is not type correct. I am wondering if there is a better way to do this.

[Justus Springer]

I just PR'd #9357, generalizing things like germ_exist and other stalk-related lemmas from sheaves valued in Type to any "nice enough" concrete category.

[Junyan Xu]

I have proven that a "morphism on a basis" from a presheaf to a sheaf (with values in an arbitrary category) on a topological space can be extended to an actual morphism (on all open sets): https://github.com/alreadydone/mathlib/commit/121a3444131fc1180ca021552b47b7563aebcaa5#diff-d7cc616887430b2cb5792e3d691f45c1bbc3eaa32c3abf1c4e735ab8b9a904d9R152
This appears necessary to construct the sheaf morphism in the Spec-Gamma adjunction; it should be equivalent to https://stacks.math.columbia.edu/tag/009V (except that the source need not be a sheaf) which is used in the Stacks Project proof. My proof doesn't involve colimits like in https://stacks.math.columbia.edu/tag/009Q and only involves limits that are guaranteed to exist by the sheaf condition, so it works with any category of values (provided that the opens_le_cover formulation of the sheaf condition is used (which I think is the one that should be used in the definition of a sheaf)). Such a construction of extension is mentioned in the comment https://stacks.math.columbia.edu/tag/009H#comment-2589 and a reference for it is The Geometry of Schemes (GTM 197), p.17 (Stacks Project and the comment actually only talk about extension of a sheaf on a basis to all open sets and not a morphism, but in the case of the Spec-Gamma adjunction we already have the sheaves, so we only need to extend the morphism).

Comments are welcome! The proofs are clumsy and I feel I'm missing some tricks; the style/naming may not yet conform to the mathlib norm; the implicit arguments may not be optimal; and I'm not sure if the is_basis and sheaf condition assumptions should be instances.

Together with the nice preliminary work like #9101 I imagine it's now relatively easy to prove the adjunction, and will work towards that goal given that @Justus Springer is less active now (as he said, he has less time in October).

[Scott Morrison]

I wonder how everyone would feel about rearranging things so opens_le_cover becomes the official definition?

[Justus Springer]

Thanks @Junyan Xu , it's great to see that more people are working on this! Note that development on this adjunction is still ongoing. I will have less time for Lean in October, but I will try to help finish the adjunction. @Andrew Yang and I have also been working on doing sheaves on topological bases. Our goal is to get the equivalence of categories between sheaves on a bases and sheaves on all open sets. But because defining "sheaf on a basis" directly would be too much of a duplication of the original sheaf definition, we are trying to embed it into the general theory of sheaves on sites. In particular, Andrew has shown recently (#9431) that a cover-lifting functors between sites G : C ⥤ D extends to a functor between sheaves on C to sheaves on D. The way it's done has to do with the right Kan extension of a functor and it's a vast generalization of how you use limits to define the extension of a sheaf on a basis. But Andrew can tell you more about this than me. The abstract statement we are going for will be something like this: A cover-lifting fully faithful functor G : C ⥤ D between sites induces an equivalence of categories between sheaves on C and sheaves on D. This then gets applied to the inclusion functor $\mathcal{B}\to Opens(X)$ from a topological bases to all open sets, which is easily seen to be cover-lifting and fully faithful.

[Justus Springer]

Another part of the puzzle is to finally connect the theory of sheaves on spaces to sheaves on sites, which is something I worked on and PR'd a few days ago: #9609

[Justus Springer]

Admitted, for the Gamma-Spec adjunction, it is not necessary to know about the full equivalence between sheaves on bases and sheaves on the whole space. You don't even need to define sheaves on bases. You just need to know how to extend morphisms. So what you have done @Junyan Xu would be the more direct route. I don't know what would be the best route to continue, but I think developing a bit of abstract API about sheaves on sites would be worth the detour.

[Justus Springer]

Also note that I have a tiny bit of code lying around on branch#spec_gamma_adjunction. For some reason I decided a long time ago that it would be best to do the adjunction via defining unit and counit: The unit would be the isomorphism $R \cong \mathcal{O}_{Spec(R)}(Spec(R))$ (which already exists) and for the counit, you'd need to define a morphism $X \to Spec(\mathcal{O}_X(X))$ for all locally ringed spaces. I have defined this morphism already as a continuous map, all that's missing is the corresponding sheaf homomorphism, seeing that it's local on stalks, and the triangle identities.

[Junyan Xu]

Thanks @Justus Springer for the updates on recent progress and roadmap; great to see that you're still actively contributing! I searched and saw you haven't posted on Zulip since the end of September, and didn't find recent PRs by you on Github, so I assumed you're not active; now I realize I should add author: when searching for PRs.

I've only heard the name "Kan extension" before but never saw its definition or what it's used for, and my knowledge on Grothendieck topologies is rusty, but more generality and categorical foundations are definitely nice (especially as we work towards etale cohomology)! For example, I was trying to find an easy way to express the restriction of a presheaf morphism to a subcategory of the opens when I saw the definition of horizontal composition in mathlib documentation, and then realized that the restriction is a special case. I'm also glad to see PR #9609 connecting a general definition to a special one.

As for the adjunction, I was thinking of using mk_of_hom_equiv, but will now also consider the unit-counit route to see if it's easier. I see that @Andrew Yang has defined the unit in global_section_of_spec.lean except for a sorry for localization at units. I've also seen your nice work in branch#spec_gamma_adjunction, but unfortunately after merging master it becomes quite hard to find the relevant commits.

[Junyan Xu]

Scott Morrison said:

I wonder how everyone would feel about rearranging things so opens_le_cover becomes the official definition?

Oh sorry, I actually meant to propose to promote the pairwise_intersections definition to the official one. It's a natural generalization of the standard definition (unique_gluing, which is like pairwise_intersections applied to cones with cone point the free object on one element), and works for arbitrary category of values (doesn't require has_products) that only makes sense with concrete categories. Although opens_le_cover may be more convenient, we can go between both easily without has_products.

[Andrew Yang]

About the sheaves on basis stuff, the current plan is to formalize Theorem C2.2.3 in the elephant. Currently the functors on two sided are both constructed (in #9431 and #9650), and it remains to show that the two functors are indeed inverses to each other. One side follows straight from existing lemmas in the mathlib, but the other side probably needs more work. That said, this construction still requires some existence of limits since Kan extension needs them. It would be great if these conditions can be inferred straight from the sheaf conditions and removed.

As for the counit, it is already tidied up and merged into master as docs#algebraic_geometry.Spec_Γ_identity.

[Junyan Xu]

Yeah I just saw #9416 a few minutes before you posted. Very nice! I think (at least in the topological space case) you'll need the existence of appropriate limits to extend a sheaf on a basis to all open sets (to define the objects at open sets not in the basis), but you probably don't need it to extend morphisms, as in the topological space case.

[Junyan Xu]

btw, it seems I and @Justus Springer agree that what you constructed is the unit (at least if we're proving the adjunction between Spec.right_op and Gamma, and not between Gamma.right_op and Spec), but you call it the counit ...

[Andrew Yang]

Hmmm, isn't $\Gamma(\mathrm{Spec}(R)) \to R$ the counit and $X \to \mathrm{Spec}(\Gamma(X))$ the unit of the adjunction?
If I'm wrong, the docs in mathlib about the iso probably needs fixing as well..

[Junyan Xu]

The unit is the inverse map $R\to\Gamma(\mathrm{Spec}(R))$ in CommRing
The counit is indeed $X \to \mathrm{Spec}(\Gamma(X))$ but in the opposite category of LocallyRingedSpace so the arrow is reversed.

[Andrew Yang]

Oh I forgot the opposites :sweat:
Will probably fix the docs when the adjunction is actually done then...

[Junyan Xu]

Another related problem is that you wrote Γ ⊣ Spec: if Γ is the left adjoint then the adjunction should be between Γ.right_op and Spec (between categories LocallyRingedSpace and CommRing^op), but since you have been working with Spec.right_op and Gamma, we'd probably like to change it to Spec ⊣ Γ.

[Justus Springer]

I also always confuse unit/counit and left/right in this adjunction. @Junyan Xu I also didn't know much about grothendieck topologies a few weeks ago, I'm learning as I'm going.

[Justus Springer]

Regarding the sheaf definition, yeah since the pairwise_intersections definition doesn't require products, it should probably become the official definition. The general definition of a sheaf on a site also doesn't require products. However, my proof that the definition on sites is equivalent to the definition on spaces works with the equalizer definition, so the proof would have to be redone. Maybe we can do this later, I doubt that this extra bit of generality will be needed soon.

[Johan Commelin]

Concerning fibre products of schemes (which have also been discussed in this thread), I stumbled upon http://math.stanford.edu/~vakil/d/FOAG/BOfiber-prods.pdf which is a nice way to organize things, I think.

[Johan Commelin]

Also, getting the definition of a Zariski sheaf in mathlib would be a nice side effect (-;

[Justus Springer]

I think I will have to come to terms with the fact that I won’t have as much time for Lean now than I had in September. I will shift focus now and concentrate on my MSc thesis, so will probably no longer contribute to mathlib for a while. I was not able to finish the Gamma-Spec adjunction, which is a project I’ve been working on for the last month or two, and indirectly even longer. But I think it’s in reach now and it will be an important milestone. I thought I’d post here some of my thoughts on the adjunction in general, where I left off and how I think one can proceed. Maybe someone will find it useful.

I left some code on branch#spec_gamma_adjunction, outlining the way I imagine the construction would go. I don’t claim ownership to this branch anymore, anyone can feel free to adopt it. The construction roughly follows stacks#01I1. However, when I was working through the stacks proof, I somehow got the feeling that it might be easier to do the adjunction via providing unit and counit instead of the hom-equivalence. But this is not set in stone and the construction is very similar.

The unit already exists, it’s the isomorphism docs#algebraic_geometry.Spec_Γ_identity. For the counit, the task is to construct a morphism of locally ringed spaces $\psi\colon X\to{\rm Spec}(\Gamma(X))$ for every locally ringed space $X$. As a map, this sends a point $x\in X$ to the prime ideal of all $f\in\Gamma(X)$ that vanish in $x$, i.e. such that the germ of $f$ at $x$ is a non-unit. I proved this to be continuous already on branch#spec_gamma_adjunction. For the sheaf morphism, one has to construct a map $\mathcal{O}_{{\rm Spec}(\Gamma(X))}(U)\to\mathcal{O}_X(\psi^{-1}(U))$ for all $U\subset {\rm Spec}\Gamma(X)$. It is at this point that we need to know how to extend a morphism of sheaves on a basis, as this morphism can only directly be defined on basic opens $U=D(f)$. This is the biggest hole in the construction right now, as soon as this has been settled (either by proving the comparison theorem of topos theory as @Andrew Yang is doing, or by a more direct approach a la @Junyan Xu ), the rest of the construction should be pretty lean-able I believe.

To get the morphism $\mathcal{O}_{{\rm Spec}(\Gamma(X))}(D(f))\to\mathcal{O}_X(\psi^{-1}(D(f)))$, note that $\psi^{-1}(D(f))=D_X(f)$ where $D_X(f)\subset X$ is the basic open on $X$, as defined in docs#algebraic_geometry.RingedSpace.basic_open. By docs#algebraic_geometry.RingedSpace.is_unit_res_basic_open, the restriction $\Gamma(X)\to\mathcal{O}_X(D_X(f))$ sends $f$ to a unit, hence lifts to a map $\Gamma(X)_f\to\mathcal{O}_X(D_X(f))$. Composing this with docs#algebraic_geometry.structure_sheaf.basic_open_iso gives you the desired map.

Excluding the issue of extending from a basis, the sorries left on branch#spec_gamma_adjunction are as follows:

1. Show naturality of the sheaf homomorphism on basic opens.
2. Show that the stalk maps of the sheaf homomorphism are local.
3. Show naturality of the counit $X\to{\rm Spec}(\Gamma(X))$ in $X$.
4. Show the left triangle identity.
5. Show the right triangle identity.

I am fairly confident that all of these should be pretty doable, but I haven’t tried in detail. Maybe someone else has already done some of them. For (2), I’d imagine we want to show that that the germ map $\Gamma(X)\to\mathcal{O}_{X,x}$ is a localisation map for the prime ideal $\psi(x)$, hence gives an isomorphism $\Gamma(X)_{\psi(x)}\cong \mathcal{O}_{X,x}$. Then we should show (by some uniqueness argument) that the stalk map $\psi_x\colon\mathcal{O}_{{\rm Spec}(\Gamma(X)), \psi(x)}\to\mathcal{O}_{X,x}$ is equal to the composition of isomorphisms $\mathcal{O}_{{\rm Spec}(\Gamma(X)), \psi(x)}\to\Gamma(X)_{\psi(x)}\to\mathcal{O}_{X,x}$, hence is local. Here, the first isomorphism is docs#algebraic_geometry.structure_sheaf.stalk_iso.

I don’t know how difficult it is to prove the triangle identities. Ultimately, that will probably decide whether it’s better to do the adjunction via unit/counit or the hom-equivalence.

[Johan Commelin]

@Justus Springer Thanks a lot for your contributions so far! What's your MSc project about?

[Justus Springer]

It was very fun! About my MSc project, I don't know for sure, I'm just starting out. But it will involve Cox Rings and some classification of Fano varieties with a torus action of complexity one :)

[Junyan Xu]

Didn't expect it to take so long, but I finally finished the job before November! The Gamma-Spec adjunction is now defined and mathlib build succeeded on the cloud, even though some proofs are slow (to be improved, but I guess you can start reviewing the PR #9802!). And I chose to establish Gamma —| Spec instead of Spec —| Gamma, so no change in earlier documentation is needed.

[Junyan Xu]

TIL the categories of ringed spaces and of locally ringed spaces have arbitrary limits, from this note by Martin Brandenburg: https://www.dropbox.com/s/y5t58kugrcaqbx8/fiber-products-of-locally-ringed-spaces-and-schemes.pdf?dl=0
And he then derives that the category of schemes has finite limits (4.3), because a finite intersection of opens is open and such open affines cover the whole space.
Seems a totally different construction than what I've learned and no gluing is involved! Maybe this is what we should aim for.

I found the pdf from https://mathoverflow.net/questions/13616/a-book-on-locally-ringed-spaces in turn from https://math.stackexchange.com/questions/1033675/does-the-category-of-locally-ringed-spaces-have-products
because after defining the adjunction between LRS and CommRing I was curious whether LRS also has fibred products: turns out it has much more.

fiber-products-of-locally-ringed-spaces-and-schemes.pdf

[Johan Commelin]

Ooh, I'll have to read that when I have a bit more time! That seems like a interesting approach!

[Johan Commelin]

I would have expected that you need separatedness for the "intersection of opens is opens and such open affines cover" bit of the argument. But like I said: I should read that pdf first.

[Junyan Xu]

Here is an outline of a proof that Scheme has (binary) fiber products from the assumption that LRS has them. The fiber product in LRS is also the fiber product in Scheme provided the object lies in Scheme, so we only need to show that if $X_1, X_2, S$ are schemes, the $X_1\times_S X_2$ is also covered by open affines (by mathlib definition, means that every point has an open neighborhood such that the restrict along the inclusion of the neighborhood is isomorphic to the Spec of a ring).

Given a point x of $X=X_1\times_S X_2$, consider its projection p(x) into S, and take an open neighborhood V of p(x) in S that is affine. Similarly take affine neighborhoods $U_1, U_2$ of $p_1(x), p_2(x)$ in $X_1, X_2$ respectively, then take basic opens within $U_1, U_2$ that projects into V. We then need that the restriction of $\mathrm{Spec}(R)$ to a basic open $D(f)$ is isomorphic to $\mathrm{Spec}(R_f)$, and that restrict commutes with composition of open embeddings.

Now replace $U_1, U_2$ by the basic opens, and use the universal property of restrict (notice that the statement is only lift without the fac and uniq parts of the universal property) to obtain morphisms $p_1^{-1}(U_1)\cap p_2^{-1}(U_2) \to U_i$ and $U_i\to V$ with all open sets endowed with the restrict LRS structure (here we use that the intersection of two opens is open). Then use the universal property to show that their compositions with $U_i\to V$ agree, and these three morphisms to $U_1,U_2,V$ realizes $p_1^{-1}(U_1)\cap p_2^{-1}(U_2)$ as the fiber product $U_1\times_V U_2$ in LRS. Finally, use Gamma-Spec adjunction to show the fiber product isomorphic the Spec of a coproduct (tensor) of rings (here we need that Spec is a full functor which Andrew proved; is it now in mathlib?).

A side comment is that instead of directly proving universal property of restrict (actually should be of of_restrict) we should probably first define open immersion, show that of_restrict is an open immersion, then show that all open immersions satisfy the universal property.

Although all these are relatively straightforward to formalize, I'm posting here to find out which lemmas have already been done, as I know at least @Andrew Yang has been working in this direction.

[Andrew Yang]

The fact that Spec is fully faithful should follow straight from the counit(?) isomorphism, so I did not work to make that into mathlib.
I agree that we should provide the universal property in terms of open immersions.
I assume the biggest obstacle in leanifying that paper is in the part that LRS has fibre products. That definition seems quite ugly, and I don't really know or have time lately to think about how to formalize them properly (my midterms are coming...)
That said, after seeing that note that you posted, I tried to look for similar results and stumbled upon https://arxiv.org/pdf/1103.2139.pdf.
This seems quite similar to the note above but wrapped everything in some categorical jargon, which may or may not make it easier to formalize, but I suppose it is an alternative.

[Junyan Xu]

Andrew Yang said:

The fact that Spec is fully faithful should follow straight from the counit(?) isomorphism

Indeed, faithfulness only needs the counit iso, though fullness also needs the unit and the right triangle identity (the harder one of the two asserting a LRS morphism is id): defining the preimage only needs the counit iso, but verifying it's a preimage needs right triangle.

[Scott Morrison]

Hopefully the results of src#category_theory.adjunction.fully_faithful are helpful here?

[Junyan Xu]

Nice, I've found the perserve_limits theorem but haven't looked into fully faithfulness yet. But the linkifier seems broken (the link points to a 404 page https://leanprover-community.github.io/mathlib_docs/find/category_theory.adjunction.fully_faithful/src ) docs#category_theory.adjunction.fully_faithful doesn't append src at the end but also isn't converting dots to slashes.

[Junyan Xu]

So I’ve skimmed through Gillam’s paper and plan to adopt his approach, while Andrew keeps pursuing the gluing approach. Although fiber products of schemes require just one approach to build, I believe the two approaches will eventually be good for different purposes in the future, no matter which one is adopted for the current purpose.

It’s now clear to me that Gillam’s localization functor from PRS (primed ringed spaces) to LRS is just a generalized version of Spec (to LRS) on CommRing: the constructions are very similar, and indeed it’s used to construct Spec in Lemma 3 (bottom of p.9), and it’s part of a general adjunction (Theorem 2) that subsumes the Gamma-Spec adjunction #9802. We would need to prove everything in structure_sheaf.lean in the more general form, so to avoid duplicate code, it would be a good idea to refactor to define Spec in terms of the localization functor. The Spec constructed this way will not have the underlying set equal to the prime spectrum, so an extra step seems necessary to transfer the LRS structure to the prime spectrum.

Gillam first shows that PRS has all limits, and uses Theorem 2 (which says the localization functor PRS -> LRS is a right adjoint with unit an iso) to deduce that LRS has all limits (I’m unable to find this implication in mathlib). PRS is easily shown to have all limits given that RS has all limits, which is just three sentences in [Gillam], unlike the lengthy argument in [Brandenburg] (Theorem 2.1). I think it’s indeed easy: PresheafedSpace can be shown to have all limits easily given that the value category has all colimits, now that we have pullback of presheaves in mathlib, similar to how it was shown that it has all colimits; then sheafification on the limit presheafed space would yield the limit in SheafedSpace. (Gillam only talks about inverse limits, but I believe the arguments apply for all (small) limits.) The sites version of sheafification recently completed by Adam Topaz would suffice but it’s yet to be merged into mathlib.

[Johan Commelin]

Sounds good. But if these changes go through, it will be important to have a good API for the connection to prime_spectrum, I guess.

[Andrew Yang]

There's now a project page dedicated to AG
if someone wants to track the current PRs and progress.

[Johan Commelin]

Thanks a lot for creating this overview!

[Johan Commelin]

Seems like the maintainers have some homework!

[Junyan Xu]

I added a bunch of "small subprojects" to the project page as a new column that I've thought about but haven't found time to code up, some essential to the main project (fibred product). Everyone is welcome to help! As I'm focusing on the main project, I'll probably only do the minimum required when the time comes if no one takes them up. You're welcome to add your ideas to the list, though for Andrew it's probably fastest to do everything himself. ;) I also renamed "to do" to "main project" and @Andrew Yang probably want to add (references to) the gluing approach to that column as well?

[Junyan Xu]

Junyan Xu said:

uses Theorem 2 (which says the localization functor PRS -> LRS is a right adjoint with unit an iso) to deduce that LRS has all limits (I’m unable to find this implication in mathlib).

and I actually found the dual form of this result in monad/limits (the left adjoint is a coreflective functor), mentioned in this card.

[Andrew Yang]

Just popping up to say that we can now glue schemes in branch#presheafed_spaces_glue.

This will probably come after a sea of PR spams :grinning:.

[Kevin Buzzard]

Thank you so much for pushing the algebraic geometry dream forwards! Many of us have been distracted by the Scholze project. In the distant past we'd been experimenting with doing algebraic geometry without using the category theory library, but Scott convinced me that we should use categories, so we defined schemes using the category theory library, went off to celebrate that mathlib had schemes, and then LTE came along and we never came back to it. In some sense this is the first big experiment to see if we can actually get category theory to do something in Lean other than more category theory, and for me this is a really important question but for a long time nobody was working on it. I'm really grateful that this new group of people have appeared (you and Junyan) who are pushing this forward, I think it's a really important experiment.

[Scott Morrison]

I don't really like this formulation: "can we actually get category theory to do something in lean other than more category theory". I mean, of course we know that category theory does something in mathematics other than more category theory, e.g. essentially all of modern algebraic geometry. Whether one can do modern algebraic geometry in Lean is a great and interesting question (surely the answer is "yes"), so why not just ask that?

[Scott Morrison]

But whatever --- this is great progress, and exciting to see, @Andrew Yang!

[Kevin Buzzard]

Yes sorry Scott -- just to be clear I absolutely meant "can category theory be used in Lean to do anything other than more category theory". I use cohomology theories all over the place in my non-Lean work and of course category theory powers this stuff via homological algebra. I meant to stress the point that until algebraic geometry, Lean's category theory library was being developed essentially independently of the rest of mathlib; it would sometimes use the rest of mathlib (e.g. when making the category of rings or the category of R-modules) but the rest of mathlib would never use it. It was Scott who argued strongly to use the category theory library when defining schemes (i.e. we didn't define scheme X like we have ring R, we defined Scheme directly) and this is what we did. This provided a link from category theory to another branch of mathlib (namely algebraic geometry) and then the question became "does it actually work? Can we now do stuff?". For a while the answer was "we don't actually know because nobody is doing stuff", but now people are doing stuff and it's working. It's also definitely worth pointing out that in a previous incarnation of schemes which didn't use the category theory library (and was never pushed to mathlib, it was Ramon Fernandez Mir's schemes repo) we did try to do gluing and it was really messy.

The other big application I see of Lean category theory right now in an area of maths which isn't just more category theory is in the LTE repo. The ultimate goal is to show that an Ext group is zero and we have defined the Ext group using the category theory language, even though in applications I guess we want it to represent the assertion that there are no non-trivial extensions of a thing by another thing. We are getting to this stuff right now in LTE so this will represent another proof that Lean 3 categories can be used for things other than Lean 3 categories.

Sorry for the confusion Scott! Hopefully you're less upset by this clarification. Let me know if you're still upset.

[Eric Wieser]

Lean's category theory library was being developed essentially independently of the rest of mathlib; it would sometimes use the rest of mathlib (e.g. when making the category of rings or the category of R-modules) but the rest of mathlib would never use it.

To provide some visual emphasis on that point:

image.png

The highlighted notes are in the category_theory, and node groupings are based on imports

[Mario Carneiro]

what's the blue bit on the right? tactic?

[Eric Wieser]

core:init. You can investigate yourself at https://eric-wieser.github.io/mathlib-import-graph/. tactic is more entangled

[Mario Carneiro]

huh. TIL that mathlib has a prelude file: tactic.transfer

[Mario Carneiro]

I guess this was imported from core and never changed

[Kevin Buzzard]

But now we have homological algebra, category theory will start to find applications in commutative algebra -- that will be the next area that it invades after alg geom. The reason it's taken so long is that basically it has been only Scott (and then later on Scott and Bhavik and Adam) and it has taken a long time to get to abelian categories. But now we're there! Adam proved that condensed abelian groups were an abelian category the other day, so that works too :D

[Alex J. Best]

The mathlib prelude file is one of the many interesting things in mathlib that make writing the import minimizer way more tricky in practice than it was in theory, I would be happy to see it gone!

[Junyan Xu]

Hi Kevin, thanks for the posts and the advertisement on Twitter. Most of the work was actually done by Andrew, as you can see from the number of merged PRs (I have only two). In my experience, the category library has been very useful and very often when I want a result it’s already in it.

I haven’t had an active PR for a while but in the meantime I created two branches: Gillam for showing LRS has limits following Gillam’s paper, and adjunction_mates for defining lax/pseudofunctors and transferring them across adjunctions, because I found these necessary to work with presheaf pullback, e.g. when showing PresheafedSpace has limits. However, a recent realization has changed my development plan and moved focus towards a more abstract, general, categorical direction. The realization is that the construction of the categories Top from Type, PresheafedSpace from Top, and SheafedSpace from PresheafedSpace, are all examples of the Grothendieck construction, resulting from the functor F : C ⥤ Cat which gives a functor between fiber categories for each morphism in the base category. In the first case, the fiber categories are partial orders (the type of topologies on a type ordered by inclusion), in the second case the type of presheaves on a space, and in the last case subsingletons (the is_sheaf Prop; the functor here “is” the implication that a pushforward of a sheaf is a sheaf). However, LocallyRingedSpace from RingedSpace isn’t such an example, but PrimedRingedSpace from RingedSpace is (with fiber categories the partial orders of “prime systems”, actually an example of "category of elements").

I haven’t checked all details, but it appears that the existence of colimits in the Grothendieck construction follows from the existence in the base category and in the fiber categories, plus some minor conditions (e.g. the functor preserves colimits), similar to the proof that PresheafedSpace has colimits, which seems mostly rely on the functors pushforward_over, pushforward_under and pushforward_forget_adjunction in my Gillam branch, which can be generalized to any Grothendieck construction; moreover the forgetful functor to the base category would preserve colimits. For example, for Top, the functor “is” the coinduced(“quotient”) topology, and it’s adjoint to the functor of induced(“subspace”) topology, and adjoint functors give rise to contravariantly isomorphic Grothendieck constructions, so together with the fact that the topologies on a space form a complete lattice (fiber categories have both limits and colimits), we can show that Top has both limits and colimits. However, my goal is not to refactor the facts about Top, but to deal with limits in PresheafedSpace, where I need to deal with presheafed pullback, which is no longer a strict functor, but has a pseudofunctor structure transferred from pushforward across adjunction (the proofs should probably be replaced with a more conceptual and probably shorter/faster one using yoneda faithfulness + adjunction hom_equiv). So here I need to generalize the Grothendieck construction to allow pseudofunctors, or more generally lax functors, which is what I plan to do when I hopefully have some time in the weekend. Would like to hear what categorical people think about it! References are also welcome.

[Johan Commelin]

@Junyan Xu Wow, that sounds like a cool plan!

[David Wärn]

You might be interested in displayed categories. You could say it's a generalization of the Grothendieck construction which allows lax functors to the category of categories and profunctors. As a result you get not only Grothendieck fibrations but all functors (up to isomorphism), but really the point is that the general notion of displayed category is fairly easy to work with in type theory (although you need to use pathovers / == to state associativity etc).

I don't know that using displayed categories for this formalisation would make things easier overall, but in case you're interested I wrote the basic definitions in Lean here.

[Andrew Yang]

Another status update:

we now have this

instance {X Y Z : Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) : has_pullback f g :=
has_pullback_of_cover (Z.affine_cover.pullback_cover f) f g

It is essentially sorry-free, where the only sorries involved are proved in the currently abandoned #9802

It is over at branch#open_subfunctor and in the file open_subfunctor.lean.

Although the file name, it is constructed via gluing naively, without the Zariski sheaf and the open subfunctor stuff.

[Johan Commelin]

Wow! That's quite a milestone!

[Junyan Xu]

Just a tiny bit of progress over branch lax_grothendieck from me last weekend; and I did find the result about limits in nLab from a TCS paper ...

[Adam Topaz]

@Junyan Xu have you seen the old-ish thread about 2-categories? What do you think about defining 2-categories and pseudofunctors in general?

[Adam Topaz]

https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/2-categories/near/231851198

[Junyan Xu]

@Adam Topaz I think I've seen that thread once. The definition of 2-categories is quite long as can be seen in Bhavik Mehta's work, and I don't have sufficient motivation to work in that generality when all I need in the current application are pseudofunctors from 1-categories to Cat. I also don't have experience working with 2-categories and can't suggest which approach is better. @Scott Morrison expressed concerns about strict 2-categories gonna be infected with eq.recand I think displayed categories are an attempt to address the issue, but in my practice eq_to_hom makes equality of objects reasonably pleasant to work with.

[Johan Commelin]

@mathlib: Brace yourself. Incoming Γ ⊣ Spec

Big kudos to @Junyan Xu and @Andrew Yang

[Andrew Yang]

And also to @Justus Springer who laid most of the foundational works!

[Kevin Buzzard]

Next job: fibre products!

[Justus Springer]

Amazing work! Thanks @Andrew Yang and @Junyan Xu for putting so much work into finishing this project. I hope I can return to become an active contributor in the not-too-distant future. This adjunction should really open the door to the interplay between algebra and geometry. I'm guessing an easy consequence now would be the equivalence of categories between CommRingᵒᵖ and AffineScheme? Is this already formalized?

[Andrew Yang]

The equivalence was done way back when I first got my hand on Lean. I've just tidied it up into a PR #11326.
Looking forward to having you back on board! Hopefully mathlib will know that fibre products exist by then (two-thirds of #10605 is in mathlib now), and together with the adjunction, these will definitely open a lot of doors for us to play with.

[Junyan Xu]

Congrats to @Andrew Yang on the merging of fibered products (#11450 and #10605)! I didn't follow closely lately but it seems you abandoned the open subfunctor approach at some point and adopted the proof on Hartshorne instead (despite the latter PR is still from a branch named open_subfunctor)? Searching for subfunctor or open_subfunctor turns up nothing relevant in the mathlib repo.

[Kevin Buzzard]

Next step: sheaf cohomology! Or proof that projective morphisms are proper? @Jujian Zhang how far are we from projective morphisms?

[Adam Topaz]

Congratulations!

Now for some additional low hanging fruit: we can use docs#category_theory.limits.has_equalizers_of_pullbacks_and_binary_products
together with the fact that Scheme has a terminal object (do we know this yet?) and docs#category_theory.limits.finite_limits_from_equalizers_and_finite_products to get all finite limits.

[Adam Topaz]

We may be missing some general construction to obtain binary products from pullbacks and a terminal object

[Adam Topaz]

Ah, we have it docs#has_binary_products_of_terminal_and_pullbacks (in the wrong namespace...)

[Jujian Zhang]

On another branch we have a grading on multi aria level polynomial rings. So we could have projective n space by combining Proj construction and that branch. So we must not be far from projective morphisms but sheaf cohomology is further away I think.

[Adam Topaz]

We don't have anything about right derived functors in terms of injective resolutions at the moment. Do we even have docs#category_theory.injective ?

[Bhavik Mehta]

Adam Topaz said:

Ah, we have it docs#has_binary_products_of_terminal_and_pullbacks (in the wrong namespace...)

Sorry! I wrote that before I figured out how the category namespaces should work!

[Andrew Yang]

As for the next step, I'm trying to develop a framework to describe morphisms between schemes whose conditions are imposed locally. (quasi-compact, quasi-separated, affine, closed immersion, (locally) of finite type, finitely presented, finite, integral, etc.)
If anyone want to get on this AG wagon that is in its full speed, a nice and useful result to have is the "qcqs-lemma" as called in the rising sea, i.e. these exercises in Hartshorne. Another good thing to have is to define dominant morphisms and proof stacks#0CC1.
image.png

[Andrew Yang]

Someone really need to snatch some AG work from me so that I can do more LTE stuff :(

[Andrew Yang]

Another good thing to have is #4013.
@Kevin Buzzard Is someone working on it now?

[Eric Rodriguez]

Andrew Yang said:

Another good thing to have is issue#4013.
Kevin Buzzard Is someone working on it now?

#4013, issue#x assumes that it's a repo named issue

[Andrew Yang]

Oh. Thanks!

[Yaël Dillies]

Btw if you need more boilerplate around ring homs (or any other hom, really!), I'm currently writing several hundred lines a day of it, so just tell me and I'll do it.

[Andrew Yang]

Also @Jujian Zhang what's the current status on sheaves of modules? I think I saw that you have been working on this too. Are you planning to return after the Proj construction?

[Andrew Yang]

@Junyan Xu Yeah. I did mention somewhere above that I abandoned the open subfunctor approach. On one hand gluing directly only takes about 500 lines, and I didn't really want to spend much more time on this so that I can do more interesting stuff. On the other hand this also gives a good enough open cover of the fibred product.
Although we should eventually need all the open subfunctor stuff later for things like the Grassmanian.

[Kevin Buzzard]

@David Ang did anyone express an interest in the properties of ring homs listed in #4013 ? Maybe you can tell the LSGNT students where we're up to now? Probably this is just the kind of algebraic geometry that some of them are learning.

[Jujian Zhang]

In some branch, category of bundled module is defined (restriction and extension of scalars). So sheaves of modules can be defined as functor into category of bundled module using restriction of scalar.

[Andrew Yang]

Oh I see. Are you planning to do more stuff about them? Such as defining the associated sheaf of a module, defining coherence, API about submodules (ideals), etc?

[Andrew Yang]

Btw is that category concrete? Do we have a good description about what the sheaf condition looks like in that category?

[Junyan Xu]

For bundled modules using restriction, I think the forgetful functor to the underlying type of the module (and to the module part of the bundled morphism, noticing that restriction doesn't change the underlying type) is faithful, so it's concrete, no problem.

(Note: I'm talking about bundledMap in this post. I haven't seen the definition using extension instead of restriction, but I guess both resulting BundledModule categories will be isomorphic through extend-restrict adjunction? Notice that the category defined using restriction is an example of the Grothendieck construction, but for extension we'd need Grothendieck construction generalized to lax functors (I haven't decided whether to refactor my work using the bicategory formalism recently developed by Yuma Mizuno).)

I guess a weird thing when using sheaves of bundled modules is that we won't be able to say M: module O_X but have to say that the image of M under the projection functor from sheaves of bundled modules to sheaves of rings is equal to O_X. This might make it complicated to define operations between two O_X modules. Say you want to define the direct sum of two O_X modules, don't you need to transfer the module structure on each open across the equality of the rings on that open? (or maybe equality is evil, and we should use isomorphism instead.)

[Andrew Yang]

It isn’t full though. I’m not sure the results still hold in this case?

[Andrew Yang]

Yes. Equality is evil and we should use an iso. Still this is unpleasant to work with :(

Would a typeclass [module Ox F] and some API converting this to and from a Sheaf BundledModule work?
I’ve never thought deep about these though. The problems elsewhere are already enough to take away all my attention.

[Adam Topaz]

Junyan Xu said:

For bundled modules using restriction, I think the forgetful functor to the underlying type of the module (and to the module part of the bundled morphism, noticing that restriction doesn't change the underlying type) is faithful, so it's concrete, no problem.

I don't think this is faithful. Take $\mathbb{Z}$ as a $\mathbb{Z}[G]$-module with the trivial $G$-action where $G$ is abelian and has nontrivial automorphisms. You can have nonidentity morphisms on the ring level which are identity on the module in this case, so those would all map to the same morphism of the underlying module.

[Adam Topaz]

But you can just take the functor sending a bundled module to the product of the ring and the module, and that should be okay.

[Adam Topaz]

If you want a more geometric example, take $A = k[X,Y]$ and $M = k$ with the obvious $A$-module structure obtained by identifying $k = A/(X,Y)$. Take $\sigma$ the automorphism of $A$ which interchanges $X$ and $Y$. Then for all $a \in k$ and $f(X,Y) \in k[X,Y]$ you have $f(X,Y) \cdot a = f(Y,X) \cdot a$ so that $(\sigma,\mathbf{1})$ is a morphism in this category, which is not the identity, but restricts to the identity on the module.

[Adam Topaz]

Once you have the projection functor from sheaves of bundled modules to sheaves of commutative rings, you could "curry" this "uncurried functor" (in the sense of Grothendieck constructions) and obtain a pseudofunctor from sheaves on rings to the fiber categories of this projection. You could then define a $\mathcal{O}_X$-module as an object in the image of this pseudofunctor under $\mathcal{O}_X$.

[Adam Topaz]

I'm sure there is some general nonsense result out there saying that you can get concreteness for algebras over any (multisorted) Lawvere theory.

[Junyan Xu]

You can have nonidentity morphisms on the ring level which are identity on the module

Oh yes indeed, I take that back. I shouldn't forget about the morphism on rings. Or just take any two morphisms between two rings and the zero modules over them...

[Andrew Yang]

Also tagging @Jon Eugster since you seemed to have expressed interest in working on the AG library somewhere else.