# Zulip Chat Archive

## Stream: new members

### Topic: Types that should be equal

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

#### Kenny Lau (Jul 22 2020 at 19:00):

congratulations, you've run into dependent type hell

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

#### Alex J. Best (Jul 22 2020 at 19:09):

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

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

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

#### Kenny Lau (Jul 22 2020 at 19:11):

and that will stop you from comparing the elements therein

#### Kevin Buzzard (Jul 22 2020 at 19:11):

But then how will he state associativity?

#### Kevin Buzzard (Jul 22 2020 at 19:12):

@Reid Barton are we now stuck?

#### Kenny Lau (Jul 22 2020 at 19:12):

what does nLab have to say about this

#### Kevin Buzzard (Jul 22 2020 at 19:12):

But we know the trick

#### Kenny Lau (Jul 22 2020 at 19:12):

pentagon mode

#### Kevin Buzzard (Jul 22 2020 at 19:12):

Mario did the trick in the DGA thread

#### Kenny Lau (Jul 22 2020 at 19:12):

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

#### Kenny Lau (Jul 22 2020 at 19:12):

the pentagon is the associativity

#### Kevin Buzzard (Jul 22 2020 at 19:13):

No, just do the mario trick

#### Kenny Lau (Jul 22 2020 at 19:13):

what is DGA?

#### Kenny Lau (Jul 22 2020 at 19:13):

I mean, what do you do in maths

#### Kevin Buzzard (Jul 22 2020 at 19:14):

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

#### Kenny Lau (Jul 22 2020 at 19:14):

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

#### Kevin Buzzard (Jul 22 2020 at 19:14):

See the link

#### Kenny Lau (Jul 22 2020 at 19:14):

oh I remember that trick now

#### Kenny Lau (Jul 22 2020 at 19:15):

so you say we keep using nat?

#### Kevin Buzzard (Jul 22 2020 at 19:15):

Why not?

#### Kevin Buzzard (Jul 22 2020 at 19:15):

The trick works well enough to make the definition

#### Kevin Buzzard (Jul 22 2020 at 19:15):

I think it is worth trying

#### Kevin Buzzard (Jul 22 2020 at 19:16):

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

#### Kenny Lau (Jul 22 2020 at 19:16):

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

#### Kenny Lau (Jul 22 2020 at 19:16):

where you have triple intersections of sets

#### Kenny Lau (Jul 22 2020 at 19:16):

what did you do with it?

#### Kevin Buzzard (Jul 22 2020 at 19:16):

No I completely forgot

#### Kevin Buzzard (Jul 22 2020 at 19:16):

I want to go back to hell

#### Kenny Lau (Jul 22 2020 at 19:18):

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

#### Kenny Lau (Jul 22 2020 at 19:18):

i.e. just work with the full exterior algebra

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

#### Kenny Lau (Jul 22 2020 at 21:01):

not now

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

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

#### 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 : V → A$ such that $j(v)j(v) = 0$ for every $v \in V$ and prove things about that to start.

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

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

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

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

#### Adam Topaz (Jul 23 2020 at 00:23):

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

#### Scott Morrison (Jul 23 2020 at 00:24):

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

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

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

#### Scott Morrison (Jul 23 2020 at 03:51):

Quick, quick, make a PR! :-)

#### Scott Morrison (Jul 23 2020 at 03:55):

Possible additions:

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

#### Scott Morrison (Jul 23 2020 at 03:55):

Very nicely done!

#### Adam Topaz (Jul 23 2020 at 03:56):

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

#### Scott Morrison (Jul 23 2020 at 03:57):

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

#### Adam Topaz (Jul 23 2020 at 03:58):

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

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

#### Eric Wieser (Jul 23 2020 at 07:38):

Ping @Utensil Song who is likely interested in this conversation

#### Adam Topaz (Jul 23 2020 at 14:14):

Same @Colter MacDonald

Last updated: May 13 2021 at 00:41 UTC