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
+12 −0
Open

feat: add ContinuousSMul instances for ℚ≥0 #28474

Changes from 2 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
14 changes: 14 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,7 @@ Copyright (c) 2017 Johannes Hölzl. All rights reserved.
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.Order
import Mathlib.Topology.Algebra.Order.Archimedean
import Mathlib.Topology.Algebra.Ring.Real
Expand Down Expand Up @@ -123,4 +124,17 @@ instance : ContinuousSub ℚ≥0 :=
instance : OrderTopology ℚ≥0 := orderTopology_of_ordConnected (t := Set.Ici 0)
instance : HasContinuousInv₀ ℚ≥0 := inferInstance

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

instance {R} [Ring R] [TopologicalSpace R] [Algebra ℚ R] [Algebra ℚ≥0 R] [ContinuousSMul ℚ R] :
Copy link
Collaborator

@themathqueen themathqueen Aug 15, 2025 •
edited
Loading

Choose a reason for hiding this comment

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

Is the Algebra ℚ≥0 R hypothesis necessary? Why not show it within the proof for continuous_smul?

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

The argument of ContinuousSMul ℚ≥0 R needs Algebra ℚ≥0 R. Obtaining it from Algebra ℚ R will cause a diamond.

Copy link
Collaborator

Choose a reason for hiding this comment

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

ah, fair enough

Copy link
Contributor

@ocfnash ocfnash Aug 29, 2025 •
edited
Loading

Choose a reason for hiding this comment

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

I don't agree with the claim about the diamond (in fact I claim the opposite!) but it doesn't matter since I have another suggestion.

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

I think the diamond already exists. Zulip

ContinuousSMul ℚ≥0 R where
continuous_smul := by
convert continuous_induced_dom.fst'.smul (M := ℚ) (X := R) continuous_snd using 2
rw [← cast_smul_eq_nnqsmul ℚ]
rfl
Copy link
Contributor

Choose a reason for hiding this comment

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

Note that via NNRat.instDistribMulActionOfRat we already have an action of ℚ≥0 on R so there is no need to include a typeclass carrying this. Also the Algebra assumption is more than we need and can be weakened to just DistribMulAction. Here is what I suggest:

Suggested change
instance {R} [Ring R] [TopologicalSpace R] [Algebra ℚ R] [Algebra ℚ≥0 R] [ContinuousSMul ℚ R] :
ContinuousSMul ℚ≥0 R where
continuous_smul := by
convert continuous_induced_dom.fst'.smul (M := ℚ) (X := R) continuous_snd using 2
rw [← cast_smul_eq_nnqsmul ℚ]
rfl
instance {R : Type*} [Ring R] [DistribMulAction ℚ R] [TopologicalSpace R] [ContinuousSMul ℚ R] :
ContinuousSMul ℚ≥0 R where
continuous_smul := continuous_induced_dom.fst'.smul continuous_snd


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

end NNRat