Fill in v_adicCompletionComapAlgHom
#245
Conversation
| @@ -63,8 +63,6 @@ def comap (w : HeightOneSpectrum B) : HeightOneSpectrum A where | |||
| isPrime := Ideal.comap_isPrime (algebraMap A B) w.asIdeal | |||
| ne_bot := mt Ideal.eq_bot_of_comap_eq_bot w.ne_bot | |||
|
|
|||
| open scoped algebraMap | |||
There was a problem hiding this comment.
I feel like this only causes trouble (e.g. the show (r : adicCompletion K (comap A w)) = @UniformSpace.Completion.coe' K this r from rfl below) and we don't really use it anyway.
|
|
||
| -- this name is surely wrong | ||
| open WithZeroTopology in | ||
| lemma v_adicCompletionComapAlgHom |
There was a problem hiding this comment.
This is the right name according to the naming convention.
We could probably rename adicCompletionComapAlgHom to adicCompletionComap.
There was a problem hiding this comment.
I am totally confused by your comment. How can w(x)=v(x)^e be called v_adicCompletionComapAlgHom? Where's the AlgHom in the statement?
There was a problem hiding this comment.
Your statement does not typecheck because
So the statement is adicCompletionComap
|
Thanks! |
No description provided.