Skip to content

[Merged by Bors] - 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

Closed
astrainfinita wants to merge 15 commits into from
Closed

[Merged by Bors] - feat: add ContinuousSMul instances for ℚ≥0 #28474

Changes from 2 commits
Commits
Show all changes
15 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
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
d0f9960
Revert "suggestion"
astrainfinita Oct 20, 2025
069f8bd
fix
astrainfinita Oct 20, 2025
7fc7755
Update Rat.lean
astrainfinita Oct 20, 2025
2b220a7
Update Rat.lean
astrainfinita Oct 20, 2025
4dce365
Merge branch 'nnrat_action' into rat_continuousSMul
astrainfinita Oct 20, 2025
5eab839
Merge branch 'master' into rat_continuousSMul
astrainfinita Oct 23, 2025
bbc7a20
fix
astrainfinita Oct 23, 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

@astrainfinita astrainfinita Aug 15, 2025

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

@themathqueen themathqueen Aug 15, 2025

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

@astrainfinita astrainfinita Oct 19, 2025

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

@ocfnash ocfnash Aug 29, 2025

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