Zulip Chat Archive

Stream: new members

Topic: Types that should be equal


view this post on Zulip Zhangir Azerbayev (Jul 22 2020 at 18:50):

When trying to define the exterior product, I've run into the following issue.

universe u
variables (K V : Type u) [field K] [add_comm_group V] [vector_space K V]
variable (q : )

inductive eqv : free_add_monoid (fin q  V)  free_add_monoid (fin q  V)  Prop
/-
A bunch of relations go here
-/

def exterior_product : Type u := (add_con_gen (exterior_product.eqv K V q)).quotient

def mul {q1 q2 : } : exterior_product K V q1  exterior_product K V q2  exterior_product K V (q1 + q2) := sorry

variables (x : exterior_product K V q1) (y : exterior_product K V q2)

#check mul K x y + mul K y x --fails
/-
exterior_algebra.lean:111:19
type mismatch at application
  mul K y
term
  y
has type
  exterior_product K V q2
but is expected to have type
  exterior_product K V q1
exterior_algebra.lean:111:19
type mismatch at application
  mul K ⁇ x
term
  x
has type
  exterior_product K V q1
but is expected to have type
  exterior_product K V q2
-/

Lean doesn't understand that exterior_algebra K V (q1 + q2) and exterior_algebra K V (q2 + q1) are the same type. Always carrying around an isomorphism would make my code complicated and unusable. Is there a better way?

view this post on Zulip Kenny Lau (Jul 22 2020 at 19:00):

congratulations, you've run into dependent type hell

view this post on Zulip Kenny Lau (Jul 22 2020 at 19:08):

@Kevin Buzzard will gladly give you a 1-hour lecture on how this is all doomed, but maybe you can read this thread instead

view this post on Zulip Alex J. Best (Jul 22 2020 at 19:09):

You could try and work in the full exterior algebra instead I.e. qq\bigoplus_q \wedge^q instead of different q\wedge^q separately

view this post on Zulip Kenny Lau (Jul 22 2020 at 19:10):

I guess a way to solve this is, as I have told you on Discord before, to use arbitrary fintype instead of fin q

view this post on Zulip Kenny Lau (Jul 22 2020 at 19:10):

then you will get two types that are not (provably) equal, namely A1 (+) A2 and A2 (+) A1

view this post on Zulip Kenny Lau (Jul 22 2020 at 19:11):

and that will stop you from comparing the elements therein

view this post on Zulip Kevin Buzzard (Jul 22 2020 at 19:11):

But then how will he state associativity?

view this post on Zulip Kevin Buzzard (Jul 22 2020 at 19:12):

@Reid Barton are we now stuck?

view this post on Zulip Kenny Lau (Jul 22 2020 at 19:12):

what does nLab have to say about this

view this post on Zulip Kevin Buzzard (Jul 22 2020 at 19:12):

But we know the trick

view this post on Zulip Kenny Lau (Jul 22 2020 at 19:12):

pentagon mode

view this post on Zulip Kevin Buzzard (Jul 22 2020 at 19:12):

Mario did the trick in the DGA thread

view this post on Zulip Kenny Lau (Jul 22 2020 at 19:12):

https://ncatlab.org/nlab/show/pentagon+identity

view this post on Zulip Kenny Lau (Jul 22 2020 at 19:12):

the pentagon is the associativity

view this post on Zulip Kevin Buzzard (Jul 22 2020 at 19:13):

No, just do the mario trick

view this post on Zulip Kenny Lau (Jul 22 2020 at 19:13):

what is DGA?

view this post on Zulip Kenny Lau (Jul 22 2020 at 19:13):

I mean, what do you do in maths

view this post on Zulip Kevin Buzzard (Jul 22 2020 at 19:14):

https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/CDGAs/near/167999328

view this post on Zulip Kenny Lau (Jul 22 2020 at 19:14):

it isn't like (X×Y)×Z=X×(Y×Z)(X \times Y) \times Z = X \times (Y \times Z) in ZFC either

view this post on Zulip Kevin Buzzard (Jul 22 2020 at 19:14):

See the link

view this post on Zulip Kenny Lau (Jul 22 2020 at 19:14):

oh I remember that trick now

view this post on Zulip Kenny Lau (Jul 22 2020 at 19:15):

so you say we keep using nat?

view this post on Zulip Kevin Buzzard (Jul 22 2020 at 19:15):

Why not?

view this post on Zulip Kevin Buzzard (Jul 22 2020 at 19:15):

The trick works well enough to make the definition

view this post on Zulip Kevin Buzzard (Jul 22 2020 at 19:15):

I think it is worth trying

view this post on Zulip Kevin Buzzard (Jul 22 2020 at 19:16):

Gouezel defined tangent spaces in a weird way but could still work with them

view this post on Zulip Kenny Lau (Jul 22 2020 at 19:16):

@Kevin Buzzard I'm sure you remember the sheaf hell

view this post on Zulip Kenny Lau (Jul 22 2020 at 19:16):

where you have triple intersections of sets

view this post on Zulip Kenny Lau (Jul 22 2020 at 19:16):

what did you do with it?

view this post on Zulip Kevin Buzzard (Jul 22 2020 at 19:16):

No I completely forgot

view this post on Zulip Kevin Buzzard (Jul 22 2020 at 19:16):

I want to go back to hell

view this post on Zulip Kenny Lau (Jul 22 2020 at 19:18):

so it looks like @Alex J. Best already gave the answer long before I recognized it

view this post on Zulip Kenny Lau (Jul 22 2020 at 19:18):

i.e. just work with the full exterior algebra

view this post on Zulip Kevin Buzzard (Jul 22 2020 at 21:01):

@Kenny Lau can you write the definition for @Zhangir Azerbayev so he can start on the API?

view this post on Zulip Kenny Lau (Jul 22 2020 at 21:01):

not now

view this post on Zulip Zhangir Azerbayev (Jul 22 2020 at 21:11):

After looking at Mario's trick, doing the full algebra does seem like the best way. My current thoughts are that I could make a monoid on fin k → V where the multiplication is concatenation, define a free additive monoid on that structure, and then quotient by all the right relations. Does that sound like it will work?

view this post on Zulip Zhangir Azerbayev (Jul 22 2020 at 22:05):

Is it a general principle that in Lean it's better to work "top down" rather than "bottom up", because when you try to glue things together you tend to run into these kinds of problems?

view this post on Zulip Alex J. Best (Jul 22 2020 at 22:45):

It is good to get the definitions right before you get too far in, but oftentimes the only way you know if the definitions work or not is if you try and use them, or by asking some experts first! The other way you can go is even if you aren't sure exactly how the definition will work limiting yourself to some interface of properties that you know must be true. For example with the real numbers lets say you wanted to define them but weren't sure wether to use dedekind cuts or completions of cauchy sequences, you could still start proving stuff about the reals provided you only used the fact they were an ordered field where every (nonempty bounded) set has a supremum.
For the example of the exterior algebra, you could just take it as an axiom that you have a type satisfying the universal property https://en.wikipedia.org/wiki/Exterior_algebra#Universal_property even if you didn't yet construct it, or just assume you have any unital associative K-algebra A and a K-linear map j:VAj : V → A such that j(v)j(v)=0j(v)j(v) = 0 for every vVv \in V and prove things about that to start.

view this post on Zulip Scott Morrison (Jul 22 2020 at 23:40):

That is, define the predicate is_exterior_algebra V Λ asserting that Λ satisfies the universal property. Now go develop the material you want about exterior algebras using that, and come back later to give a (gross, if necessary) construction.

view this post on Zulip Scott Morrison (Jul 22 2020 at 23:42):

Best of all, you end up having developed a library that is immune to slow elaboration due to heavy rfl / weird definitional unification / fragility of theorems wrt definitions, etc.

view this post on Zulip Adam Topaz (Jul 22 2020 at 23:54):

You can also define the exterior algebra using the universal property:

import ring_theory.algebra
import linear_algebra

variables (R : Type*) [comm_ring R]
variables (M : Type*) [add_comm_group M] [module R M]

inductive pre
| of : M  pre
| zero : pre
| one : pre
| mul : pre  pre  pre
| add : pre  pre  pre
| smul : R  pre  pre

def lift_fun {A : Type*} [ring A] [algebra R A] (f : M [R] A) : pre R M  A :=
  λ t, pre.rec_on t f 0 1 (λ _ _, (*)) (λ _ _, (+)) (λ x _ a, x  a)

namespace extalg
def rel : (pre R M)  (pre R M)  Prop := λ x y,
   (A : Type*) (h1 : ring A), by letI := h1; exact
   (h2 : algebra R A), by letI := h2; exact
   (f : M [R] A), ( m, (f m) * (f m) = 0) 
  (lift_fun R M f) x = (lift_fun R M f) y

def setoid : setoid (pre R M) := rel R M,
begin
  refine ⟨_,_,_⟩,
  { intros x _ _ _ _ _ _ _, refl, },
  { intros x y h _ _ _ _ _ _ _, symmetry, apply h, assumption, },
  { intros x y z h1 h2 _ _ _ _ _ _ _, rw [h1,h2], assumption', },
end
end extalg

def extalg := quotient (extalg.setoid R M) -- the exterior algebra.

view this post on Zulip Scott Morrison (Jul 23 2020 at 00:19):

Nicely done! (Except, of course, it's not the exterior algebra until you've shown that it satisfies the universal property. :-)

view this post on Zulip Adam Topaz (Jul 23 2020 at 00:23):

Yeah, I'm too lazy to even show it's a ring :laughing:

view this post on Zulip Scott Morrison (Jul 23 2020 at 00:24):

I guess it makes sense to define the tensor algebra first?

view this post on Zulip Adam Topaz (Jul 23 2020 at 00:26):

Sure, why not?

import ring_theory.algebra
import linear_algebra

variables (R : Type*) [comm_ring R]
variables (M : Type*) [add_comm_group M] [module R M]

inductive pre
| of : M  pre
| zero : pre
| one : pre
| mul : pre  pre  pre
| add : pre  pre  pre
| smul : R  pre  pre

def lift_fun {A : Type*} [ring A] [algebra R A] (f : M [R] A) : pre R M  A :=
  λ t, pre.rec_on t f 0 1 (λ _ _, (*)) (λ _ _, (+)) (λ x _ a, x  a)

namespace tensoralg
def rel : (pre R M)  (pre R M)  Prop := λ x y,
   (A : Type*) (h1 : ring A), by letI := h1; exact
   (h2 : algebra R A), by letI := h2; exact
   (f : M [R] A),
  (lift_fun R M f) x = (lift_fun R M f) y

def setoid : setoid (pre R M) := rel R M,
begin
  refine ⟨_,_,_⟩,
  { intros x _ _ _ _ _ _ , refl, },
  { intros x y h _ _ _ _  _ _, symmetry, apply h, },
  { intros x y z h1 h2 _ _ _ _ _ _, rw [h1,h2], },
end
end tensoralg

def tensoralg := quotient (tensoralg.setoid R M) -- the tensor algebra.

view this post on Zulip Adam Topaz (Jul 23 2020 at 03:14):

Scott Morrison said:

I guess it makes sense to define the tensor algebra first?

Okay. I proved the universal property for the tensor algebra.
https://gist.github.com/adamtopaz/84315ae5b11319013707b2d0804fb37e

view this post on Zulip Scott Morrison (Jul 23 2020 at 03:51):

Quick, quick, make a PR! :-)

view this post on Zulip Scott Morrison (Jul 23 2020 at 03:55):

Possible additions:

  1. define the structure is_tensor_algebra (which will be a Type-valued but still subsingleton "predicate") before you even start on the construction, and show at the end that you've built such a structure
  2. we have the categories of R-algebras and R-modules, and the forgetful functor as well --- so check that we're really talking about the right universal property in the first place by checking this construction is the left adjoint of the forgetful functor.

view this post on Zulip Scott Morrison (Jul 23 2020 at 03:55):

Very nicely done!

view this post on Zulip Adam Topaz (Jul 23 2020 at 03:56):

I'm a little concerned about universe issues with the way I've defined the relation...

view this post on Zulip Scott Morrison (Jul 23 2020 at 03:57):

ooh... indeed. Time to add universe annotations everywhere and see what happens.

view this post on Zulip Adam Topaz (Jul 23 2020 at 03:58):

Yeah. I'll have to play with it tomorrow. It's late here.

view this post on Zulip Adam Topaz (Jul 23 2020 at 03:59):

But universes are not an issue for the left adjoint property, since objects in these categories all have the same universe level anyway

view this post on Zulip Eric Wieser (Jul 23 2020 at 07:38):

Ping @Utensil Song who is likely interested in this conversation

view this post on Zulip Adam Topaz (Jul 23 2020 at 14:14):

Same @Colter MacDonald


Last updated: May 13 2021 at 00:41 UTC