Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

refactor(perfectoid_space): beautification #34

Merged
merged 22 commits into from
May 3, 2019
Merged

refactor(perfectoid_space): beautification #34

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
22 commits
Select commit Hold shift + click to select a range
5a0c37e
WIP -- changing machines
jcommelin Apr 30, 2019
38560ab
Start on PreValuedRingedSpace, 2 sorries
jcommelin Apr 30, 2019
5d0db55
WIP
jcommelin Apr 30, 2019
2d83547
Category structure on CVLRS
jcommelin May 1, 2019
583b4a9
Create some nice isos
jcommelin May 1, 2019
a1653b9
unsorrying comp_id and id_comp
kbuzzard May 1, 2019
3ab5284
Pretty clean definition of bundled perfectoid spaces
jcommelin May 2, 2019
cdfdfad
Every perfectoid space is an adic space
jcommelin May 2, 2019
ed9ba34
Get rid of universes, add some comments
jcommelin May 3, 2019
deafb72
Remove everything after the definition of PerfectoidSpace
jcommelin May 3, 2019
237d631
Notation for: nonempty (A ≅ B)
jcommelin May 3, 2019
9efd8c6
CVLRS -> CLVRS
jcommelin May 3, 2019
156d04d
rename Spa → spa, Spa' → Spa
jcommelin May 3, 2019
4c0f2a5
Remove local infix notation at end of files
jcommelin May 3, 2019
d0fa253
Remove old commented code
jcommelin May 3, 2019
4f82685
Write out Bourbaki's name in full
jcommelin May 3, 2019
774223c
Missed a local infix
jcommelin May 3, 2019
d4cf657
Mention Wedhorn's 𝒱 in the docstring of CLVRS
jcommelin May 3, 2019
ff248d0
Remove McC and McV
jcommelin May 3, 2019
94e18e0
Remove superfluous imports
jcommelin May 3, 2019
f7c3806
Revert "Remove superfluous imports"
jcommelin May 3, 2019
203e6d6
Move ugly imports to a lower place in the hierarchy
jcommelin May 3, 2019
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions src/Huber_pair.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -31,14 +31,14 @@ structure is_ring_of_integral_elements {R : Type u} [Huber_ring R] [decidable_eq
-- a Huber Ring is an f-adic ring.
-- a Huber Pair is what Huber called an Affinoid Ring.
structure Huber_pair :=
(R : Type u)
(R : Type) -- change this to (Type u) to enable universes
[RHuber : Huber_ring R]
[dec : decidable_eq R]
(Rplus : set R)
[intel : is_ring_of_integral_elements Rplus]

instance : has_coe_to_sort Huber_pair :=
{ S := Type u, coe := Huber_pair.R }
{ S := Type, coe := Huber_pair.R }

instance Huber_pair.Huber_ring (A : Huber_pair) : Huber_ring A := A.RHuber

Expand Down
Loading