mathlib icon indicating copy to clipboard operation
mathlib copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat(topology/continuous_function/ideals): maximal ideals correspond to (complements of) singletons

Open j-loreaux opened this issue 3 years ago • 2 comments

This establishes the correspondence between maximal ideals of C(X, 𝕜) (where X is compact Hausdorff and is_R_or_C 𝕜) and the complements of singletons in X. This allows for the proof that the natural map from X to character_space 𝕜 C(X, 𝕜) is a homeomorphism.

  • [x] depends on: #16709
  • [x] depends on: #16713
  • [x] depends on: #16714
  • [x] depends on: #16677
  • [x] depends on: #16663
  • [x] depends on: #16721
  • [x] depends on: #16722
  • [x] depends on: #16801

Open in Gitpod

j-loreaux avatar Sep 30 '22 03:09 j-loreaux

Just a heads up that #16860 is introducing a maximal_spectrum definition.

alreadydone avatar Oct 08 '22 04:10 alreadydone

This PR/issue depends on:

  • ~~leanprover-community/mathlib#16709~~
  • ~~leanprover-community/mathlib#16713~~
  • ~~leanprover-community/mathlib#16714~~
  • ~~leanprover-community/mathlib#16677~~
  • ~~leanprover-community/mathlib#16663~~
  • ~~leanprover-community/mathlib#16721~~
  • ~~leanprover-community/mathlib#16722~~
  • ~~leanprover-community/mathlib#16801~~ By Dependent Issues (🤖). Happy coding!

mathlib-dependent-issues-bot avatar Oct 12 '22 07:10 mathlib-dependent-issues-bot

Thanks!

bors merge

ocfnash avatar Oct 24 '22 18:10 ocfnash

Pull request successfully merged into master.

Build succeeded:

bors[bot] avatar Oct 24 '22 21:10 bors[bot]