Algebraic geometry development

Stream: maths

[Kevin Buzzard]

@Andrew Yang @Junyan Xu @Adam Topaz @Johan Commelin @Jujian Zhang @Damiano Testa and whoever else works in algebraic geometry: in about a month's time I will be giving four two-hour "lectures" on algebraic geometry in Lean for PhD students (having spent 4 more lectures beforehand teaching them the basics), and these "lectures" will mostly be me doing live coding of mathlib PRs. Does anyone have any requests as to what I should work on? Looking at the "classic" project https://github.com/leanprover-community/mathlib/projects/13 I see that defining various typeclasses for morphisms looks interesting -- I know that we got things like formally etale, formally smooth etc recently; should I go for separated/proper, and affine, or does anyone have any other requests? Is there any movement on sheaves of modules? What do we need for etale cohomology? (just a definition, not any theorems about it)

[Johan Commelin]

We really need to get an API for flat morphisms. That seems to be blocking a bunch of other stuff.

[Johan Commelin]

And closed immersions.

[Kevin Buzzard]

Flat morphisms: I was holding off on developing an API for flat modules/algebras until we had some homological algebra, because it seemed to me that there are some pretty slick proofs of flatness results using Tor. Did we balance Tor yet?

[Johan Commelin]

We first need to be able to use the definition of flatness, right?

[Andrew Yang]

I think closed immersions would be a reasonable target.

[Johan Commelin]

I don't think we have a proof that $A \otimes M \to B \otimes M \to C \otimes M$ stays exact, if $M$ is a flat module.

[Kevin Buzzard]

Flat morphisms of schemes would need sheaves of modules, right?

[Johan Commelin]

We only have this file with a stubbed out definition, about tensoring with inclusions of ideals.

[Andrew Yang]

Johan Commelin said:

I don't think we have a proof that $A \otimes M \to B \otimes M \to C \otimes M$ stays exact, if $M$ is a flat module.

This is waiting for the proof that R-Mod has enough injectives, which is on its way.

[Johan Commelin]

Ooh! Do you have a proof sketch somewhere?

[Johan Commelin]

The proof in Stacks doesn't need "enough injectives", does it?

[Andrew Yang]

Kevin Buzzard said:

Flat morphisms of schemes would need sheaves of modules, right?

We could technically bypass this by defining flat morphisms to be morphisms that are flat on stalks?

[Andrew Yang]

This is the proof I am thinking of, which only needs the existence of a cogenerator and Baer's criterion.

[Johan Commelin]

Aah, nice!

[Johan Commelin]

How long do you think it'll take to get there?

[Andrew Yang]

It is apparently quite easy: See this gist.
The catch is that Baer's criterion was not proven for f.g. ideals, so we do not yet have the iff to the mathlib definition.
But I think we might as well remove the f.g. requirement for the mathlib definition and move on.

[Johan Commelin]

Wonderful! And what's the status with getting enough injectives?

[Adam Topaz]

This should be "easy'(ish) with "cofree" modules

[Adam Topaz]

Do we know that $\mathbb{Q}/\mathbb{Z}$ is injective over $\mathbb{Z}$?

[Johan Commelin]

Yup, we recently had a PR on divisible groups

[Andrew Yang]

It seems like we are two PRs away from knowing that Ab has enough injectives.
After that, since mathlib knows that injective objects are preserved by right adjoints, and we have the adjoint between Ab and R-Mod, it should be relatively easy to get.
All these work are due to @Jujian Zhang and he probably has a better grasp at the amount of stuff remaining.

[Jujian Zhang]

Yes, two PRs from Ab having enough objectives, in this PR, it is shown that adjoins functor a transfers enough injectives, then apply to this PR and an easy adjunction between restriction and coextension of scalars, then we have enough injectives for any R-mod

[Matej Penciak]

I've also been sitting on some work since March that shows any module is isomorphic to the direct limit of its finitely generated submodules. I don't know if it's very helpful, but if anyone wants to use it to bridge the gap from f.g. ideals to all ideals feel free to copy whatever you want from it: https://github.com/mpenciak/flat_modules/blob/main/src/finite_submodules.lean. (I bumped the mathlib version in July though)

I was hoping I'd use it to prove some stuff about flat modules but life got in the way, and I never got around to working on it more.

[Andrew Yang]

By the way, what is the current status on sheaves of modules? Have we settled on an approach? Is anyone building stuff on top of some approach to determine which is the most practical?

[Johan Commelin]

At least to me, it's not clear that we've converged on a certain design

[Kevin Buzzard]

My understanding was that @Jujian Zhang was working on one of the choices and we were going to see how it turned out (but the last time we spoke he had Covid)

[Jack J Garzella]

@Andrew Yang @Kevin Buzzard Here's a quick update on sheaves of modules:

After considering the options and some zulip discussions (see #maths > Definition of presheaf of modules) with @Adam Topaz, I am convinced that the only sustainable way to do sheaves of modules is to define them as module objects over monoid objects in the category of sheaves of abelian groups.

This removes the need to redo a bunch of code that already exists, and the code written in the process will also be useful for things like group schemes. I'm pretty sure that even if we do one of the other options, eventually it'll have to be rewritten this way. The disadvantage is that it's a bit of a challenge to prove that for a sheaf of modules $\mathcal{F}$, there is a module structure on $\mathcal{F}(U)$.

To demonstrate the viability of this approach, I set out to show that for a sheaf of monoids $\mathcal{F}$, there is a monoid structure on $\mathcal{F}(U)$. Unfortunately there have been a lot of false starts. Essentially, I spent most of the summer trying to prove a worse version of https://github.com/leanprover-community/mathlib/blob/4d0b6301ef962e6bd74462998943ce38b7adb132/src/category_theory/monoidal/internal/types.lean#L25,
which I wasn't aware was in mathlib (apparently the people in #maths > Definition of presheaf of modules weren't either?). After discovering this, essentially all that's left for this proof of concept (other than putting all the pieces together) should be proving that certain functors are lax monoidal based on the fact that they preserve limits (see #Is there code for X? > Monoidal functor from preserves limits/colimits). I'm not exactly sure why I'm struggling so much, perhaps I'm not using zulip correctly, or maybe it's just because I'm still very new?

Anyways, after this, I got a bit busy, but I want to take another crack sometime soon, like next week or the week after.

[Kevin Buzzard]

@Jujian Zhang what do you think?

[Adam Topaz]

We should have module objects over monoid objects in monoidal categories anyway so we may as well start there.

[Jujian Zhang]

I am not very familiar with the maths of this approach, it sounds like a unified approach. In this approach, how easy/hard it would be to define coherent and quasi coherent sheaves of modules?

[Scott Morrison]

We already have module objects over monoid objects in monoidal categories. docs#Mod

[Scott Morrison]

I'm embarrassed to have lost track of this, but someone did the 2-category of algebras/bimodules/intertwiners internal to a monoidal category, as well.

[Damiano Testa]

Dear All,

sorry for coming late to this discussion: I am having a bad case of teaching and Covid and am still struggling to recover from both!

I see that there are already quite a few people working on a categorical approach to algebraic geometry.

I know that I have said this in the past, but a quick way to start proving stuff about algebraic varieties is to use the functor of points (maybe even simply on affine schemes). I think that this could also be suitable for an "independent start".

For a concrete proposal, defining and computing the set of $R$-valued points of affine space over $\mathbb{Z}$ could be a fun project.

[Adam Topaz]

I think the right approach is to define the Zariski topology on the category of rings, show that representable presheaves are sheaves, and show an equivalence of categories between the category of schemes and the sheaves on this topology which are locally representable.

[Adam Topaz]

Sorry to hear about covid/teaching. I hope things are better now!

[Damiano Testa]

Thanks, Adam! I am feeling better, but still have some side-effects. I am also recovering from Covid! :upside_down:

[Joël Riou]

I have been thinking of a different approach for (pre)sheaves of modules. Instead of using the symmetric monoidal structure given by the tensor product of (pre)sheaves of abelian groups, and taking modules over monoid objects, a more direct (and lower tech) approach would be to develop notions of (abelian) group objects, ring objects, module objects, internally to categories. In the case of (pre)sheaves of sets, this would give the notion of (pre)sheaves of modules (over a "nonconstant" ring). In the case of the category of schemes, this also allows the definition of groups schemes.

I recently had the idea of defining internal A objects in a category C, when A is a concrete category, as follows:

/-- The category of internal `A`-objects in the category `C`. -/
structure internal (A : Type u₂) [category.{v₂} A] [concrete_category.{v₁} A]
  (C : Type u₁) [category.{v₁} C] :=
(obj : C)
(presheaf : Cᵒᵖ ⥤ A)
(iso : yoneda.obj obj ≅ presheaf ⋙ forget A)

Abelian group objects in C are internal Ab C. Ring objects are internal Ring C. All the structure is on the yoneda presheaf associated to a certain object. This is very much the way group schemes are sometimes defined in the literature: this is a scheme G for which the functor $Hom(-,G)$ is endowed with a functorial structure of group. (Note that I do not assume that the category C has finite products, but I can show that if C has some binary products and a terminal object, an internal Ab C structure on X : C is basically the same as the datum of a zero morphism from the terminal object, a neg automorphism and an addition morphism prod X X ⟶ X satisfying some relations).

Then, given R : internal Ring C and M : internal Ab C, an R-module structure module R M can be introduced. If F : C ⥤ D is a functor which preserves finite products, then there are induced functors internal Ab C ⥤ internal Ab D, and with some extra work, the same would be true for Ring-objects, and modules. Then, using that internal abelian group objects in Type are abelian groups, etc, we can get module structures on the section of a sheaf of Modules using the evaluation functors.

I have been able to define most of this (and also construct the additive group scheme Gₐ : internal Ab Scheme in this manner).
My very draft code (with a few unsignificant sorries) is in the group-object branch of mathlib
https://github.com/leanprover-community/mathlib/compare/master...group-object

[Adam Topaz]

@Joël Riou this is similar to an idea I had while doing some experiments with universal algebra (in lean4). What I want to do is write some macros/commands that would generate classes in the algebraic hierarchy, as well as the relevant category of bundled objects, and this was essentially the idea I had to generate the category of internal objects associated to an algebraic gadget. Doing this for structures with more than one sort adds a layer of complexity though.

[Adam Topaz]

In case you're interested, here's what I wrote so far along these lines -- it's mostly hacked together at this point, and so far it's just about "introducing operations and notations." Adding axioms is the next step. I haven't had much time to work on this for a little while, unfortunately.

import Lean
open Lean Elab Command

inductive OpKind
| generic : String → Nat → OpKind
| const : String → String → OpKind
| zero : String → OpKind
| one : String → OpKind
| unary : String → String → OpKind
| binfix : String → String → OpKind
deriving Inhabited

def OpKind.arity : OpKind → Nat
| .generic _ n => n
| .const _ _ => 0
| .zero _ => 0
| .one _ => 0
| .unary _ _ => 1
| .binfix _ _ => 2

declare_syntax_cat lang_gen
syntax "generic" str num : lang_gen
syntax "const" str str : lang_gen
syntax "unary" str str : lang_gen
syntax "infix" str str : lang_gen
syntax "zero" str : lang_gen
syntax "one" str : lang_gen

def TSyntax.toOpKind : TSyntax `lang_gen → OpKind
| `(lang_gen| generic $s:str $n:num) => OpKind.generic s.getString n.getNat
| `(lang_gen| one $s:str) => OpKind.one s.getString
| `(lang_gen| zero $s:str) => OpKind.zero s.getString
| `(lang_gen| infix $s:str $t:str) => OpKind.binfix s.getString t.getString
| _ => panic! "oops!"

def OpKind.toIdent : OpKind → Ident
| .generic s _ => mkIdent s
| .one s => mkIdent s
| .zero s => mkIdent s
| .binfix s _ => mkIdent s
| _ => panic! "oops!"

def mkType (t : Term) (n : Nat) : MacroM Term :=
match n with
| 0 => `($t)
| (n+1) => do `($t → $(← mkType t n))

def mkTypes (t : Term) (ns : Array Nat) : MacroM (Array Term) := do
  let mut out := #[]
  for i in ns do
    out := out.push (← mkType t i)
  return out

def addNotation (op : OpKind) (s : Ident) : MacroM Syntax :=
match op with
| .binfix nm nt => `(infix:12 $(Syntax.mkStrLit nt):str => $(mkIdent nm))
| .one nm => `(instance OfNatOne (α : Type _) [$s α] : OfNat α (nat_lit 1) := ⟨$(mkIdent nm)⟩)
| .zero nm => `(instance OfNatZero (α : Type _) [$s α] : OfNat α (nat_lit 0) := ⟨$(mkIdent nm)⟩)
| _ => panic! "oops!"

elab "mk_raw_class" s:ident "[" xs:lang_gen,* "]" : command => do
  let args := xs.getElems.map TSyntax.toOpKind
  let names := args.map OpKind.toIdent
  let e := liftMacroM do `(class $s (α : Type _) where $[$names:ident : $(← mkTypes (← `(α)) $ args.map OpKind.arity)]*)
  elabCommand (← e)
  elabCommand (← `(namespace $s))
  for arg in args do
    elabCommand (← liftMacroM $ addNotation arg s)
  elabCommand (← `(end $s))

mk_raw_class gadget [
  infix "operation" "*",
  infix "another_operation" "+",
  infix "yet_another" "*+",
  one "mulId",
  zero "addId"]

example (α : Type _) [gadget α] (x y : α) : α := x * y
example (α : Type _) [gadget α] (x y : α) : α := x + y
example (α : Type _) [gadget α] (x y : α) : α := x *+ y
example (α : Type _) [gadget α] : α := 1
example (α : Type _) [gadget α] : α := 0

example (α : Type _) [gadget α] : gadget.mulId = (1 : α) := rfl

[Adam Topaz]

One issue is to understand what conditions on A one needs to impose to ensure that this category of internal A-objects is well-behaved (whatever that means). Certainly if A is the category of algebras for some Lawvere theory would suffice. Is there a simple characterization of such categories?

[David Wärn]

I think https://ncatlab.org/nlab/show/finitary+monad gives a characterisation of Lawvere theories among concrete categories?

[Adam Topaz]

Does that only work for finitary Lawvere theories?

[Adam Topaz]

Of course for algebra we're really only interested in finitary theories so that's okay

[Adam Topaz]

So I guess the category needs to be concrete, monadic w.r.t. the forgetful functor, and the forgetful functor should commute with filtered colimits.

[Adam Topaz]

To be a bit more precise, what I had in mind is something along these lines:

import category_theory.yoneda

structure is_monoid_hom {α β : Type*} (f : α → β) [monoid α] [monoid β] : Prop :=
(map_id : f 1 = 1)
(map_mul {x y} : f (x * y) = f x * f y)

open category_theory

structure internal_monoid (C : Type*) [category C] :=
(obj : C)
[str : ∀ Y : C, monoid ((yoneda.obj obj).obj (opposite.op Y))]
(is_monoid_hom_map : ∀ (Y₁ Y₂ : C) (f : Y₁ ⟶ Y₂), is_monoid_hom ((yoneda.obj obj).map f.op))

The benefit here is that we get a monoid instance "for free" on the hom sets, whereas with the approach above you would have to transfer that instance along some bijection.
On the other hand, to avoid replication with this approach we would have to use some metaprogramming, which is what I was (barely) starting to do with the code block above.

[Adam Topaz]

Also, if we replace yoneda with the docs#category_theory.ihom analogue, we could generalize this to (closed) monoidal categories which are not just cartesian.

[Joël Riou]

In my approach, in order to avoid too much code replication, I have used n-ary operations on the forgetful functor of the concrete category A for n=0,1,2,3... For example, on Ab, we have the 2-ary operation given by +; then, the yoneda presheaf M.presheaf of any Ab-object is equipped with a 2-ary operation, and if some binary product exists, it corresponds to a morphism prod M.obj M.obj ⟶ M.obj. The commutativity of + as a 2-ary operation on Ab implies the same for the corresponding operations on M.presheaf and M.obj.
(In order to do group schemes, the fact that there is a presheaf iso in my structure internal A C is very useful: in order to define the additive group scheme [actually a commutative ring scheme], I just consider the presheaf of abelian groups which sends a scheme to the global sections of the structure sheaf, and I check that when we apply the forgetful functor, the presheaf of sets we get is representable by Spec(ℤ[X]). If we had monoid/comm_group instances directly in the definition of internal group objects, I would think the definition of such group schemes would be slightly harder.

[Adam Topaz]

For the various algebraic categories where objects are just types bundled with some structure and the forgetful functor is the "identity" on morphisms, constructing internal objects in the two approaches would be essentially equivalent since the isomorphism in your approach would be essentially some wrapper around the identity.

[Adam Topaz]

Of course the correct answer is to do both things and provide an API to go back and forth ;)

[Adam Topaz]

Unfortunately, that assumes we have an infinite amount of time.

[Joël Riou]

I do not think so. In my file algebraic_geometry.group_schemes, I define the groupe scheme Gₐ like this:

def Gₐ' : internal CommRing Scheme.{u} :=
{ obj := Spec.obj (op (CommRing.of (polynomial (ulift.{u} ℤ)))),
  presheaf := Γ,
  iso := (Γ_Spec.adjunction.yoneda_nat_iso _).symm ≪≫
    (Γ.comp_yoneda_obj _).symm ≪≫ iso_whisker_left Γ polynomial_coyoneda_iso, }

def Gₐ : internal Ab Scheme.{u} := (internal.forget₂ CommRing Ring Scheme.{u} ⋙
  internal.forget₂ Ring Ab.{u} Scheme.{u}).obj Gₐ'

This iso is not at all the identity. If I had to define comm_group instances directly on the Hom-sets, the construction would be more painful. On the contrary here, the definition above is very easy.

[Johan Commelin]

@Joël Riou I think your approach is interesting. Does it allow us to define representations of group schemes in a similar way?

[Joël Riou]

Of course, one may define a linear representation of a group scheme as a morphism G ⟶ GL n for some n (assuming the linear group GL has been defined), but this is presumably not the best approach.

Alternatively, in general, one may introduce the notion of internal G-set in a category C, i.e. an object X : C equipped with an internal (yoneda) operation of G. Then, if X is also equipped with a structure of R-module, one may require that the action is R-linear.

If we apply this to the case R is the affine line, and put some restrictions on M (like "free of finite type"), this should give a reasonable definition of representations of group schemes in the sense that for any scheme S, the group of points G(S) would act linearly on M(S).

[Kevin Buzzard]

I can't get the coercion from SheavedSpace Ab to Top working. What am I doing wrong? Looks like a universe issue? I think putting all the {0}s there is really ugly. Can I get rid of them somehow?

import algebraic_geometry.sheafed_space

/-
already in mathlib:

instance algebraic_geometry.SheafedSpace.coe_carrier : has_coe (SheafedSpace C) Top :=
{ coe := λ X, X.carrier }
-/

--example : has_coe (algebraic_geometry.SheafedSpace Ab) Top := infer_instance -- fails

def forget1 (X : algebraic_geometry.SheafedSpace.{0} Ab.{0}) : Top.{0} := X -- works
--def forget2 (X : algebraic_geometry.SheafedSpace Ab) : Top := X -- fails
instance : has_coe (algebraic_geometry.SheafedSpace Ab) Top :=
{ coe := λ X, X.carrier}
-- def forget3 (X : algebraic_geometry.SheafedSpace Ab) : Top := X -- still fails

[Kevin Buzzard]

example (X0 : algebraic_geometry.SheafedSpace.{0} Ab.{0}) : false := sorry -- works fine
variable (X0 : algebraic_geometry.SheafedSpace.{0} Ab.{0}) -- maximum class-instance resolution depth has been reached

[Junyan Xu]

Kevin Buzzard said:

example (X0 : algebraic_geometry.SheafedSpace.{0} Ab.{0}) : false := sorry -- works fine
variable (X0 : algebraic_geometry.SheafedSpace.{0} Ab.{0}) -- maximum class-instance resolution depth has been reached

I think Lean is having trouble inferring the has_products instance, because this error goes away if you do these changes.

[Junyan Xu]

Even with that PR, some universe ascriptions are still necessary; the minimum you can get away with seems to be

universe u
def forget1 (X : algebraic_geometry.SheafedSpace Ab.{u}) : Top.{u} := X

[Kevin Buzzard]

Shouldn't the unused arguments linter be complaining before your PR?

[Kevin Buzzard]

In the max class instance logs there are things like

[class_instances] caching instance for Type → @limits.has_limits CommRing CommRing.large_category
λ (J : Type),
  @limits.has_smallest_limits_of_has_limits CommRing CommRing.large_category
    (@limits.has_smallest_limits_of_has_limits CommRing CommRing.large_category
       (@limits.has_smallest_limits_of_has_limits CommRing CommRing.large_category
          (@limits.has_smallest_limits_of_has_limits CommRing CommRing.large_category
             (@limits.has_smallest_limits_of_has_limits CommRing CommRing.large_category
                (@limits.has_smallest_limits_of_has_limits CommRing CommRing.large_category
                   (@limits.has_smallest_limits_of_has_limits CommRing CommRing.large_category
                      (@limits.has_smallest_limits_of_has_limits CommRing CommRing.large_category
                         (@limits.has_smallest_limits_of_has_limits CommRing CommRing.large_category
                            CommRing.has_limits))))))))

That does not look like a good thing to cache to me.

[Andrew Yang]

I think limits.has_smallest_limits_of_has_limits should not be an instance.

[Adam Topaz]

This is a problem because all the index categories for the finite limits were changed to be in universe 0

[Andrew Yang]

We still have docs#category_theory.limits.has_finite_limits_of_has_limits_of_size so things should be fine.
limits.has_finite_limits_of_has_limits_of_size almost always causes type interference loops and it was added as an instance due to my oversight. I thought we removed the instance tag during the preserves-limit-universe-generalization but it seems like it is still around.

[Junyan Xu]

Kevin Buzzard said:

Shouldn't the unused arguments linter be complaining before your PR?

Not sure why the linter didn't complain, but now I've completely removed the need of has_product for restricting a sheaf to an open subspace in #17361.

[Deepak Kamlesh]

Hello. This is Deepak. I am one of the graduate students taking Kevin Buzzard's TCC course on formalizing math this term. I was hoping to add some results on Noetherian Schemes following the Stacks project to get some credits for the course. I am just a beginner so I will probably need some help going forward and thank you all in advance. I have two questions at the moment. First of all it would be great to know if it is okay to go ahead with working on Noetherian schemes? I have looked at the mathlib rep and the pending pull requests which doesn't seem to have anything on the topic but Kevin suggested me to ask here and be sure.

[Andrew Yang]

Welcome! I believe no one is working on noetherian schemes.

[Andrew Yang]

You might want to imitate file#algebraic_geometry/morphisms/basic. Alternatively, you might be able to (ab)use the API on morphisms.

[Deepak Kamlesh]

Hello Andrew and thank you very much for your reply. Actually so far I have been having difficulties even with rather basic things like making some definitions and lemmas. The key reason being that there are so many layers of structure to schemes that I am often not even able to get to the correct types of objects to work with and poring over the documentation hasn't helped much especially with my limited understanding of lean. In particular, perhaps you could answer the following hopelessly ignorant question. Given a scheme how do I get to it's ring of global sections? There is a small section on the global section functor in the file on locally ringed spaces but I don't understand how to use it apparently. I need it to state the lemma below where I want to show that being a locally noetherian scheme implies existence of a noetherian affine cover.

lemma exists_noetherian_affine_cover_of_is_locally_noetherian :
(is_locally_noetherian X) → ∃ (𝒰 : Scheme.open_cover X) (i : 𝒰.J)
[∀ i, is_affine (𝒰.obj i)],
(is_noetherian_ring (op (𝒰.obj i)).Γ) := sorry

However I get the following error-

function expected at Scheme.Γ
term has type  Schemeᵒᵖ ⥤ CommRing

I suppose I need to pass an argument that converts a scheme to the underlying topological space as an open subset. Not clear at all how to do it though. Any help would be much appreciated. And apologies for such silly queries, I imagine I will probably have a few of those before I become a bit more proficient at this.

[Scott Morrison]

No, I think rather the problem is the Scheme.\Gamma is a functor, rather than a function that takes a Scheme as an argument.

[Scott Morrison]

Where possible, please post examples as a #mwe (i.e. with the imports required), so someone can just copy and paste your code into an editor and see the same error message.

[Scott Morrison]

I could easily show you the right syntax, except that I'm too lazy to reconstruct your imports and variables. :-)

[Andrew Yang]

It should be Scheme.Γ.obj (op (𝒰.obj i)). For a functor F, F.obj is the map on objects, and F.map is the map on arrows.

[Deepak Kamlesh]

Hello Scott. Yes, thank you very much for telling me about MWEs! l will keep it in mind next time. :)

[Deepak Kamlesh]

Andrew Yang said:

It should be Scheme.Γ.obj (op (𝒰.obj i)). For a functor F, F.obj is the map on objects, and F.map is the map on arrows.
`
Andrew, I see what you mean, however the error persists. Let me share a MWE below.

import algebraic_geometry.AffineScheme
import ring_theory.nilpotent
import topology.sheaves.sheaf_condition.sites
import category_theory.limits.constructions.binary_products
import algebra.category.Ring.constructions
import ring_theory.integral_domain
import ring_theory.noetherian
import ring_theory.local_properties
import algebraic_geometry.Scheme
import algebraic_geometry.properties

open topological_space opposite category_theory category_theory.limits Top
namespace algebraic_geometry

variable (X : Scheme)

class is_locally_noetherian: Prop :=
(locally_noetherian : ∀ (x : X.carrier), ∃ (U : X.affine_opens) (x : set U),
(is_noetherian_ring (X.presheaf.obj (op U))))

#check is_locally_noetherian

lemma exists_noetherian_affine_cover_of_is_locally_noetherian :
(is_locally_noetherian X) → ∃ (𝒰 : Scheme.open_cover X) (i : 𝒰.J)
[∀ i, is_affine (𝒰.obj i)],
(is_noetherian_ring ((𝒰.obj i).Γ.obj (op (𝒰.obj i)))) := sorry

[Andrew Yang]

(𝒰.obj i).Γ.obj (op (𝒰.obj i)) -> Scheme.Γ.obj (op (𝒰.obj i))

[Deepak Kamlesh]

Andrew Yang said:

(𝒰.obj i).Γ.obj (op (𝒰.obj i)) -> Scheme.Γ.obj (op (𝒰.obj i))

Yes, haha, success! It works. Sorry, I misunderstood you at first. Thanks.

[Deepak Kamlesh]

Another issue I have struggled with is how to define quasi-compactness for schemes.
There is a function is_compact for topological spaces however it takes as input a subset of the underlying space.
But again I am not sure how to convert a scheme into a set since Scheme.carrier only gives me a Top type.
Below is the corresponding MWE.

import algebraic_geometry.AffineScheme
import ring_theory.nilpotent
import topology.sheaves.sheaf_condition.sites
import category_theory.limits.constructions.binary_products
import algebra.category.Ring.constructions
import ring_theory.integral_domain
import ring_theory.noetherian
import ring_theory.local_properties
import algebraic_geometry.Scheme
import algebraic_geometry.properties
import set_theory.zfc.basic

open topological_space opposite category_theory category_theory.limits Top
namespace algebraic_geometry

variable (X : Scheme)

class is_locally_noetherian: Prop :=
(locally_noetherian : ∀ (x : X.carrier), ∃ (U : X.affine_opens) (x : set U),
(is_noetherian_ring (X.presheaf.obj (op U))))

namespace noetherian_scheme

#check is_compact

class is_noetherian: Prop :=
(locally_noetherian : is_locally_noetherian X)
(quasi_compact : is_compact X.carrier)

end noetherian_scheme
end algebraic_geometry

[Andrew Yang]

We use compact_space for types, and is_compact for subsets. A Top type has a coercion to Type, so compact_space X.carrier should work.

[Andrew Yang]

By the way, the (x : set U) in the definition is_locally_noetherian means "let x be an arbitrary subset of U". You should write (h : x ∈ U.val) instead. (U.val is the underlying open set of U : X.affine_opens)

[Kevin Buzzard]

@Deepak Kamlesh the whole thing might look completely intimidating right now but there is a logic to all of this, and you'll figure it out if you keep working on problems. Mathematicians are for example constantly using the "fact" that a functor "is" a function, but in Lean a functor has a component which is a function on objects and another component which is a function on morphisms, and after a while you'll start thinking about these things in the correct way, and learning about how you can look up what the answer to your questions are rather than having to ask them. Until that point please continue asking! I am also learning algebraic geometry in Lean right now, I'm trying to define sheaves of modules and it's the first time I've used the alg geom API, but I'm at the stage where I can figure out most things myself. My experimental repo is here https://github.com/ImperialCollegeLondon/tcc-lean-alg-geom-2022 .

[Deepak Kamlesh]

Andrew Yang said:

By the way, the (x : set U) in the definition is_locally_noetherian means "let x be an arbitrary subset of U". You should write (h : x ∈ U.val) instead. (U.val is the underlying open set of U : X.affine_opens)

Thanks a lot for pointing this out! I was unsure about that part of my definition.

[Deepak Kamlesh]

Thanks for your support Kevin! I will keep working on it indeed. :)

[Kevin Buzzard]

By the way I'm learning by teaching and I'm uploading my classes to YouTube on the Xena project channel

[Deepak Kamlesh]

Hello. I am trying to prove (2 implies 1) of Lemma 28.5.2 from the Stacks projects (https://stacks.math.columbia.edu/tag/01OU) which says that if every affine open subset of a scheme has a noetherian ring of global sections then the scheme itself is locally noetherian. My strategy is to just make use of the affine cover that exists for a scheme to do this. Of course there are more steps to actually implement this in Lean and along the way I reach a stage where I have to prove that a certain open subset is affine. And I do have an isomorphism with Spec R for some R which is what the goal is asking for but there is some subtle distinction that I am not able to resolve and it's causing a type mismatch. I would be grateful in case anyone can illuminate what's going on. I am providing a minimal code below. Thank you.

import algebraic_geometry.AffineScheme
import ring_theory.nilpotent
import topology.sheaves.sheaf_condition.sites
import category_theory.limits.constructions.binary_products
import algebra.category.Ring.constructions
import ring_theory.integral_domain
import ring_theory.noetherian
import ring_theory.local_properties
import algebraic_geometry.Scheme
import algebraic_geometry.properties
import set_theory.zfc.basic


open topological_space opposite category_theory category_theory.limits Top
open algebraic_geometry.Scheme
open classical
namespace algebraic_geometry

variable (X : Scheme)

class is_locally_noetherian: Prop :=
(locally_noetherian : ∀ (x : X.carrier), ∃ (U : X.affine_opens) (x : set U),
(is_noetherian_ring (X.presheaf.obj (op U))))

lemma is_locally_noetherian_of_forall_affine_open_global_section_is_noetherian_ring
  (h : ∀ (U : X.affine_opens), is_noetherian_ring (X.presheaf.obj (op U))) :
  (is_locally_noetherian X) :=
begin
split,
intro x,
have h2:= Scheme.local_affine X x,
rcases h2 with ⟨U, R, hU⟩,
have h3: is_affine (X.restrict (U.obj).open_embedding),
  {
    rw ← mem_Spec_ess_image,
    split,
    {
      have hiso := nonempty.some hU,
      have hsymm := iso.symm hiso,
      have hnew := nonempty.intro hsymm,
      exact hnew,
    },
    {
      exact op R,
    },
  },
  sorry
end

end algebraic_geometry

[Adam Topaz]

stacks#01OU

[Adam Topaz]

Your def of locally Noetherian seems wrong.

[Adam Topaz]

the second x is unrelated to the first one in the condition there.

[Reid Barton]

Right, you presumably meant ∃ (U : X.affine_opens), x \in U \and ...

[Andrew Yang]

By the way, the easiest method to obtain an affine open containing some x : X.carrier is either (X.affine_cover.map x).opens_range or to use docs#algebraic_geometry.algebraic_geometry.is_basis_affine_open and use the basis API.

[Andrew Yang]

For the former, the proof that it contains x is X.affine_cover.covers x, and you can show that it is an affine open using docs#algebraic_geometry.range_is_affine_open_of_open_immersion

[Calvin Lee]

Hi all! I'm working on some algebraic geometry that needs the sheaf of Kähler differentials. In In particular, this is a sheaf of modules, which is not currently possible to construct in mathlib.

Has there been any progress here in the past few months? Or would it make sense for me to hack on @Joël Riou 's branch to try to get something working?
@Jujian Zhang I was told you might know something about this as well

[Jujian Zhang]

Hi, there is an implementation of sheaves of modules in Kevin’s tcc course repository by defining them as sheaves of abelian groups that happens to have module structures. I have a complete implementation of presheaves of modules using monoid object in Mon_Ab and a mostly complete implementation of sheaves of modules using monoid object in the same branch with an adjunct ion between tensoring and internal Homs.

[Jujian Zhang]

This is the link to Kevin’s repo: https://github.com/ImperialCollegeLondon/tcc-lean-alg-geom-2022

[Jujian Zhang]

This is the link to my branch: https://github.com/leanprover-community/mathlib/tree/jjaassoonn/Mon_Ab

[Michael Stoll]

Jujian Zhang said:

This is the link to Kevin’s repo: https://github.com/ImperialCollegeLondon/tcc-lean-alg-geom-2022

Are the promised youtube videos somewhere? @Kevin Buzzard

[Jujian Zhang]

https://youtu.be/-wj-eCGv1D4 This is the first one. But I couldn’t find a playlist.

[Calvin Lee]

Jujian Zhang said:

This is the link to my branch: https://github.com/leanprover-community/mathlib/tree/jjaassoonn/Mon_Ab

thanks this looks really nice, I'll see if there's anything I can do to clean up the sorries

[Michael Stoll]

Jujian Zhang said:

https://youtu.be/-wj-eCGv1D4 This is the first one. But I couldn’t find a playlist.

Searching for "Formalising algebraic geometry" on youtube finds the first three lectures. (I had been trying "Algebraic geometry experiments"...)

[Kevin Buzzard]

There is every chance that I forgot to upload the last one, although there's also every chance that I'll have it lying around somewhere.

[Kevin Buzzard]

I'm not sure if they're particularly interesting, they're 2 hours and unedited

[Michael Stoll]

It's definitely fun watching them!

[Deepak Kamlesh]

Hello all. I have continued working on Noetherian schemes following the Stacks project. I am currently working on (1 implies 3) part of the lemma 28.5.2 (https://stacks.math.columbia.edu/tag/01OU) and I have a query. In the minimal working example included below I have an existential quantifier in the goal and for some reason the use tactic won't work which is quite weird. I am not sure if it's trivial and I am too sleepy too see it or if there is something non-trivial going on. Any help would be much appreciated, thank you!

import algebraic_geometry.AffineScheme
import topology.sheaves.sheaf_condition.sites
import category_theory.limits.constructions.binary_products
import algebra.category.Ring.constructions
import ring_theory.noetherian
import algebraic_geometry.Scheme
import algebraic_geometry.properties
import algebraic_geometry.locally_ringed_space
import topology.basic

noncomputable theory
open_locale classical

open topological_space opposite category_theory category_theory.limits Top
open algebraic_geometry.Scheme
open classical
namespace algebraic_geometry

variable (X : Scheme)

class is_locally_noetherian: Prop :=
(locally_noetherian : ∀ (x : X.carrier), ∃ (U : X.affine_opens), (x ∈ U.val) ∧
(is_noetherian_ring (X.presheaf.obj (op U))))

class is_noetherian: Prop :=
(locally_noetherian : is_locally_noetherian X)
(quasi_compact : compact_space X.carrier)

namespace noetherian

lemma exists_noetherian_affine_cover_of_is_locally_noetherian
  [h : is_locally_noetherian X] : ∃ (𝒰 : Scheme.open_cover X)(i : 𝒰.J),
  (∀ i, is_affine (𝒰.obj i)) ∧
  (is_noetherian_ring (Scheme.Γ.obj (op (𝒰.obj i)))) :=
begin
have h2 := @is_locally_noetherian.locally_noetherian X h,
choose hx hU h_noeth using h2,
let hprop : X.carrier → Prop :=
λ x, is_affine_open (hx x).val,
let haffine : Π (x : X.carrier), hprop x := λ x, (hx x).prop,
have hcover : open_cover X :=
  {
    J := X.carrier,
    obj := λ x, Scheme.Spec.obj (op $ X.presheaf.obj $ op (hx x)),
    map := λ x, begin
    exact is_affine_open.from_Spec (haffine x),
    end,
    f := λ x, x,
    is_open := λ x, begin
    exact is_affine_open.is_open_immersion_from_Spec (haffine x),
    end,
    covers := λ x, begin
    have hrange := is_affine_open.from_Spec_range (haffine x),
    rw hrange,
    exact hU x,
    end,
  },
use hcover,
sorry
end

end noetherian

end algebraic_geometry

[Johan Commelin]

@Deepak Kamlesh if you click on open_cover in your goal state, you will see that the universe variables don't line up.

[Johan Commelin]

universe u

variable (X : Scheme.{u})

[Johan Commelin]

lemma exists_noetherian_affine_cover_of_is_locally_noetherian
  [h : is_locally_noetherian X] : ∃ (𝒰 : Scheme.open_cover.{u u} X) (i : 𝒰.J),

[Johan Commelin]

I added .{u u} in that final line

[Johan Commelin]

Now use works

[Deepak Kamlesh]

@Johan Commelin
Yes, I see that. Thank you for your prompt help. I am afraid I don't have experience with handling type level universes so I doubt I would have noted the error myself. And also thank you for the correct solution. :)

[Kevin Buzzard]

We allow covers of schemes in universe u to be indexed by a type in universe v? The world has gone mad!

[Johan Commelin]

Well, I can imagine v = 0 being quite useful.

[Kevin Buzzard]

Yes but I can only imagine the case u=v=0 being useful ;-)

[Kevin Buzzard]

Maybe when we do representable functors someone will come up with an outlandish construction which constructs the representing object in a universe one higher, but I don't know of any such argument off the top of my head. I've seen etale cohomology groups showing up in the wrong universe and then having to be tamed, but I don't think I've seen schemes themselves doing this.

[Deepak Kamlesh]

Hello. I have come across a situation where I have the ring of sections of an affine open subset and I want to prove that the application of the Spec functor to it, followed by the Gamma functor gives the same ring back. I think I need to use the Gamma Spec adjunction in some way to prove it. But I don't quite see how to do it. I can't make sense of the lean file on adjunction perhaps because it's using definitions and results from the lean file on category theory which I am unfamiliar with. So any help that might demystify the situation would be much appreciated. It's the last remaining hypothesis in the proof below, MWE included. Thank you.

import algebraic_geometry.AffineScheme
import topology.sheaves.sheaf_condition.sites
import category_theory.limits.constructions.binary_products
import algebra.category.Ring.constructions
import ring_theory.noetherian
import algebraic_geometry.Scheme
import algebraic_geometry.properties
import algebraic_geometry.locally_ringed_space
import topology.basic

noncomputable theory
open_locale classical

open topological_space opposite category_theory category_theory.limits Top
open algebraic_geometry.Scheme
open classical
namespace algebraic_geometry

universe u
variable (X : Scheme.{u})

class is_locally_noetherian: Prop :=
(locally_noetherian : ∀ (x : X.carrier), ∃ (U : X.affine_opens), (x ∈ U.val) ∧
(is_noetherian_ring (X.presheaf.obj (op U))))

class is_noetherian: Prop :=
(locally_noetherian : is_locally_noetherian X)
(quasi_compact : compact_space X.carrier)

namespace noetherian

lemma exists_noetherian_affine_cover_of_is_locally_noetherian
  [h : is_locally_noetherian X] : ∃ (𝒰 : Scheme.open_cover.{u u} X),
  ∀ (i: 𝒰.J), is_affine (𝒰.obj i) ∧
  (is_noetherian_ring (Scheme.Γ.obj (op (𝒰.obj i)))) :=
begin
have h2 := @is_locally_noetherian.locally_noetherian X h,
choose hx hU h_noeth using h2,
let hprop : X.carrier → Prop :=
λ x, is_affine_open (hx x).val,
let haffine : Π (x : X.carrier), hprop x := λ x, (hx x).prop,
let hcover : open_cover X :=
  {
    J := X.carrier,
    obj := λ x, Scheme.Spec.obj (op $ X.presheaf.obj $ op (hx x)),
    map := λ x, begin
    exact is_affine_open.from_Spec (haffine x),
    end,
    f := λ x, x,
    is_open := λ x, begin
    exact is_affine_open.is_open_immersion_from_Spec (haffine x),
    end,
    covers := λ x, begin
    have hrange := is_affine_open.from_Spec_range (haffine x),
    rw hrange,
    exact hU x,
    end,
  },
use hcover,
intro x,
have hj : (x : hcover.J) = (x: X.carrier) := rfl,
split,
  {
    apply algebraic_geometry.Spec_is_affine (op $ X.presheaf.obj $ op (hx x)),
  },
have hnew : hcover.obj x = Scheme.Spec.obj (op $ X.presheaf.obj $ op (hx x)) := rfl,
rw hnew,
have heq : (Γ.obj (op (Spec.obj (op (X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (op ↑(hx x))))))) =
(X.presheaf.obj (op (hx x))) := sorry,
rw heq,
apply h_noeth x,
end

end noetherian
end algebraic_geometry

[Johan Commelin]

For that you need more than just an adjunction.

[Johan Commelin]

You need this file: src/algebraic_geometry/Gamma_Spec_adjunction.lean

[Kevin Buzzard]

You need that it's a "Galois insertion" rather than just a "Galois connection" but I don't know the category theoretic terminology for this (you need that the unit of the adjunction is an equivalence)

[Deepak Kamlesh]

I have a situation in my proof where I have an isomorphism of two rings in the opposite category to commutative rings. However I want to change this to get the isomorphism in the category of commutative rings. I checked the opposite Lean file and there is a theorem in case of equality but not isomorphism. There is another result about a type level equivalence between a type and it's opposite but when I apply it gives the opposite in the category of isomorphisms not the individual rings themselves. Any suggestions on how to resolve this will be of great help. MWE below. Thank you.

import algebraic_geometry.AffineScheme
import topology.sheaves.sheaf_condition.sites
import category_theory.limits.constructions.binary_products
import algebra.category.Ring.constructions
import ring_theory.noetherian
import algebraic_geometry.Scheme
import algebraic_geometry.properties
import algebraic_geometry.locally_ringed_space
import topology.basic

noncomputable theory
open_locale classical

open topological_space opposite category_theory category_theory.limits Top
open algebraic_geometry.Scheme
open classical
namespace algebraic_geometry

universe u
variable (X : Scheme.{u})

class is_locally_noetherian: Prop :=
(locally_noetherian : ∀ (x : X.carrier), ∃ (U : X.affine_opens), (x ∈ U.val) ∧
(is_noetherian_ring (X.presheaf.obj (op U))))

class is_noetherian: Prop :=
(locally_noetherian : is_locally_noetherian X)
(quasi_compact : compact_space X.carrier)

namespace noetherian

lemma exists_noetherian_affine_cover_of_is_locally_noetherian
  [h : is_locally_noetherian X] : ∃ (𝒰 : Scheme.open_cover.{u u} X),
  ∀ (i: 𝒰.J), is_affine (𝒰.obj i) ∧
  (is_noetherian_ring (Scheme.Γ.obj (op (𝒰.obj i)))) :=
begin
have h2 := @is_locally_noetherian.locally_noetherian X h,
choose hx hU h_noeth using h2,
let hprop : X.carrier → Prop :=
λ x, is_affine_open (hx x).val,
let haffine : Π (x : X.carrier), hprop x := λ x, (hx x).prop,
let hcover : open_cover X :=
  {
    J := X.carrier,
    obj := λ x, Scheme.Spec.obj (op $ X.presheaf.obj $ op (hx x)),
    map := λ x, begin
    exact is_affine_open.from_Spec (haffine x),
    end,
    f := λ x, x,
    is_open := λ x, begin
    exact is_affine_open.is_open_immersion_from_Spec (haffine x),
    end,
    covers := λ x, begin
    have hrange := is_affine_open.from_Spec_range (haffine x),
    rw hrange,
    exact hU x,
    end,
  },
use hcover,
intro x,
have hj : (x : hcover.J) = (x: X.carrier) := rfl,
split,
  {
    apply algebraic_geometry.Spec_is_affine (op $ X.presheaf.obj $ op (hx x)),
  },
have hnew : hcover.obj x = Scheme.Spec.obj (op $ X.presheaf.obj $ op (hx x)) := rfl,
rw hnew,
have hiso := (category_theory.as_iso Γ_Spec.adjunction.counit).app (op (X.presheaf.obj (op (hx x)))),
have hcomp : (Spec ⋙ Γ.right_op).obj (op $ X.presheaf.obj $ op (hx x)) =
op (Γ.obj (op (Spec.obj (op $ X.presheaf.obj $ op (hx x))))) := rfl,
rw hcomp at hiso,
have hid : (𝟭 CommRingᵒᵖ).obj (op $ X.presheaf.obj $ op (hx x)) =
(op $ X.presheaf.obj $ op (hx x)) := rfl,
rw hid at hiso,
have hcong : (Γ.obj (op (Spec.obj (op $ X.presheaf.obj $ op (hx x))))) ≅
(X.presheaf.obj (op (hx x))) := begin
apply equiv_to_opposite.inv_fun,
apply hiso,
sorry
end,

sorry
end

end noetherian
end algebraic_geometry

[Adam Topaz]

docs#quiver.hom.unop

[Adam Topaz]

docs#category_theory.iso.unop

[Deepak Kamlesh]

I want to prove that a ring S is noetherian and I know that another ring R is isomorphic to S and that R is noetherian. So I tried to use the theorem 'is_noetherian_ring_of_ring_equiv' from the lean file https://github.com/leanprover-community/mathlib/blob/195fcd60ff2bfe392543bceb0ec2adcdb472db4c/src/ring_theory/noetherian.lean#L532.
However I am getting an error which I don't understand. I think it might be a type universe level issue that I don't know how to resolve. It's the last step left in the proof so it would be great to know an answer. Also where might one learn more about how to resolve such errors? Neither the book mathematics in lean nor theorem proving in Lean discuss this if I remember correctly. Thank you for your time.

import algebraic_geometry.AffineScheme
import topology.sheaves.sheaf_condition.sites
import category_theory.limits.constructions.binary_products
import algebra.category.Ring.constructions
import ring_theory.noetherian
import algebraic_geometry.Scheme
import algebraic_geometry.properties
import algebraic_geometry.locally_ringed_space
import topology.basic

noncomputable theory
open_locale classical

open topological_space opposite category_theory category_theory.limits Top
open algebraic_geometry.Scheme
open classical
namespace algebraic_geometry

universe u
variable (X : Scheme.{u})

class is_locally_noetherian: Prop :=
(locally_noetherian : ∀ (x : X.carrier), ∃ (U : X.affine_opens), (x ∈ U.val) ∧
(is_noetherian_ring (X.presheaf.obj (op U))))

class is_noetherian: Prop :=
(locally_noetherian : is_locally_noetherian X)
(quasi_compact : compact_space X.carrier)

namespace noetherian

lemma exists_noetherian_affine_cover_of_is_locally_noetherian
  [h : is_locally_noetherian X] : ∃ (𝒰 : Scheme.open_cover.{u u} X),
  ∀ (i: 𝒰.J), is_affine (𝒰.obj i) ∧
  (is_noetherian_ring (Scheme.Γ.obj (op (𝒰.obj i)))) :=
begin
have h2 := @is_locally_noetherian.locally_noetherian X h,
choose hx hU h_noeth using h2,
let hprop : X.carrier → Prop :=
λ x, is_affine_open (hx x).val,
let haffine : Π (x : X.carrier), hprop x := λ x, (hx x).prop,
let hcover : open_cover X :=
  {
    J := X.carrier,
    obj := λ x, Scheme.Spec.obj (op $ X.presheaf.obj $ op (hx x)),
    map := λ x, begin
    exact is_affine_open.from_Spec (haffine x),
    end,
    f := λ x, x,
    is_open := λ x, begin
    exact is_affine_open.is_open_immersion_from_Spec (haffine x),
    end,
    covers := λ x, begin
    have hrange := is_affine_open.from_Spec_range (haffine x),
    rw hrange,
    exact hU x,
    end,
  },
use hcover,
intro x,
have hj : (x : hcover.J) = (x: X.carrier) := rfl,
split,
  {
    apply algebraic_geometry.Spec_is_affine (op $ X.presheaf.obj $ op (hx x)),
  },
have hnew : hcover.obj x = Scheme.Spec.obj (op $ X.presheaf.obj $ op (hx x)) := rfl,
rw hnew,
have hiso := (category_theory.as_iso Γ_Spec.adjunction.counit).app (op (X.presheaf.obj (op (hx x)))),
have hcomp : (Spec ⋙ Γ.right_op).obj (op $ X.presheaf.obj $ op (hx x)) =
op (Γ.obj (op (Spec.obj (op $ X.presheaf.obj $ op (hx x))))) := rfl,
rw hcomp at hiso,
have hid : (𝟭 CommRingᵒᵖ).obj (op $ X.presheaf.obj $ op (hx x)) =
(op $ X.presheaf.obj $ op (hx x)) := rfl,
rw hid at hiso,
have hcong : (Γ.obj (op (Spec.obj (op $ X.presheaf.obj $ op (hx x))))) ≅
(X.presheaf.obj (op (hx x))) := begin
have hunop := iso.unop hiso,
rw unop_op at hunop,
rw unop_op at hunop,
exact hunop.symm,
end,
have hnoth := h_noeth x,
let hcong := hcong.symm,
apply is_noetherian_ring_of_ring_equiv ↥(X.presheaf.obj (op ↑(hx x))) hcong,
end

end noetherian
end algebraic_geometry

[Adam Topaz]

It seems that you're using the python code environment instead of the default (or the lean one). You can edit your message and replace python with lean. That should render your code a little better.

[Deepak Kamlesh]

Error resolved to my previous message, thank you.

[Kevin Buzzard]

This is a very impressive piece of work! You're clearly very nearly there. I hope I'll find some time later to sort out your last problem if someone else doesn't beat me to it. Unfortunately I don't know my way around this part of the library well enough, but it seems to me that one thing you need is a solution to this sorry:

example (A B : CommRing) (h : A ≃+* B) : A ≅ B :=
begin
  library_search, -- fails
end

Then you can apply this and your attempt to use is_noetherian_ring_of_ring_equiv is more likely to work. I tried exact h but it doesn't work.

[Eric Wieser]

We already solved that in this thread

[Kevin Buzzard]

We need the other way but that's a good place to look!

[Eric Wieser]

Assume "we need" refers to the message above, I think it's precisely the same code as in the other thread

[Eric Wieser]

docs#ring_equiv.to_CommRing_iso is your sorry, modulo defeq for the coe_sort on CommRing

[Eric Wieser]

@Deepak Kamlesh: In general, I'd recommend against posting the same question in multiple topics or streams; if you think your question is relevant in both places, create the post in one place, and link to it from the other

[Deepak Kamlesh]

Kevin Buzzard said:

This is a very impressive piece of work! You're clearly very nearly there. I hope I'll find some time later to sort out your last problem if someone else doesn't beat me to it. Unfortunately I don't know my way around this part of the library well enough, but it seems to me that one thing you need is a solution to this sorry:

example (A B : CommRing) (h : A ≃+* B) : A ≅ B :=
begin
  library_search, -- fails
end

Then you can apply this and your attempt to use is_noetherian_ring_of_ring_equiv is more likely to work. I tried exact h but it doesn't work.

Dear Kevin, we already figured it out in the noetherian modules chat and finished the proof. Thank you.

[Eric Wieser]

Otherwise the communtiy tries to help you twice, which can be a waste of time!

[Deepak Kamlesh]

Eric Wieser said:

Otherwise the communtiy tries to help you twice, which can be a waste of time!

Yes, I will keep that in mind Eric, thank you. Unfortunately I was a bit desperate today for reasons of deadline.

[Kevin Buzzard]

Deadline?? Is this for some course somewhere?

[Kevin Buzzard]

FWIW

def CommRing_ring_equiv_to_iso (A B : CommRing) (h : A ≃+* B) : A ≅ B :=
{ hom := h,
  inv := h.symm,
  hom_inv_id' := by ext1; simp only [comp_apply, ring_equiv.coe_to_ring_hom, ring_equiv.symm_apply_apply, id_apply],
  inv_hom_id' := by ext1; simp only [comp_apply, ring_equiv.coe_to_ring_hom, ring_equiv.apply_symm_apply, id_apply]}

and thanks Eric for stopping me; I'll get back to doing what I'm supposed to be doing!

[Deepak Kamlesh]

Kevin Buzzard said:

Deadline?? Is this for some course somewhere?

Kevin, yes, I am writing you an email now to sort it out.

[Kevin Buzzard]

Is this for my course???

[Kevin Buzzard]

OK got the email -- you passed :-)