Zulip Chat Archive

Stream: maths

Topic: Cute lemma


view this post on Zulip 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)
  ( :  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

view this post on Zulip 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)

view this post on Zulip Patrick Massot (Apr 11 2019 at 20:44):

pasted image

view this post on Zulip Patrick Massot (Apr 11 2019 at 20:44):

That's the comment above the lemma

view this post on Zulip 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

view this post on Zulip 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:

view this post on Zulip 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

view this post on Zulip Reid Barton (Apr 11 2019 at 21:27):

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

view this post on Zulip Reid Barton (Apr 11 2019 at 21:27):

then the diagram almost turned out to be a cube anyways

view this post on Zulip Reid Barton (Apr 11 2019 at 21:28):

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

view this post on Zulip 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

view this post on Zulip 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