## Stream: maths

### Topic: Cute lemma

#### Patrick Massot (Apr 11 2019 at 20:42):

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 (Apr 11 2019 at 20:43):

@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)

pasted image

#### Patrick Massot (Apr 11 2019 at 20:44):

That's the comment above the lemma

#### Patrick Massot (Apr 11 2019 at 20:45):

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

#### Scott Olson (Apr 11 2019 at 21:08):

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 (Apr 11 2019 at 21:11):

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 (Apr 11 2019 at 21:27):

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

#### Reid Barton (Apr 11 2019 at 21:27):

then the diagram almost turned out to be a cube anyways

#### Reid Barton (Apr 11 2019 at 21:28):

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

#### Reid Barton (Apr 11 2019 at 21:33):

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 (Apr 11 2019 at 21:37):

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

Last updated: May 12 2021 at 08:14 UTC