search

leanprover-community / lean-perfectoid-spaces

Perfectoid spaces in the Lean formal theorem prover.
https://leanprover-community.github.io/lean-perfectoid-spaces/
Apache License 2.0
115 stars 13 forks source link

Wrong category instance for CLVRS #35

Closed jcommelin closed 5 years ago

jcommelin commented 5 years ago

https://github.com/leanprover-community/lean-perfectoid-spaces/blob/93849977078e0dc24fe0ba57e0d1dc2876749411/src/adic_space.lean#L433

We currently take the full subcategory, but we should of course require local ring morphisms on the stalks. We don't need this instance, so we might as well just remove it.

jcommelin commented 5 years ago

Never mind... I guess I should sleep. The morphisms preserve valuations, so they automatically induce maps of local rings on stalks.