Skip to content

feat: add ContinuousSMul instances for ℚ≥0 #28474

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

Open
wants to merge 4 commits into
base: master
Choose a base branch
from
Open

feat: add ContinuousSMul instances for ℚ≥0 #28474

Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
e912a79
feat: add `ContinuousSMul` instances for `ℚ≥0`
astrainfinita Aug 15, 2025
f70ef66
suggestion
astrainfinita Aug 15, 2025
162b1ab
Merge branch 'master' into rat_continuousSMul
astrainfinita Oct 19, 2025
94eb313
suggestion
astrainfinita Oct 19, 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
12 changes: 12 additions & 0 deletions Mathlib/Topology/Instances/Rat.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,8 @@
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Johannes Hölzl, Mario Carneiro
-/
import Mathlib.Algebra.Algebra.Rat
import Mathlib.Data.NNRat.Lemmas
import Mathlib.Data.NNRat.Order
import Mathlib.Topology.Algebra.Order.Archimedean
import Mathlib.Topology.Algebra.Ring.Real
Expand Down Expand Up @@ -123,4 +125,14 @@
instance : OrderTopology ℚ≥0 := orderTopology_of_ordConnected (t := Set.Ici 0)
instance : ContinuousInv₀ ℚ≥0 := inferInstance

instance : ContinuousSMul ℚ ℝ where
continuous_smul := continuous_induced_dom.fst'.smul (M := ℝ) (X := ℝ) continuous_snd

instance {R : Type*} [Ring R] [MulAction ℚ R] [TopologicalSpace R] [ContinuousSMul ℚ R] :

Check failure on line 131 in Mathlib/Topology/Instances/Rat.lean

View workflow job for this annotation

GitHub Actions / Build (fork) 

@NNRat.instContinuousSMulOfRingOfRat argument 2 inst✝³ : Ring
ContinuousSMul ℚ≥0 R where
continuous_smul := continuous_induced_dom.fst'.smul continuous_snd
Comment on lines +131 to +133
Copy link
Contributor

Choose a reason for hiding this comment

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

Now that I realise NNRat.instMulActionOfRat is harmful, I realise that we should not author new lemmas about it (indeed we should excise it).

Thus your original design in which both the data of the ℚ≥0 and ℚ` actions were supplied was the right approach. Looking now I suppose we can generalise it slightly as follows:

Suggested change
instance {R : Type*} [Ring R] [MulAction ℚ R] [TopologicalSpace R] [ContinuousSMul ℚ R] :
ContinuousSMul ℚ≥0 R where
continuous_smul := continuous_induced_dom.fst'.smul continuous_snd
instance {R : Type*} [SMul ℚ≥0 R] [MulAction ℚ R] [IsScalarTower ℚ≥0 ℚ R]
[TopologicalSpace R] [ContinuousSMul ℚ R] :
ContinuousSMul ℚ≥0 R where
continuous_smul := by
convert continuous_induced_dom.fst'.smul (M := ℚ) (X := R) continuous_snd using 2 with
⟨⟨q, hq⟩, r⟩
conv_lhs => rw [← one_smul ℚ r, ← smul_assoc]
simp

(Note that for this to apply in the lemma below, we will need to add import Mathlib.Algebra.Module.Rat so that Lean can find IsScalarTower ℚ≥0 ℚ ℝ, and of course we should now drop import Mathlib.Data.NNRat.Lemmas.)

Apologies for the suggesting we use the bad instance.


instance : ContinuousSMul ℚ≥0 NNReal where
continuous_smul := Continuous.subtype_mk (by fun_prop) _

end NNRat
Loading