# Zulip Chat Archive

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

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

#### 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₁₃)

#### 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