Skip to content

[Merged by Bors] - chore: remove MulAction ℚ α → MulAction ℚ≥0 α instances #30671

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
astrainfinita wants to merge 5 commits into from
Closed

[Merged by Bors] - chore: remove MulAction ℚ α → MulAction ℚ≥0 α instances #30671

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
a05c783
chore: remove `MulAction ℚ α → MulAction ℚ≥0 α` instances
astrainfinita Oct 19, 2025
efbc0b2
more
astrainfinita Oct 19, 2025
308ffc5
shake
astrainfinita Oct 20, 2025
d47fa93
replace existing lemmas
astrainfinita Oct 20, 2025
069f8bd
fix
astrainfinita Oct 20, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
42 changes: 2 additions & 40 deletions Mathlib/Algebra/Algebra/Rat.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Kenny Lau, Yury Kudryashov
-/
import Mathlib.Algebra.Algebra.Defs
import Mathlib.Algebra.GroupWithZero.Action.Basic
import Mathlib.Algebra.Module.Equiv.Defs
import Mathlib.Data.Rat.Cast.CharZero

Expand All @@ -28,24 +27,7 @@ theorem map_rat_algebraMap [Semiring R] [Semiring S] [Algebra ℚ R] [Algebra
end RingHom

namespace NNRat
variable [DivisionSemiring R] [CharZero R]

section Semiring
variable [Semiring S] [Module ℚ≥0 S]

variable (R) in
/-- `nnqsmul` is equal to any other module structure via a cast. -/
lemma cast_smul_eq_nnqsmul [Module R S] (q : ℚ≥0) (a : S) : (q : R) • a = q • a := by
refine MulAction.injective₀ (G₀ := ℚ≥0) (Nat.cast_ne_zero.2 q.den_pos.ne') ?_
dsimp
rw [← mul_smul, den_mul_eq_num, Nat.cast_smul_eq_nsmul, Nat.cast_smul_eq_nsmul, ← smul_assoc,
nsmul_eq_mul q.den, ← cast_natCast, ← cast_mul, den_mul_eq_num, cast_natCast,
Nat.cast_smul_eq_nsmul]

end Semiring

section DivisionSemiring
variable [DivisionSemiring S] [CharZero S]
variable [DivisionSemiring R] [CharZero R] [DivisionSemiring S] [CharZero S]

instance _root_.DivisionSemiring.toNNRatAlgebra : Algebra ℚ≥0 R where
smul_def' := smul_def
Expand All @@ -64,28 +46,10 @@ instance instSMulCommClass [SMulCommClass R S S] : SMulCommClass ℚ≥0 R S whe
instance instSMulCommClass' [SMulCommClass S R S] : SMulCommClass R ℚ≥0 S :=
have := SMulCommClass.symm S R S; SMulCommClass.symm _ _ _

end DivisionSemiring
end NNRat

namespace Rat
variable [DivisionRing R] [CharZero R]

section Ring
variable [Ring S] [Module ℚ S]

variable (R) in
/-- `qsmul` is equal to any other module structure via a cast. -/
lemma cast_smul_eq_qsmul [Module R S] (q : ℚ) (a : S) : (q : R) • a = q • a := by
refine MulAction.injective₀ (G₀ := ℚ) (Nat.cast_ne_zero.2 q.den_pos.ne') ?_
dsimp
rw [← mul_smul, den_mul_eq_num, Nat.cast_smul_eq_nsmul, Int.cast_smul_eq_zsmul, ← smul_assoc,
nsmul_eq_mul q.den, ← cast_natCast, ← cast_mul, den_mul_eq_num, cast_intCast,
Int.cast_smul_eq_zsmul]

end Ring

section DivisionRing
variable [DivisionRing S] [CharZero S]
variable [DivisionRing R] [CharZero R] [DivisionRing S] [CharZero S]

instance _root_.DivisionRing.toRatAlgebra : Algebra ℚ R where
smul_def' := smul_def
Expand All @@ -108,8 +72,6 @@ instance instSMulCommClass [SMulCommClass R S S] : SMulCommClass ℚ R S where
instance instSMulCommClass' [SMulCommClass S R S] : SMulCommClass R ℚ S :=
have := SMulCommClass.symm S R S; SMulCommClass.symm _ _ _

end DivisionRing

instance algebra_rat_subsingleton {R} [Semiring R] : Subsingleton (Algebra ℚ R) :=
⟨fun x y => Algebra.algebra_ext x y <| RingHom.congr_fun <| Subsingleton.elim _ _⟩

Expand Down
12 changes: 12 additions & 0 deletions Mathlib/Algebra/Module/Rat.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -71,6 +71,18 @@ instance IsScalarTower.rat {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [
[Module ℚ R] [Module ℚ M] : IsScalarTower ℚ R M where
smul_assoc r x y := map_rat_smul ((smulAddHom R M).flip y) r x

/-- `nnqsmul` is equal to any other module structure via a cast. -/
lemma NNRat.cast_smul_eq_nnqsmul (R : Type*) [DivisionSemiring R]
[MulAction R M] [MulAction ℚ≥0 M] [IsScalarTower ℚ≥0 R M]
(q : ℚ≥0) (x : M) : (q : R) • x = q • x := by
rw [← one_smul R x, ← smul_assoc, ← smul_assoc]; simp

/-- `qsmul` is equal to any other module structure via a cast. -/
lemma Rat.cast_smul_eq_qsmul (R : Type*) [DivisionRing R]
[MulAction R M] [MulAction ℚ M] [IsScalarTower ℚ R M]
(q : ℚ) (x : M) : (q : R) • x = q • x := by
rw [← one_smul R x, ← smul_assoc, ← smul_assoc]; simp

section
variable {α : Type u} {M : Type v}

Expand Down
16 changes: 11 additions & 5 deletions Mathlib/Algebra/Order/Module/Rat.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,8 +3,8 @@ Copyright (c) 2024 Yaël Dillies. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yaël Dillies
-/
import Mathlib.Algebra.Module.Rat
import Mathlib.Algebra.Order.Module.Basic
import Mathlib.Data.NNRat.Lemmas
import Mathlib.Data.Rat.Cast.Order

/-!
Expand All @@ -13,13 +13,19 @@ import Mathlib.Data.Rat.Cast.Order

variable {α : Type*}

instance PosSMulMono.nnrat_of_rat [Preorder α] [MulAction ℚ α] [PosSMulMono ℚ α] :
instance PosSMulMono.nnrat_of_rat [Preorder α] [MulAction ℚ α] [MulAction ℚ≥0 α]
[IsScalarTower ℚ≥0 ℚ α] [PosSMulMono ℚ α] :
PosSMulMono ℚ≥0 α where
smul_le_smul_of_nonneg_left _q hq _a₁ _a₂ ha := smul_le_smul_of_nonneg_left (α := ℚ) ha hq
smul_le_smul_of_nonneg_left _q hq _a₁ _a₂ ha := by
rw [← NNRat.cast_smul_eq_nnqsmul ℚ, ← NNRat.cast_smul_eq_nnqsmul ℚ]
exact smul_le_smul_of_nonneg_left (α := ℚ) ha hq

instance PosSMulStrictMono.nnrat_of_rat [Preorder α] [MulAction ℚ α] [PosSMulStrictMono ℚ α] :
instance PosSMulStrictMono.nnrat_of_rat [Preorder α] [MulAction ℚ≥0 α] [MulAction ℚ α]
[IsScalarTower ℚ≥0 ℚ α] [PosSMulStrictMono ℚ α] :
PosSMulStrictMono ℚ≥0 α where
smul_lt_smul_of_pos_left _q hq _a₁ _a₂ ha := smul_lt_smul_of_pos_left (α := ℚ) ha hq
smul_lt_smul_of_pos_left _q hq _a₁ _a₂ ha := by
rw [← NNRat.cast_smul_eq_nnqsmul ℚ, ← NNRat.cast_smul_eq_nnqsmul ℚ]
exact smul_lt_smul_of_pos_left (α := ℚ) ha hq

section LinearOrderedAddCommGroup
variable [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α]
Expand Down
9 changes: 0 additions & 9 deletions Mathlib/Data/NNRat/Lemmas.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,6 @@ Authors: Yaël Dillies, Bhavik Mehta
-/
import Mathlib.Algebra.Field.Rat
import Mathlib.Algebra.Group.Indicator
import Mathlib.Algebra.GroupWithZero.Action.End
import Mathlib.Algebra.Order.Field.Rat
import Mathlib.Data.Rat.Lemmas
import Mathlib.Tactic.Zify
Expand All @@ -23,14 +22,6 @@ open scoped NNRat
namespace NNRat
variable {α : Type*} {q : ℚ≥0}

/-- A `MulAction` over `ℚ` restricts to a `MulAction` over `ℚ≥0`. -/
instance [MulAction ℚ α] : MulAction ℚ≥0 α :=
MulAction.compHom α coeHom.toMonoidHom

/-- A `DistribMulAction` over `ℚ` restricts to a `DistribMulAction` over `ℚ≥0`. -/
instance [AddCommMonoid α] [DistribMulAction ℚ α] : DistribMulAction ℚ≥0 α :=
DistribMulAction.compHom α coeHom.toMonoidHom
Comment on lines -26 to -32
Copy link
Contributor

@ocfnash ocfnash Oct 22, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think we should keep these, just demoting them to defs, rather than deleting them altogether; they could be useful inside a proof (e.g., if someone has a ℚ action and wants to apply some lemma about a ℚ≥0 action).

Copy link
Collaborator Author

@astrainfinita astrainfinita Oct 22, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think these should be .restrictScalars lemmas rather than specialized lemmas.

Copy link
Contributor

@ocfnash ocfnash Oct 23, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Good point, I agree!

IIUC you have in mind generalisations such as:

def MulAction.restrictScalars (γ β α : Type*) [Monoid β] [Monoid γ] [MulAction γ β]
    [MulAction β α] [SMulCommClass γ β β] [IsScalarTower γ β β] : MulAction γ α where
 ...

Looking now I can't find these in Mathlib. If they really are missing, perhaps you'd be interested in adding them!


@[simp, norm_cast]
lemma coe_indicator (s : Set α) (f : α → ℚ≥0) (a : α) :
((s.indicator f a : ℚ≥0) : ℚ) = s.indicator (fun x ↦ ↑(f x)) a :=
Expand Down