Types that should be equal

Stream: new members

[Zhangir Azerbayev]

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]

congratulations, you've run into dependent type hell

[Kenny Lau]

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

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]

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]

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

[Kenny Lau]

and that will stop you from comparing the elements therein

[Kevin Buzzard]

But then how will he state associativity?

[Kevin Buzzard]

@Reid Barton are we now stuck?

[Kenny Lau]

what does nLab have to say about this

[Kevin Buzzard]

But we know the trick

[Kenny Lau]

pentagon mode

[Kevin Buzzard]

Mario did the trick in the DGA thread

[Kenny Lau]

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

[Kenny Lau]

the pentagon is the associativity

[Kevin Buzzard]

No, just do the mario trick

[Kenny Lau]

what is DGA?

[Kenny Lau]

I mean, what do you do in maths

[Kevin Buzzard]

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

[Kenny Lau]

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

[Kevin Buzzard]

See the link

[Kenny Lau]

oh I remember that trick now

[Kenny Lau]

so you say we keep using nat?

[Kevin Buzzard]

Why not?

[Kevin Buzzard]

The trick works well enough to make the definition

[Kevin Buzzard]

I think it is worth trying

[Kevin Buzzard]

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

[Kenny Lau]

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

[Kenny Lau]

where you have triple intersections of sets

[Kenny Lau]

what did you do with it?

[Kevin Buzzard]

No I completely forgot

[Kevin Buzzard]

I want to go back to hell

[Kenny Lau]

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

[Kenny Lau]

i.e. just work with the full exterior algebra

[Kevin Buzzard]

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

[Kenny Lau]

not now

[Zhangir Azerbayev]

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]

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]

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]

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]

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]

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]

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

[Adam Topaz]

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

[Scott Morrison]

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

[Adam Topaz]

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]

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]

Quick, quick, make a PR! :-)

[Scott Morrison]

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.

[Scott Morrison]

Very nicely done!

[Adam Topaz]

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

[Scott Morrison]

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

[Adam Topaz]

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

[Adam Topaz]

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]

Ping @Utensil Song who is likely interested in this conversation

[Adam Topaz]

Same @Colter MacDonald