Skip to content

[Merged by Bors] - refactor: rename UniqueContinuousFunctionalCalculus to ContinuousMap.UniqueHom#20643

Closed
j-loreaux wants to merge 5 commits intomasterfrom
j-loreaux/rename-UniqueCFC
Closed

[Merged by Bors] - refactor: rename UniqueContinuousFunctionalCalculus to ContinuousMap.UniqueHom#20643
j-loreaux wants to merge 5 commits intomasterfrom
j-loreaux/rename-UniqueCFC

Conversation

@j-loreaux
Copy link
Copy Markdown
Contributor

@j-loreaux j-loreaux commented Jan 10, 2025

Given that UniqueContinuousFunctionalCalculus no longer mentions spectrum, it really has very little to tie it to the ContinuousFunctionalCalculus. In some sense, it's just a property of C(s, R), but because we want to allow R := ℝ≥0, the algebra A also matters. Because of this, we put the class within the ContinuousMap namespace.

We also rename UniqueNonUnitalContinuousFunctionalCalculus to ContinuousMapZero.UniqueHom.

Open in Gitpod

@j-loreaux j-loreaux added the t-analysis Analysis (normed *, calculus) label Jan 10, 2025
@github-actions
Copy link
Copy Markdown

github-actions bot commented Jan 10, 2025 •
edited
Loading

PR summary 18007365ee

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ Complex.instContinuousMapUniqueHom
+ ContinuousMap.UniqueHom
+ ContinuousMapZero.UniqueHom
+ NNReal.instContinuousMap.UniqueHom
+ NNReal.instContinuousMapZero.UniqueHom
+ Real.instContinuousMapUniqueHom
+ instance (priority := 100) RCLike.instContinuousMapUniqueHom [TopologicalSpace A]
- Complex.uniqueContinuousFunctionalCalculus
- NNReal.instUniqueContinuousFunctionalCalculus
- NNReal.instUniqueNonUnitalContinuousFunctionalCalculus
- Real.uniqueContinuousFunctionalCalculus
- instance (priority := 100) RCLike.uniqueContinuousFunctionalCalculus [TopologicalSpace A]

You can run this locally as follows 
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

@j-loreaux j-loreaux requested a review from dupuisf January 10, 2025 19:59
@dupuisf
Copy link
Copy Markdown
Contributor

dupuisf commented Jan 14, 2025

I'm not sure I like this rename: the typeclass is more about a property of the algebra A than of the continuous maps, at least that's certainly how we think of it in the context of the CFC. Would it even have any applications at all outside of this context?

@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jan 14, 2025
@j-loreaux
Copy link
Copy Markdown
Contributor Author

j-loreaux commented Jan 14, 2025

  1. I'm certainly open to other name suggestions
  2. I would argue it's (almost) entirely about continuous maps. For R := 𝕜 with RCLike 𝕜, this is a direct consequence of Stone--Weierstrass. You need to know almost nothing about A except that it's a topological 𝕜-algebra. For R := ℝ≥0, you do technically need A (which is why this class exists at all), but only that it's a topological ℝ-algebra so that subtraction in the algebra makes sense.
  3. As for applications outside this context, I don't know of any at the moment, which is why I didn't move the definition of this class outside the CFC files, but I think it's certainly possible. Again, all you need is a star homomorphism from continuous maps to a topological 𝕜-algebra.

@j-loreaux j-loreaux removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jan 14, 2025
@dupuisf
Copy link
Copy Markdown
Contributor

dupuisf commented Jan 17, 2025

Fair enough, it's not like I have a better name to suggest anyway.

bors r+

@ghost ghost added the ready-to-merge This PR has been sent to bors. label Jan 17, 2025
mathlib-bors bot pushed a commit that referenced this pull request Jan 17, 2025
@j-loreaux
refactor: rename UniqueContinuousFunctionalCalculus to `ContinuousM…
a76d7c9 
…ap.UniqueHom` (#20643)

Given that `UniqueContinuousFunctionalCalculus` no longer mentions `spectrum`, it really has very little to tie it to the ContinuousFunctionalCalculus. In some sense, it's just a property of `C(s, R)`, but because we want to allow `R := ℝ≥0`, the algebra `A` also matters. Because of this, we put the class within the `ContinuousMap` namespace.

We also rename `UniqueNonUnitalContinuousFunctionalCalculus` to `ContinuousMapZero.UniqueHom`.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jan 17, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title refactor: rename UniqueContinuousFunctionalCalculus to ContinuousMap.UniqueHom [Merged by Bors] - refactor: rename UniqueContinuousFunctionalCalculus to ContinuousMap.UniqueHom Jan 17, 2025
@mathlib-bors mathlib-bors bot closed this Jan 17, 2025
@mathlib-bors mathlib-bors bot deleted the j-loreaux/rename-UniqueCFC branch January 17, 2025 03:59
Julian added a commit that referenced this pull request Jan 20, 2025
@Julian
Merge branch 'polynomial-sequences' into bhargava-factorial
856ec0d 
* polynomial-sequences: (149 commits)
  Aha, here's how to get Lean to stop showing S.elems' in the infoview.
  Try satisfying the linter gods again.
  Probably enough initial tidying to send the PR.
  Kill more temporary names.
  Touch more natDegree.
  Does protected satisfy the docstring linter?
  Bit shorter.
  More
  Quiet linters.
  Remove redundant imports.
  Copyright header and more twiddling.
  Rename lemma to 'degree_smul_of_leadingCoeff_rightRegular' and split out
  feat(Polynomial): polynomial sequences are bases for R[X]
  chore(Dynamics/PeriodicPts): don't import `MonoidWithZero` (#20765)
  chore(Associated): split out `Ring` results (#20737)
  feat(AlgebraicGeometry): flat morphisms of schemes (#19790)
  feat(AlgebraicGeometry): scheme-theoretic fibre (#19427)
  chore: split Mathlib.Analysis.Asymptotics.Asymptotics (#20785)
  doc: typo (#20829)
  feat(CategoryTheory): condition for an induced functor between comma categories to be final  (#20139)
  feat(1000.yaml): allow statements of theorems also (#20637)
  feat(Algebra/Homology/Embedding): homology of truncGE' (#19570)
  chore: cleanup many porting notes in Combinatorics (#20823)
  chore: eliminate porting notes about `deriving Fintype` (#20820)
  feat(Algebra/Lie): a Lie algebra is solvable iff it is solvable after faithfully flat base change (#20808)
  feat: define bases of root pairings (#20667)
  feat(Tactic): basic ConcreteCategory support for elementwise (#20811)
  feat(CategoryTheory): define unbundled `ConcreteCategory` class  (#20810)
  chore(CategoryTheory): rename `ConcreteCategory` to `HasForget` (#20809)
  feat: `CommSemiring (NonemptyInterval ℚ≥0)` (#20783)
  chore(yaml_check.py): re-format (#20807)
  feat: elementary estimate for Real.log (#20766)
  feat: definition of linear topologies (#14990)
  feat(RingTheory): flatness over a semiring (#19115)
  feat(Algebra/Homology/Embedding): the canonical truncation truncLE (#19550)
  feat(Algebra/Homology/Embedding): API for the homology of an extension of homological complex (#19203)
  feat(Algebra/Ring): `RingEquiv.piUnique` (#20794)
  feat(RingTheory/LocalRing): add instance `Unique (MaximalSpectrum R)` for a local ring `R` (#20801)
  chore(GroupExtension/Defs): define `Section` and redefine `Splitting` (#20802)
  chore: restore `def` to `adicCompletion` (#20796)
  refactor: rename `UniqueContinuousFunctionalCalculus` to `ContinuousMap.UniqueHom` (#20643)
  feat(Algebra/Homology/Embedding): the morphism from a complex to its `truncGE` truncation (#19544)
  chore(Mathlib/Computability/TuringMachine): split file (#20790)
  feat(Data/Finset/Card): add `InjOn` and `SurjOn` versions of finset cardinality lemmas (#20753)
  feat(Order/WellFoundedSet): add convenience constructors for IsWF and IsPWO for WellFoundedLT types (#20752)
  feat(Set/Finite): a set is finite if its image and fibers are finite (#20751)
  chore: cleanup .gitignore files (#20795)
  feat(Topology/Group/Profinite):  Profinite group is limit of finite group (#16992)
  feat(Combinatorics/SimpleGraph): vertices in cycles (#20602)
  CI: merge `bot_fix_style` actions (#20789)
  ...
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@dupuisf dupuisf Awaiting requested review from dupuisf

Assignees

No one assigned

Labels

ready-to-merge This PR has been sent to bors. t-analysis Analysis (normed *, calculus)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@j-loreaux @dupuisf @leanprover-community-bot-assistant