noetherian modules

Stream: maths

[Johan Commelin]

What are the next steps for noetherian modules?
1. We want to prove that if M is noetherian, then so are all its submodules and quotients.
2. This suggests that we might quickly want is_noetherian to be a class.
3. To prove (1) we want to show that a linear map M -> N induces an order preserving map submodule R M -> submodule R N.

[Johan Commelin]

The map induced map in (3) is injective if M -> N is an inclusion or quotient map.

[Johan Commelin]

Is this induced map an example of (one side of) a Galois connection? And is it useful to know this?

[Reid Barton]

There are actually three maps forming two Galois connections I think

[Johan Commelin]

Taking image, taking inverse image, and ...?

[Reid Barton]

Whatever the right adjoint to the inverse image is

[Reid Barton]

The biggest submodule whose inverse image is contained in the original one

[Reid Barton]

I guess it's not useful

[Johan Commelin]

Right, so you have N' \sub N, and then you'dd take the image of f^{-1} N' \cap M?

[Johan Commelin]

Scratch that, that's nonsense

[Reid Barton]

Start with a submodule of M

[Johan Commelin]

Right,

[Johan Commelin]

Call it M', and put \cap M' in my formula

[Reid Barton]

It's those n whose inverse image is a subset of M'. I think

[Reid Barton]

You have it for just a map of sets also.

[Reid Barton]

It has a forall where the direct image has an exists

[Johannes Hölzl]

Yeah, sets and filters also have this strange right adjoint to preimage. I don't know if this is useful anywhere...

[Reid Barton]

Actually, now I think it doesn't exist for submodules

[Reid Barton]

Because the inverse image of zero might not be zero

[Reid Barton]

So the inverse image map doesn't preserve the empty sup

[Reid Barton]

So it can't have a right adjoint

[Reid Barton]

So ignore everything I said.

[Reid Barton]

Direct and inverse image of submodules should be a Galois connection though

[Johan Commelin]

Right, and I guess this is a general fact about subobjects in algebraic concrete categories...

[Johan Commelin]

So it would be cool if we could either deduce it from such a general fact, or have a subtype_galois_connection tactic (-;

[Reid Barton]

I guess we can start with the complete lattice of subobjects tactic and the span Galois insertion tactic

[Johannes Hölzl]

A galois_connection tactic would be nice, but I don't see how it should work. To prove that something is free (e.g. span, generator etc) is not for free.

[Johan Commelin]

No, I didn't mean that one. I meant the direct/inverse image connection.

[Johan Commelin]

That one is usually just a follow-your-nose result.

[Reid Barton]

You can take the intersection of all the subobjects which contain the given set. Basically get the complete lattice structure from the intersection instead

[Reid Barton]

But then in a particular case, you will probably want a more explicit description of the generated subobject.

[Johan Commelin]

Mario would say that we shouldn't automate this, but just go for it (-;

[Reid Barton]

Does the subobject instance tactic work for R-modules? Does it understand that the structure is module R?

[Johan Commelin]

this instance is already in mathlib

[Johan Commelin]

I didn't test the tactic, because that is not yet in mathlib

[Johan Commelin]

linear_algebra.subtype_module

[Mario Carneiro]

A galois_connection tactic would be nice, but I don't see how it should work. To prove that something is free (e.g. span, generator etc) is not for free.

span is not free when presented in a "constructive" way, i.e. linear combinations of elements in the set, but it is free given the Moore collection axioms. A Moore collection is a set of sets that is closed under arbitrary intersection (let's call these things closed sets). This enables the definition of a closure operator that is the span (i.e. the intersection of all closed sets containing S), and then there is some work to show that this operator has a constructive interpretation using an inductive family or what have you. Any algebraically presented subobject family like is_subgroup or is_submodule, where the assumptions all say "if these things are in the subgroup then these other things are in the subgroup", is a Moore collection, and there is a formulaic proof of such.

[Mario Carneiro]

This approach seems like a way to automate this, but it does not go via the galois connection, since that approach brings in the details of the constructive definition of span (here I mean constructive in the mathematician's sense) which are not as uniform

[Reid Barton]

Right so there are three definitions of, say, the submodule of M generated by a set S.

[Reid Barton]

1 is the intersection of the submodules containing S.

[Mario Carneiro]

If a Moore collection is generated by the closure with respect to a (possibly infinite) family of finite arity operators, then it is an algebraic closure system (ACS), which has still more properties for free. Almost all of the algebraic sub-things are ACSs

[Reid Barton]

2 is the set of elements which can be built up from S from the operations of a module, i.e., we define an inductive type of trees which are expressions in the language of R-modules.

[Reid Barton]

3 is the one in terms of linear combinations.

[Mario Carneiro]

(2) seems like an inductive definition that is amenable to automation in the same sense as I have suggested

[Reid Barton]

1 and 2 are automatable. 3 is not, you have to think of something which is a good "normal form" (roughly) and then prove a special theorem.

[Reid Barton]

I guess it probably doesn't matter much which definition we choose or whether the definitions are consistent between different kinds of structures

[Mario Carneiro]

If we want a one-line setup of the collection, the complete lattice, the span operator and the galois connection, it would be best to take one of the uniform versions as the definition, and leave the nonuniform version as a theorem to be proven separately

[Reid Barton]

I should look into this Moore system stuff. It sounds related to locally presentable categories (a locally finitely presentable category is the category of models of a finitary essentially algebraic theory) and there are some theorems about subobjects in them, though usually I don't care so much about those theorems.

[Mario Carneiro]

I learned about it first through metamath, see http://us.metamath.org/mpeuni/df-mre.html and http://us.metamath.org/mpeuni/df-acs.html which have some links to references. Wikipedia doesn't seem to have anything on it

[Johannes Hölzl]

Yeah, I should have looked into them the first time you mentioned them. I like the Examples section in https://ncatlab.org/nlab/show/Moore+closure :

What are examples? Better to ask what isn't an example!

[Reid Barton]

I see, so it looks a lot more general than subobjects in an algebraic theory.

[Mario Carneiro]

oh, looks like the WP reference is https://en.wikipedia.org/wiki/Closure_operator

[Mario Carneiro]

"finitary closure operator" in that article corresponds to what I called an ACS

[Scott Morrison]

Does anyone know why the noetherian branch isn't compiling?

[Scott Morrison]

@Chris Hughes, @Kenny Lau, what are the prospects of getting tensor products of commutative rings into mathlib?

[Kenny Lau]

I wrote half the file a month ago

[Patrick Massot]

is_add_group_hom is now in mathlib

[Patrick Massot]

https://github.com/leanprover/mathlib/commit/afd1c063638d611fda65db7499ccbd7257c90870

[Patrick Massot]

What is the current state of quotient groups by the way?

[Chris Hughes]

Kevin's stuff got merged. There's about 100 lines of the basic facts.

[Scott Morrison]

@Chris Hughes can you point me to it?

[Patrick Massot]

I was thinking of the left_cosets vs group_quotient issue

[Patrick Massot]

I think we have two competing versions

[Chris Hughes]

Everything's quotient_group.quotient now.

[Patrick Massot]

left_cosets disappeared?

[Chris Hughes]

Yes.

[Patrick Massot]

That's good news, but again something to be changed in Kenny's tensor product file

[Chris Hughes]

but quotient_group includes quotient by non normal subgroups

[Chris Hughes]

@Scott Morrison It's in group_theory/quotient_group

[Scott Morrison]

@Chris Hughes, oh, oops, I thought you were talking about tensor products of rings. :-)

[Patrick Massot]

couldn't we call this group.quotient instead of quotient_group? The later really looks like the quotient is a group

[Scott Morrison]

@Kenny Lau, are you going to PR that stuff on tensor products? I'd like to be able to use it!

[Chris Hughes]

I think group.quotient is a better name.

[Kenny Lau]

@Kenny Lau, are you going to PR that stuff on tensor products? I'd like to be able to use it!

give me some time

[Kenny Lau]

Tensor product PR: https://github.com/leanprover/mathlib/pull/303

[Kenny Lau]

@Scott Morrison further feature request?

[Kenny Lau]

@Patrick Massot you might be interested

[Patrick Massot]

thanks Kenny!

[Patrick Massot]

Kenny's tensor product is merged! I'm really super excited by the idea of mathlib taking advantage of Kenny's proving power!

[Kevin Buzzard]

rofl I was reviewing it

[Kenny Lau]

it's alright Kevin, I may still have things to add there anyway

[Kenny Lau]

I may prove the dimension theorem, and then I would prove that the dimension of tensor is the product of the dimension

[Johannes Hölzl]

@Kevin Buzzard was I too fast merging it? Any suggestions?

[Kevin Buzzard]

nothing serious. I'll finish my review. I am trying to get into the habit of reviewing mathlib PRs where the mathematics relates to the perfectoid project.

[Kevin Buzzard]

@Mario Carneiro just to let you know I am still working on the Noetherian branch of community mathlib. I have a proof that subs and quotients of Noeth are Noeth but it's currently broken as I fiddle with it to try and make things more general and reasonable. I'm sure there will still be lots of work to do when I finally make the PR, hopefully tomorrow. Admin got the better of me today, that and the fact that I kept having little insights about how to do things a little better than they were done before.

[Kevin Buzzard]

OK so I pushed the proof that a sub of a Noetherian module is Noetherian to community-mathlib, the Noetherian branch. I spent some time proving order embeddings which I could have probably avoided. I'd appreciate any feedback on the push. Am I supposed to open a PR to mathlib? I have littered my PR with comments, which of course will have to go in the end, but they're just to flag things I wasn't sure about or to explain what I was trying to do.

I also have a proof that quotients of Noetherian modules are Noetherian, but I was waiting for Chris' quotient module PR to be accepted -- I see that it was accepted an hour ago so I'll work on quotient modules later.

[Deepak Kamlesh]

Hello and apologies if this is the wrong forum to discuss this.
I am a DPhil student and I am writing some proofs on Noetherian schemes in Lean for a course project on Formalizing mathematics. I have come across a situation where 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's a type level universe issue. What I have provided is of type u but the expected argument is type max u ? but the ? in my argument is of type u so I am confused. I tried asking in the algebraic geometry forum but it's taking some time to get a reply so I thought I would try my luck here. MWE included below. 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

[Ruben Van de Velde]

Looks like you're got an equiv, but not a ring equiv

[Ruben Van de Velde]

And thanks for the #mwe

[Eric Wieser]

I think you need docs#category_theory.iso.CommRing_iso_to_ring_equiv

[Eric Wieser]

And have hnoth := h_noeth x, should be haveI hnoth := h_noeth x,

[Eric Wieser]

Then your proof goes through for me!

[Deepak Kamlesh]

Thank you Ruben and Eric. I tried the transformation to ring_equiv. However now I get a different error that says failed to synthesize type class instance for (X :Scheme). I am a beginner to Lean so I don't have much experience with handling errors in Lean, sorry. Could it be that the ring type changes so Lean can't recognize the Scheme definitions and results anymore? MWE below.

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,
have h_ringequiv := category_theory.iso.CommRing_iso_to_ring_equiv hcong,
have hfinal:= is_noetherian_ring_of_ring_equiv ↥(X.presheaf.obj (op ↑(hx x))) h_ringequiv,
sorry
end


end noetherian
end algebraic_geometry

[Eric Wieser]

You didn't apply my last haveI comment

[Deepak Kamlesh]

Eric Wieser said:

And have hnoth := h_noeth x, should be haveI hnoth := h_noeth x,

Oh I hadn't seen this message yet. Yes, that's great, yeah! It works. Thank you. :D

[Eric Wieser]

now I get a different error that says failed to synthesize type class instance for (X :Scheme)

For future reference, you've discarded the important part of the error message when you wrote this; the actual error was that it couldn't find is_noetherian_ring _ for some messy _.