Cute lemma

Stream: maths

[Patrick Massot]

I think I have the right statement I was missing for a tiny part of the perfectoid project that slowed me down since two days ago:

lemma continuous_extend_of_really_wants_to
  {X : Type*} {Y : Type*} {R : Type*} {S : Type*}
  {X' : Type*} {Y' : Type*} {R' : Type*} {S' : Type*}
  [uniform_space X] [uniform_space Y] [uniform_space R] [uniform_space S]
  [topological_space X'] [topological_space Y'] [topological_space R'] [topological_space S']
  (i_X : X' → X) (j_X : X → Y) (k_X : X' → Y') (i_Y : Y' → Y)
  (i_R : R' → R) (j_R : R → S) (k_R : R' → S') (i_S : S' → S) (φ : X' → R')
  (hiX : dense_embedding i_X) (hkX : dense_embedding k_X) (hiY : dense_embedding i_Y)
  (hiR : dense_embedding i_R) (hkR : dense_embedding k_R) (hiS : dense_embedding i_S)
  (hjX : uniform_embedding j_X) (hjR : uniform_embedding j_R)
  (hX : j_X ⁻¹' range i_Y ⊆ range i_X) (hR : -range i_S ⊆ j_R '' -range i_R)
  (hφ : ∀ F : filter X', cauchy_of i_X F → (∀ x ∉ range i_X, (comap i_X $ 𝓝 x) ⊓ F = ⊥) →
           (cauchy_of i_R $ map φ F) ∧ ∀ r ∉ range i_R, (comap i_R $ 𝓝 r) ⊓ map φ F = ⊥) :
  continuous (hkX.extend φ) :=
sorry

[Patrick Massot]

@Sebastian Ullrich At some point we'll really need a version of Lean which allows to write the first four lines of assumptions in a more concise way (fixing the Type* bug would be a nice first step)

[Patrick Massot]

pasted image

[Patrick Massot]

That's the comment above the lemma

[Patrick Massot]

It's not so bad, much bigger diagrams will have to be handled by Lean at some point

[Scott Olson]

It's a dependently typed language, just make a function that parses the diagram from a string and generates the type of the lemma :smiley:

[Scott Olson]

Programming languages in general tend to struggle with areas of math that are usually filled with diagrams on paper... even outside the theorem proving world, low-level graphics programming tends to be full of comments with ASCII diagrams like that

[Reid Barton]

I misread the title as "cube lemma" at first and got excited for a moment

[Reid Barton]

then the diagram almost turned out to be a cube anyways

[Reid Barton]

Using category theory (or just bundled objects and morphisms) helps a little bit

[Reid Barton]

This is the biggest diagram I've encountered so far
https://github.com/rwbarton/lean-homotopy-theory/blob/lean-3.4.2/src/homotopy_theory/formal/cofibrations/gluing.lean#L18

variables {a₁ a₂ a₃ a₄ b₁ b₂ b₃ b₄ : C}
  {f₁₂ : a₁ ⟶ a₂} {f₁₃ : a₁ ⟶ a₃} {f₂₄ : a₂ ⟶ a₄} {f₃₄ : a₃ ⟶ a₄}
  (po_f : Is_pushout f₁₂ f₁₃ f₂₄ f₃₄)
  {g₁₂ : b₁ ⟶ b₂} {g₁₃ : b₁ ⟶ b₃} {g₂₄ : b₂ ⟶ b₄} {g₃₄ : b₃ ⟶ b₄}
  (po_g : Is_pushout g₁₂ g₁₃ g₂₄ g₃₄)
  {u₁ : a₁ ⟶ b₁} {u₂ : a₂ ⟶ b₂} {u₃ : a₃ ⟶ b₃} -- u₄ will be the induced map of pushouts
  (ha₁ : cofibrant a₁) (ha₃ : cofibrant a₃) (hb₁ : cofibrant b₁) (hb₃ : cofibrant b₃)
  (hf₁₂ : is_cof f₁₂) (hg₁₂ : is_cof g₁₂)
  (hwu₁ : is_weq u₁) (hwu₂ : is_weq u₂) (hwu₃ : is_weq u₃)
  (s₁₂ : f₁₂ ≫ u₂ = u₁ ≫ g₁₂) (s₁₃ : f₁₃ ≫ u₃ = u₁ ≫ g₁₃)

cube.png

[Reid Barton]

Patrick's diagram is trickier though because there are really two categories