Ryan Lahfa (Feb 04 2021 at 14:37):
I'm trying to define a Banach ring in Lean, which is a complete normed ring.
For this, I wanted to define a structure, so I defined:
import analysis.normed_space.basic variables (R: Type*) structure banach_ring extends normed_ring R, complete_space R
I have multiple questions:
(a) Is it a good idea?
(b) As I understand now, I will have to
to_xxx to get the underlying structure that I want in my definitions, should I re-inline the most important facts in the structure definition?
(c) I want to define the notion of Banach A-algebra afterward which is a Banach algebra B with a bounded morphism A → B, am I following a proper path to achieve this?
(My motivation is to define the set of all bounded real "semivaluations" over A of a Banach ring A, i.e. the spectrum of Berkovich.)
Ryan Lahfa (Feb 04 2021 at 14:49):
Or maybe I should do something like this:
import analysis.normed_space.basic variables (R: Type*) [normed_ring R] structure banach_ring extends complete_space R
Johan Commelin (Feb 04 2021 at 14:57):
I would first develop a bunch of stuff where you just assume
[normed_ring R] [complete_space R]. For a Banach algebra, it makes sense to make a new defn, since you need the boundedness assumption on the algebra map.
Ryan Lahfa (Feb 04 2021 at 14:59):
Alright, thank you for the advice!
Last updated: May 13 2021 at 18:26 UTC