namespaces, and more

Stream: new members

[Notification Bot]

Matej Penciak has marked this topic as unresolved.

[Matej Penciak]

Instead of creating a new thread I figured I'd contain all of my posts in here... I've been slogging away at Lean for a couple days now trying to learn as much as I can. I've gotten stuck in making any progress, but also have a couple lemmas that may be interesting (and that haven't been done as far as I can tell...)

I came into this hoping to make some progress in proving the equivalence of definitions for flat modules in docs#module.flat.

The first is that I define the subtype of finitely generated submodules and generate a couple instances that may be worthwhile for the proof (also a few helpful lemmas, but I'm coming to realize I haven't written enough)

import ring_theory.noetherian
universes u v

variables (R : Type u) (M : Type v) [ring R] [add_comm_group M] [module R M]

def fin_submodule : Type v := { N : submodule R M // N.fg }

instance : semilattice_sup (fin_submodule R M) :=  ...

instance : is_directed (fin_submodule R M) (≤) := ...

I also worked on direct limits a bit and proved something that says that if all the components of a map out of a direct limit are injective, then the map itself is injective.

import algebra.direct_limit

universes u v w

open function (injective)
open module.direct_limit

variables {R : Type u} [ring R] {ι : Type v} [decidable_eq ι] [preorder ι] [is_directed ι (≤)] [nonempty ι]
variables (G : ι → Type w) [Π i, add_comm_group (G i)] [Π i, module R (G i)]
variables (f : Π i j, i ≤ j → G i →ₗ[R] G j) [directed_system G (λ i j h, f i j h)]
variables {P : Type u} [add_comm_group P] [module R P] (h : Π i j, injective $ f i j)

def direct_limit_map_component (g : module.direct_limit G f →ₗ[R] P) : Π i, G i →ₗ[R] P := λi,
{ to_fun := g ∘ (of R ι G f i),
  map_add' := by simp, -- kind of slow
  map_smul' := by simp  -- kind of slow}
}

lemma injective_of_direct_limit (g : module.direct_limit G f →ₗ[R] P)
(h : Π i, injective (direct_limit_map_component G f g i)) : injective g := ...

I was hoping to continue on and prove that a module is linearly equivalent to the direct limit of its finitely generated submodules, but I'm running into a wall with how I've set things up. Does anyone have suggestions or resources for best practices in how to set these kinds of things up? I would hope to have everything in place so that the "obvious" parts (stuff like x : ↥N implies x ∈ N, or N : fin_submodule R M can easily generate a module R ↥N instance) are handled automatically.

[Johan Commelin]

@Matej Penciak Interesting project! What exactly is your question?
If by simp is kind of slow, try replacing it with the output of by squeeze_simp. (Pro tip: you can click on the output and it will auto-replace itself in the code. You can even hit Alt-V to do that.)

[Johan Commelin]

Are you working on the TODOs in the file on flatness?

[Matej Penciak]

Johan Commelin said:

Matej Penciak Interesting project! What exactly is your question?
If by simp is kind of slow, try replacing it with the output of by squeeze_simp. (Pro tip: you can click on the output and it will auto-replace itself in the code. You can even hit Alt-V to do that.)

So I guess my question was pretty vague in the original message, so something that has specifically come up is the following: From the work above I already have that fin_submodule R M as I've defined it is a directed system, so I would want to make a direct limit out of it with module.direct_limit. I'm having issues with defining an instance of Π (N P : fin_submodule R M), N ≤ P → (↥(N.val) →ₗ[R] ↥(P.val)) though. The naive way I've written it seems to have the right type, but I'm getting a somewhat cryptic error:

<thing> has type
  Π (N P : fin_submodule R M), N ≤ P → (↥(N.val) →ₗ[R] ↥(P.val))
but is expected to have type
  Π (i j : fin_submodule R M), i ≤ j → (↥(i.val) →ₗ[R] ↥(j.val))

Digging a little deeper, if I compare the two in infoview I have a slight mismatch in the two instances:

The thing I've constructed:
defn1.png

The thing I need:
defn2.png

I can try to generate a MWE, but I'm worried I might end up needing like half the file in order to reconstruct this issue...

[Matej Penciak]

Johan Commelin said:

Are you working on the TODOs in the file on flatness?

I'm trying! But I'd say so far I haven't gotten past the "administrative" part of the proof

[Eric Wieser]

I can try to generate a MWE, but I'm worried I might end up needing like half the file in order to reconstruct this issue...

Is this on a branch of mathlib? If so, you can share the link and we can diagnose in gitpod / by checking out locally

[Eric Wieser]

direct_limit_map_component looks like it's just docs#module.direct_limit.of composed with g (g ∘ₗ of R ι G f i), which means you don't even need those simps!

[Matej Penciak]

Eric Wieser said:

I can try to generate a MWE, but I'm worried I might end up needing like half the file in order to reconstruct this issue...

Is this on a branch of mathlib? If so, you can share the link and we can diagnose in gitpod / by checking out locally

I made a leanproject and keep it synced up between my home and office computers with this github repo https://github.com/mpenciak/flatstuff.
flatness.lean is where I wanted to have the main argument once I got to it, but the issues I'm running into are down at the bottom on line 292 of finite_submodules.lean

Just a heads up that the file is pretty rough in a lot of places (and I would very much appreciate suggestions on improvements)!

[Matej Penciak]

Eric Wieser said:

direct_limit_map_component looks like it's just docs#module.direct_limit.of composed with g (g ∘ₗ of R ι G f i), which means you don't even need those simps!

That it is! I knew there must have been a better way of writing a composition of linear maps

[Eric Wieser]

You don't usually want to use λ⟨x, hx⟩ in definitions, as it makes them not unfold nicely

[Eric Wieser]

Better to use λ x and then use x and x.prop later

[Eric Wieser]

(It's fine to use in map_add etc, but don't use it in to_fun)

[Eric Wieser]

https://github.com/mpenciak/flatstuff/pull/1

[Matej Penciak]

Eric Wieser said:

https://github.com/mpenciak/flatstuff/pull/1

Thank you! As I mentioned on the PR I learned a ton, back to work!

[Antoine Chambert-Loir]

A related thing that would be useful is having VSCode recall you all default variables / instances on the upper right of the screen.

[Notification Bot]

2 messages were moved from this topic to #Is there code for X? > tensor products commute with direct limits by Johan Commelin.