feat(ring_theory/algebra_operations): multiplication of submodules of an algebra #658
Conversation
| protected theorem mul_comm : M * N = N * M := | ||
| le_antisymm (mul_le.2 $ λ r hrm s hsn, mul_mem_mul_rev hsn hrm) | ||
| (mul_le.2 $ λ r hrn s hsm, mul_mem_mul_rev hsm hrn) | ||
|
|
There was a problem hiding this comment.
Is there a problem making a comm_semigroup instance here?
|
|
||
| theorem mul_bot : M * ⊥ = ⊥ := | ||
| eq_bot_iff.2 $ mul_le.2 $ λ m hm n hn, by rw [submodule.mem_bot] at hn ⊢; rw [hn, mul_zero] | ||
|
|
There was a problem hiding this comment.
This and bot_mul should be simp
| (h0 : C 0) (ha : ∀ x y, C x → C y → C (x + y)) | ||
| (hs : ∀ (r : R) x, C x → C (r • x)) : C r := | ||
| (@mul_le _ _ _ _ _ _ _ ⟨C, h0, ha, hs⟩).2 hm hr | ||
|
|
There was a problem hiding this comment.
The arguments sometimes have to be in a particular order for it to work with induction ... using mul_induction, although I'm not sure what the correct order is. Instinctively, r should come just after C.
There was a problem hiding this comment.
The error message says "invalid user defined recursor, type of the major premise 'r' must be for the form (I ...), where I is a constant" so I don't think this solves the problem.
There was a problem hiding this comment.
The naming convention has induction or rec with the variable r at the end, and induction_on or rec_on with r just after C.
There was a problem hiding this comment.
just like span_induction?
There was a problem hiding this comment.
or finsupp.induction?
|
|
||
| theorem mul_mono (hmp : M ≤ P) (hnq : N ≤ Q) : M * N ≤ P * Q := | ||
| mul_le.2 $ λ m hm n hn, mul_mem_mul (hmp hm) (hnq hn) | ||
|
|
There was a problem hiding this comment.
My taste would be for mul_le_mul_of_le_of_le here.
There was a problem hiding this comment.
changed to mul_le_mul per add_le_add
There was a problem hiding this comment.
Can we label this with @[mono]?
kckennylau
force-pushed
the
submodule-mul
branch
from
9a5589d
to
a3ed643
Compare
| zero := ⊥, | ||
| zero_add := λ _, bot_sup_eq, | ||
| add_zero := λ _, sup_bot_eq, | ||
| add_comm := λ _ _, sup_comm } |
There was a problem hiding this comment.
This doesn't have anything to do with algebras. It should go in linear_algebra.basic (along with add_eq_sup and zero_eq_bot below)
kckennylau
force-pushed
the
submodule-mul
branch
from
a3ed643
to
bc68225
Compare
| @@ -0,0 +1,132 @@ | |||
| import ring_theory.algebra ring_theory.noetherian | |||
kckennylau
force-pushed
the
submodule-mul
branch
from
bc68225
to
6764f02
Compare
kckennylau
force-pushed
the
submodule-mul
branch
from
6764f02
to
bef7e6b
Compare
TO CONTRIBUTORS:
Make sure you have:
If this PR is related to a discussion on Zulip, please include a link in the discussion.
For reviewers: code review check list