feat(algebra/category/RingModPair): definition of the category of pairs of ring and module #10724
Conversation
bryangingechen
changed the title
semorrison
added
the
awaiting-review
|
I think Perhaps |
semorrison
added
awaiting-author
jjaassoonn
added
awaiting-review
jjaassoonn
changed the title
There was a problem hiding this comment.
Not sure if you still plan to get this merged. I wonder if you need CommRingMod instead?
@alreadydone Is there a general way to formalize grothendieck construction in mathlib now?
| -/ | ||
| def hom (P Q : RingModPair) : Type (max v u) := | ||
| Σ (ring_hom : P.ring ⟶ Q.ring), | ||
| P.mod ⟶ (category_theory.Module.restrict_scalars ring_hom).obj Q.mod |
There was a problem hiding this comment.
I wonder if you should use semilinear maps instead. This at least avoids the need to define id and comp by hand below.
| id := λ P, sigma.mk (𝟙 _) | ||
| { to_fun := λ x, x, | ||
| map_add' := λ _ _, rfl, | ||
| map_smul' := λ _ _, rfl }, | ||
| comp := λ X Y Z f g, sigma.mk (f.1 ≫ g.1) | ||
| { to_fun := λ x, g.2 $ f.2 x, | ||
| map_add' := λ x y, by simp only [map_add], | ||
| map_smul' := λ r x, | ||
| by simp only [map_smul, ring_hom.id_apply, restrict_scalars.smul_def, comp_apply] }, |
There was a problem hiding this comment.
There should be simp lemmas concerning the application of such morphisms to actual elements.
| -/ | ||
| def hom.mod_hom {P Q : RingModPair} (f : P ⟶ Q) : | ||
| P.mod ⟶ (category_theory.Module.restrict_scalars f.ring_hom).obj Q.mod := f.2 | ||
|
|
There was a problem hiding this comment.
There should be a constructor to construct arrows from a ring hom and a linear map.
| map_comp' := λ _ _ _ _ _, rfl } | ||
|
|
||
| /-- | ||
| The canonical functor sending a ring-module pair to its underlying abelian group |
There was a problem hiding this comment.
| The canonical functor sending a ring-module pair to its underlying abelian group | |
| The canonical functor sending a ring-module pair to the underlying abelian group of the module. |
Both the ring and the module has an underlying abelian group. It doesn't hurt to be clearer.
erdOne
added
awaiting-author
It's possible to use category_theory.grothendieck because R ↦ Module R is a strict functor from (Comm)Ring to Cat. (I think it's also possible to define PresheafedSpace using this strict Grothendieck construction) The generalization to oplax functors is in this branch but not yet PR'd. |
I defined the category of modules following this link.
This may or may not be useful to define sheaf of modules.