breen_deligne.suitable

Stream: condensed mathematics

[Johan Commelin]

I pushed some sorrys to breen_deligne.suitable. Anyone interested in fooling around with Breen--Deligne data and explicit (block) matrices should feel free to kill them (-;

[Kevin Buzzard]

Do we still only have 2x2 block matrices?

[Adam Topaz]

Doesn't 2×2 suffice for the BD stuff? These are used in the BD homotopy from addition, right?

[Kevin Buzzard]

Yes I should think so, I just noticed it when I was documenting the files :-)

[Johan Commelin]

I've added

def very_suitable (f : universal_map m n) (r r' : out_param ℝ≥0) (c₁ c₂ : ℝ≥0) : Prop :=
∃ (N k : ℕ) (c' : ℝ≥0), f.bound_by N ∧ f.suitable c₁ c' ∧ r ^ k * N ≤ 1 ∧ c' ≤ r' ^ k * c₂

and

class very_suitable (BD : data) (r r' : out_param ℝ≥0) (c_ : ℕ → ℝ≥0) : Prop :=
(universal_very_suitable : ∀ i j, (BD.d i j).very_suitable r r' (c_ i) (c_ j))

[Johan Commelin]

Under the assumption BD.very_suitable r r' c_, Lean now agrees that the double complex used in the proof of thm9.5 is admissible

[Eric Wieser]

Does out_param do anything in a def?