Zulip Chat Archive
Stream: triage
Topic: issue #4033: properties of (sub)modules
Random Issue Bot (Nov 21 2020 at 14:18):
Today I chose issue 4033 for discussion!
properties of (sub)modules
Created by @Johan Commelin (@jcommelin) on 2020-09-03
Labels: feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Apr 12 2021 at 14:24):
Today I chose issue 4033 for discussion!
properties of (sub)modules
Created by @Johan Commelin (@jcommelin) on 2020-09-03
Labels: feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Kevin Buzzard (Apr 12 2021 at 14:46):
flat modules are in ring_theory.flat and projective modules are PR'ed in #6813 (which I just put back on the queue today).
Random Issue Bot (Dec 31 2021 at 14:17):
Today I chose issue 4033 for discussion!
properties of (sub)modules
Created by @Johan Commelin (@jcommelin) on 2020-09-03
Labels: feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Mar 08 2022 at 14:13):
Today I chose issue 4033 for discussion!
properties of (sub)modules
Created by @Johan Commelin (@jcommelin) on 2020-09-03
Labels: feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Kevin Buzzard (Mar 08 2022 at 15:40):
@Jujian Zhang what is the status of injective modules?
Jujian Zhang (Mar 08 2022 at 16:55):
Non-existent what so ever. We can say what is an injective object in the category of modules; but we don't have something like the following:
class module.projective (R : Type u) [semiring R] (P : Type (max u v)) [add_comm_monoid P]
[module R P] : Prop :=
(out : ∃ s : P →ₗ[R] (P →₀ R), function.left_inverse (finsupp.total P P R id) s)
not to mention that a module is an injective module iff it is an injective object
Jujian Zhang (Mar 08 2022 at 16:58):
I will try writing a file similar to algebra/module/injective.lean
Jujian Zhang (Mar 23 2022 at 08:47):
There is a definition of injective module and a proof of Baer's criterion sitting at #12895.
Kevin Buzzard (Mar 23 2022 at 10:18):
Nice!
Random Issue Bot (Jun 25 2022 at 14:19):
Today I chose issue 4033 for discussion!
properties of (sub)modules
Created by @Johan Commelin (@jcommelin) on 2020-09-03
Labels: feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Sep 17 2022 at 14:14):
Today I chose issue 4033 for discussion!
properties of (sub)modules
Created by @Johan Commelin (@jcommelin) on 2020-09-03
Labels: feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Johan Commelin (Sep 17 2022 at 14:33):
The only remaining item on the list is "finitely presentable". We have this for algebras (and hence ring homs), but not yet for modules. Anyone interested in writing a small API to close this issue?
Andrew Yang (Sep 17 2022 at 15:12):
I had plans on developing some results regarding finitely presentable modules, but I won't have time until next month.
Random Issue Bot (Oct 11 2022 at 14:34):
Today I chose issue 4033 for discussion!
properties of (sub)modules
Created by @Johan Commelin (@jcommelin) on 2020-09-03
Labels: feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Oct 19 2022 at 14:36):
Today I chose issue 4033 for discussion!
properties of (sub)modules
Created by @Johan Commelin (@jcommelin) on 2020-09-03
Labels: feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Oct 31 2022 at 14:29):
Today I chose issue 4033 for discussion!
properties of (sub)modules
Created by @Johan Commelin (@jcommelin) on 2020-09-03
Labels: feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Nov 12 2022 at 14:07):
Today I chose issue 4033 for discussion!
properties of (sub)modules
Created by @Johan Commelin (@jcommelin) on 2020-09-03
Labels: feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Dec 23 2022 at 14:09):
Today I chose issue 4033 for discussion!
properties of (sub)modules
Created by @Johan Commelin (@jcommelin) on 2020-09-03
Labels: feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Feb 19 2023 at 14:08):
Today I chose issue 4033 for discussion!
properties of (sub)modules
Created by @Johan Commelin (@jcommelin) on 2020-09-03
Labels: feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Aug 12 2023 at 14:07):
Today I chose issue 4033 for discussion!
properties of (sub)modules
Created by @Johan Commelin (@jcommelin) on 2020-09-03
Labels: feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Last updated: Dec 20 2023 at 11:08 UTC