generalize to Monoid+MulAction#1
Conversation
alreadydone
commented
Aug 13, 2025
alreadydone
commented
Vierkantor
left a comment
Vierkantor
left a comment
There was a problem hiding this comment.
@alreadydone, @xroblot, do you agree with my suggestions?
@xroblot When you merge these, I'll get your original PR merged!
| @@ -516,6 +515,16 @@ lemma SMulCommClass.of_mul_smul_one {M N} [Monoid N] [SMul M N] | |||
| (H : ∀ (x : M) (y : N), y * x • (1 : N) = x • y) : SMulCommClass M N N := | |||
| ⟨fun x y z ↦ by rw [← H x z, smul_eq_mul, ← H, smul_eq_mul, mul_assoc]⟩ | |||
|
|
|||
There was a problem hiding this comment.
| /-- | |
| Let `Q / P / N / M` be a scalar tower. If `P / N / M`, `Q / P / M` and `Q / P / N` are | |
| scalar towers, then `Q / N / M` is also a scalar tower. | |
| -/ |
| [SMul M N] [SMul M P] [SMul M Q] [SMul N P] [SMul N Q] [Monoid P] [MulAction P Q] | ||
| [IsScalarTower M N P] [IsScalarTower M P Q] [IsScalarTower N P Q] : IsScalarTower M N Q where | ||
| smul_assoc m n q := by rw [← smul_one_smul P, smul_assoc m, smul_assoc, smul_one_smul] | ||
|
|
There was a problem hiding this comment.
| /-- | |
| Let `Q / P / N / M` be a scalar tower. If `P / N / M`, `Q / N / M` and `Q / P / N` are | |
| scalar towers, then `Q / P / M` is also a scalar tower. | |
| -/ |
| (H : ∀ (x : M) (y : N), y * x • (1 : N) = x • y) : SMulCommClass M N N := | ||
| ⟨fun x y z ↦ by rw [← H x z, smul_eq_mul, ← H, smul_eq_mul, mul_assoc]⟩ | ||
|
|
||
| @[to_additive] lemma IsScalarTower.trans_left (M N P Q) |
There was a problem hiding this comment.
Not sure about left/right, since the metaphor of towers is more vertical. Maybe we can call Q / P / N / M in that order highest / higher / lower / lowest?
| @[to_additive] lemma IsScalarTower.trans_left (M N P Q) | |
| @[to_additive] lemma IsScalarTower.to_lower (M N P Q) |
| [IsScalarTower M N P] [IsScalarTower M P Q] [IsScalarTower N P Q] : IsScalarTower M N Q where | ||
| smul_assoc m n q := by rw [← smul_one_smul P, smul_assoc m, smul_assoc, smul_one_smul] | ||
|
|
||
| @[to_additive] lemma IsScalarTower.trans_right (M N P Q) |
There was a problem hiding this comment.
| @[to_additive] lemma IsScalarTower.trans_right (M N P Q) | |
| @[to_additive] lemma IsScalarTower.to_higher (M N P Q) |
There was a problem hiding this comment.
I have a 123 version too:
theorem IsScalarTower.to₁₂₃ (M N P Q)
[SMul M N] [SMul M P] [SMul M Q] [SMul N P] [SMul N Q] [SMul P Q] [FaithfulSMul P Q]
[IsScalarTower M N Q] [IsScalarTower M P Q] [IsScalarTower N P Q] : IsScalarTower M N P where
smul_assoc m n p := by simp_rw [← (smul_left_injective' (α := Q)).eq_iff, smul_assoc]
This basically require 34 to be an injective map.
The 234 version would need cancelling 12 from the right side of an equality between compositions, so it basically requires 12 to be a surjective map, but I don't know of a readily available typeclass to impose that.
There was a problem hiding this comment.
theorem IsScalarTower.to₂₃₄ (M N P Q)
[SMul M N] [SMul M P] [SMul M Q] [SMul P Q] [Monoid N] [MulAction N P] [MulAction N Q]
[IsScalarTower M N P] [IsScalarTower M N Q] [IsScalarTower M P Q]
(h : Function.Surjective fun m : M ↦ m • (1 : N)) : IsScalarTower N P Q where
smul_assoc n p q := by obtain ⟨m, rfl⟩ := h n; simp_rw [smul_one_smul, smul_assoc]
has the same assumptions as 134 except for the surjectivity.
|
I am a bit confused here. Should I just merge the current version and then apply the suggestions of @Vierkantor and should I wait for @alreadydone to apply the suggestions and then merge the resulting version? |
|
Sorry for the confusion! I would like to see the suggestions by @alreadydone and my suggestions merged into leanprover-community#27866, and then I'll approve that PR. |
|
Ok, so I'll merge this PR into leanprover-community#27866 and then apply your changes there since I don't think I can modify this PR directly. |
|
Sounds good to me! |
|
Indeed it's my responsibility to act on reviews on my PR, but I got confused. Thanks for merging and addressing the reviews! |
3 participants
