Zulip Chat Archive

Stream: new members

Topic: Setting up definitions


view this post on Zulip Jakob Scholbach (Feb 12 2021 at 20:59):

I am working my way through the Mathematics in Lean tutorial, so I want to start beginning formalize some "real" notions, for example the condition that a module over a commutative ring is flat. Is there some tutorial or cheat sheet etc, how to even write down a definition? Is that supposed to be a theorem or a def? I am skimming through the mathlib files, but I don't yet see how the syntax would work out. Thanks!

view this post on Zulip Kevin Buzzard (Feb 12 2021 at 21:00):

The definition of flatness will be a def of type Prop.

view this post on Zulip Kevin Buzzard (Feb 12 2021 at 21:01):

definitions are hard to get right :-(

view this post on Zulip Kevin Buzzard (Feb 12 2021 at 21:03):

The big question is: which definition will you use?

view this post on Zulip Jakob Scholbach (Feb 12 2021 at 21:03):

My initial idea would be to say: for all injective maps of R-modules the tensor product with the module should still be injective.

view this post on Zulip Jakob Scholbach (Feb 12 2021 at 21:04):

As a test case: then show that all free modules are flat.

view this post on Zulip Kevin Buzzard (Feb 12 2021 at 21:04):

And which universes will everything be in?

view this post on Zulip Kevin Buzzard (Feb 12 2021 at 21:05):

This might all be in a branch of mathlib. @Johan Commelin ?

view this post on Zulip Jakob Scholbach (Feb 12 2021 at 21:06):

Being a beginner (for the moment I want to just play around and see a little bit of progress for myself) I would say the ring and the modules should be in the same universe.

view this post on Zulip Jakob Scholbach (Feb 12 2021 at 21:07):

Or is that problematic?

view this post on Zulip Johan Commelin (Feb 12 2021 at 21:09):

If it's just for fun to play around, that shouldn't be a problem

view this post on Zulip Jakob Scholbach (Feb 12 2021 at 21:10):

Where is a good place to read about the syntax of definitions in lean?

view this post on Zulip Johan Commelin (Feb 12 2021 at 21:11):

Of course Ql\mathbb Q_l is in universe Type 0, but etale cohomology of a scheme in Type 0 lives in Type 1, so with your definition those vector spaces wouldn't be flat... (assuming you define etale cohomology using the general topos theoretic machine)
But it's totally fine to ignore that issue for now.

view this post on Zulip Johan Commelin (Feb 12 2021 at 21:12):

@Jakob Scholbach Have you seen the video recordings of "Lean for the Curious Mathematician"?

view this post on Zulip Johan Commelin (Feb 12 2021 at 21:13):

https://www.youtube.com/watch?v=8mVOIGW5US4&list=PLlF-CfQhukNlxexiNJErGJd2dte_J1t1N

view this post on Zulip Johan Commelin (Feb 12 2021 at 21:14):

The ones on "Structures and classes" and "Building a xyz hierarchy" are probably most relevant if you want to learn about making definitions

view this post on Zulip Jakob Scholbach (Feb 12 2021 at 21:14):

I noticed that they are there, watched the one about category theory, but nothing else; nor did I work through the exercises. I'll check these out, thanks!

view this post on Zulip Johan Commelin (Feb 12 2021 at 21:14):

def flat (R M : Type) [comm_ring R] [add_comm_group M] [module R M] :=
-- some predicate goes here

view this post on Zulip Johan Commelin (Feb 12 2021 at 21:17):

At some point I wrote some code about tensoring linear maps with a module. In other words, give f ⁣:M1M2f \colon M_1 \to M_2 and another module MM, the induced map M1MM2MM_1 \otimes M \to M_2 \otimes M.
But I don't know if that code ended up in mathlib.

view this post on Zulip Johan Commelin (Feb 12 2021 at 21:17):

I think it's still waiting for attention by me or someone else: https://github.com/leanprover-community/mathlib/pull/4773

view this post on Zulip Eric Wieser (Feb 12 2021 at 21:40):

Is that docs#linear_map.prod_map?

view this post on Zulip Eric Wieser (Feb 12 2021 at 22:04):

Ah, tmul not prod

view this post on Zulip Adam Topaz (Feb 13 2021 at 03:44):

Here's one possible "definition" which doesn't have universe issues:

import ring_theory.ideal.basic
import linear_algebra.tensor_product

open_locale tensor_product

variables (A M : Type*) [comm_ring A] [add_comm_group M] [module A M]

def flat_aux (𝔞 : ideal A) : 𝔞 [A] M →ₗ[A] M := tensor_product.lift $
linear_map.mk₂ A (λ a m, ((a : A)  m))
(λ a b m, by simp [add_smul]) (λ a b m, by simp [ mul_smul, mul_comm])
(λ a m n, by simp) (λ a b m, by simp [ mul_smul, mul_comm])

def flat : Prop :=  (𝔞 : ideal A), function.injective $ flat_aux A M 𝔞

Of course, this is a bit backwards, since it's a theorem that this is equivalent to the "usual" definition of flatness :)

view this post on Zulip Kevin Buzzard (Feb 13 2021 at 09:28):

Of course it doesn't matter if things are defined in a nonstandard way as long as it's mathematically equivalent to the standard way. The question is whether one can build the standard API from the definition. This now is a much easier and more fun challenge because it only involves proving theorems

view this post on Zulip Johan Commelin (Feb 15 2021 at 05:44):

@Jakob Scholbach So there is a branch#flat-module of mathlib, in which I've tried to set up the basic theory for flatness.

view this post on Zulip Johan Commelin (Feb 15 2021 at 05:51):

I got stuck for two reasons:

  1. mathlib doesn't have enough basic lemmas about tensor products in all the different variants. Tensor product of modules is there, but ideally we will have base change, associativity of base change, etc... There is currently no framework that makes polynomial A a (not the) tensor product of A and polynomial int. I think we should have such a framework in order for things to work smoothly.
  2. As definition I chose the minimalist assertion: for every ideal II, the natural map IMMI \otimes M \to M is injective. Bootstrapping from this to the "usual" definition of preserving injectivity of arbitrary maps was painful. I tried to follow https://stacks.math.columbia.edu/tag/00HD but the proof became very awkard because Lean doesn't let you smoothly move between submodules and injective maps. Recently I didn't have time to work on this, but my gut feeling is that we should first prove a general "induction principle" for the category of RR-modules, that will say something like "if you have suitable predicate P on modules, then you only need to check it on finitely generated modules", and maybe another version that will say "if you have an even more suitable predicate Q, then you only need to check it on ideals". Once we have those results, the proof of stacks-tag 00HD should be "straightforward".

view this post on Zulip Thomas Browning (Feb 15 2021 at 06:21):

From my experience, proving these general induction principles is very worthwhile, particularly if it allows you to black-box a Zorn's lemma argument


Last updated: May 08 2021 at 04:14 UTC