-
Notifications
You must be signed in to change notification settings - Fork 12
/
liquid.lean
135 lines (117 loc) · 5.28 KB
/
liquid.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
import thm95
import statement
/-!
# Liquid Tensor Experiment
This file is the entry point for this project.
The first goal of the Liquid Tensor Experiment
is to formalize a theorem by Clausen and Scholze stated below,
namely a mix of Theorem 9.4 and Theorem 9.5 of
[Analytic]: http://www.math.uni-bonn.de/people/scholze/Analytic.pdf
**How to browse this project? See `README.md` in the root of the repository.**
We will now state the main theorem.
First we need to fix a package of data corresponding to the Breen--Deligne resolution.
If you don't know the Breen--Deligne resolution, don't worry,
we'll explain more about how to find out more about it below.
Once we have fixed this data, we can state the theorem.
-/
universe variables u
open_locale nnreal -- enable the notation `ℝ≥0` for the nonnegative real numbers.
open category_theory ProFiltPseuNormGrpWithTinv polyhedral_lattice opposite
variables (r r' : ℝ≥0)
variables [fact (0 < r)] [fact (0 < r')] [fact (r < r')] [fact (r' < 1)]
variables (BD : breen_deligne.package) (κ : ℕ → ℝ≥0)
variables [BD.data.very_suitable r r' κ] [∀ (i : ℕ), fact (0 < κ i)]
include r r' BD κ
/-- A mix of Theorems 9.4 and 9.5 in [Analytic] -/
theorem first_target :
∀ m : ℕ, ∃ (k K : ℝ≥0) (hk : fact (1 ≤ k)) (c₀ : ℝ≥0),
∀ (S : Type) [fintype S] (V : SemiNormedGroup.{u}) [normed_with_aut r V],
((BD.data.system κ r V r').obj (op $ of r' (Lbar r' S))).is_weak_bounded_exact k K m c₀ :=
begin
intro m,
obtain ⟨k, K, hk, H⟩ := thm95'' BD r r' κ m,
obtain ⟨c₀, H⟩ := H ℤ,
use [k, K, hk, c₀],
introsI S hS V hV,
specialize H S V,
let i := (BD.data.system κ r V r').map_iso (HomZ_iso (of r' $ Lbar r' S)).op,
refine H.of_iso i.symm _,
intros c n,
rw ← system_of_complexes.apply_hom_eq_hom_apply,
apply SemiNormedGroup.iso_isometry_of_norm_noninc;
apply breen_deligne.data.complex.map_norm_noninc
end
/-!
## On the statement
Most of the theorem should be fairly readable.
We will now briefly explain some of the more peculiar syntax.
The proof reduces to `thm95''` (a variant of Theorem 9.5).
* `[BD.suitable κ]` assumes that the nonnegative reals `κ i` satisfy some suitable conditions
with respect to the package of Breen--Deligne data `BD`.
* `[fact (0 < r)]` records the "fact" `0 < r` as an assumption to whatever comes later.
* `(S : Type) [fintype S]` is Lean's way of saying "`S` is a finite set".
See also the "Brief note on type theory" in `README.md`.
* `[normed_with_aut r V]` adds the assumption that `V` is endowed with an automorphism `T`
that scales elements `v` of `V` by the positive scalar `r`: `∥T(v)∥ = r * ∥v∥`.
* `Lbar_system` is the system of complexes of seminormed groups
occuring in Theorems 9.4/9.5 of [Analytic].
* `is_bounded_exact` is the assertion that a system of complexes
of seminormed groups satisfies a suitable exactness criterion of being
`≤ k`-exact in degrees `≤ m` for `c ≥ c₀` (where `c` is an index to the system of complexes).
-/
example : first_target_stmt r r' BD κ := first_target r r' BD κ
/-- Theorem 9.4 in [Analytic] for weak bounded exactness -/
theorem thm94_weak :
∀ m : ℕ, ∃ (k K : ℝ≥0) (hk : fact (1 ≤ k)) (c₀ : ℝ≥0),
∀ (S : Profinite) (V : SemiNormedGroup.{u}) [normed_with_aut r V],
((BD.data.system κ r V r').obj (op $ of r' ((Lbar.functor.{0 0} r').obj S)))
.is_weak_bounded_exact k K m c₀ :=
begin
intro m,
obtain ⟨k, K, hk, H⟩ := thm95''.profinite BD r r' κ m,
obtain ⟨c₀, H⟩ := H ℤ,
use [k, K, hk, c₀],
introsI S V hV,
specialize H S V,
let i := (BD.data.system κ r V r').map_iso (HomZ_iso (of r' $ (Lbar.functor.{0 0} r').obj S)).op,
refine H.of_iso i.symm _,
intros c n,
rw ← system_of_complexes.apply_hom_eq_hom_apply,
apply SemiNormedGroup.iso_isometry_of_norm_noninc;
apply breen_deligne.data.complex.map_norm_noninc
end
/-- Theorem 9.4 in [Analytic] -/
theorem thm94 :
∀ m : ℕ, ∃ (k K : ℝ≥0) (hk : fact (1 ≤ k)) (c₀ : ℝ≥0),
∀ (S : Profinite) (V : SemiNormedGroup.{u}) [normed_with_aut r V],
((BD.data.system κ r V r').obj (op $ of r' ((Lbar.functor.{0 0} r').obj S)))
.is_bounded_exact k K m c₀ :=
begin
intro m,
obtain ⟨k, K, hk, c₀, H⟩ := thm94_weak r r' BD κ m,
resetI,
refine ⟨k ^ 2, K + 1, infer_instance, c₀, _⟩,
introsI,
refine system_of_complexes.is_weak_bounded_exact.strong_of_complete _ (H _ _) _ _ zero_lt_one,
apply breen_deligne.data.system_admissible,
end
/-- Theorem 9.4 in [Analytic] for weak bounded exactness -/
theorem thm94_weak' :
∀ m : ℕ, ∃ (k K : ℝ≥0) (hk : fact (1 ≤ k)) (c₀ : ℝ≥0),
∀ (S : Profinite) (V : SemiNormedGroup.{u}) [normed_with_aut r V],
((BD.data.system κ r V r').obj (op $ of r' ((Lbar.functor.{0 0} r').obj S)))
.is_weak_bounded_exact k K m c₀ :=
begin
intro m,
obtain ⟨k, K, hk, H⟩ := thm95''.profinite BD r r' κ m,
obtain ⟨c₀, H⟩ := H ℤ,
use [k, K, hk, c₀],
introsI S V hV,
specialize H S V,
let i := (BD.data.system κ r V r').map_iso (HomZ_iso (of r' $ (Lbar.functor.{0 0} r').obj S)).op,
refine H.of_iso i.symm _,
intros c n,
rw ← system_of_complexes.apply_hom_eq_hom_apply,
apply SemiNormedGroup.iso_isometry_of_norm_noninc;
apply breen_deligne.data.complex.map_norm_noninc
end