## Stream: new members

### Topic: Setting up definitions

#### 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!

#### Kevin Buzzard (Feb 12 2021 at 21:00):

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

#### Kevin Buzzard (Feb 12 2021 at 21:01):

definitions are hard to get right :-(

#### Kevin Buzzard (Feb 12 2021 at 21:03):

The big question is: which definition will you use?

#### 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.

#### Jakob Scholbach (Feb 12 2021 at 21:04):

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

#### Kevin Buzzard (Feb 12 2021 at 21:04):

And which universes will everything be in?

#### Kevin Buzzard (Feb 12 2021 at 21:05):

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

#### 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.

#### Jakob Scholbach (Feb 12 2021 at 21:07):

Or is that problematic?

#### Johan Commelin (Feb 12 2021 at 21:09):

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

#### Jakob Scholbach (Feb 12 2021 at 21:10):

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

#### Johan Commelin (Feb 12 2021 at 21:11):

Of course $\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.

#### Johan Commelin (Feb 12 2021 at 21:12):

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

#### 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

#### 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!

#### 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


#### 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 \colon M_1 \to M_2$ and another module $M$, the induced map $M_1 \otimes M \to M_2 \otimes M$.
But I don't know if that code ended up in mathlib.

#### 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

#### Eric Wieser (Feb 12 2021 at 21:40):

Is that docs#linear_map.prod_map?

#### Eric Wieser (Feb 12 2021 at 22:04):

Ah, tmul not prod

#### 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 :)

#### 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

#### 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.

#### 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 $I$, the natural map $I \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 $R$-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".

#### 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