Zulip Chat Archive

Stream: maths

Topic: flexible indices


view this post on Zulip Johan Commelin (Feb 20 2019 at 09:45):

I'm fooling around with sequences of groups. Here is an extract of some code:

import algebra.group group_theory.subgroup
import category_theory.instances.groups
import category_theory.functor_category
import data.set.function

universes v v₁ v₂ v₃ u u₁ u₂ u₃ -- declare the `v`'s first; see `category_theory.category` for an explanation

namespace category_theory
open set instances
variables (C : Type u₁) [𝒞 : category.{v₁} C]
include 𝒞

def sequence :=   C

namespace sequence

instance : category (sequence C) := functor.category _ _

variables {C} (X : sequence C)

def delta (i : ) {j : } (h : i = j - 1 . obviously) :
  X.obj i  X.obj j :=
X.map $
begin
  rw auto_param_eq at h,
  rw h, tidy,
end

view this post on Zulip Johan Commelin (Feb 20 2019 at 09:45):

What I am after is a nice definition of delta

view this post on Zulip Johan Commelin (Feb 20 2019 at 09:47):

It is the map X.obj i \hom X.obj (i+1) but I want to use unification to replace i with (i-1+1) when necessary.

view this post on Zulip Johan Commelin (Feb 20 2019 at 09:51):

Currently this fails:

variable (i : )
#check X.delta (i-1)  X.delta i

view this post on Zulip Johan Commelin (Feb 20 2019 at 09:51):

Because the second X.delta should be X.delta (i-1+1), which is ugly.

view this post on Zulip Johan Commelin (Feb 20 2019 at 09:59):

My goal is to make things like this typecheck:

variable (A : sequence Group)

def is_complex :=
 (i : ), range (A.delta (i-1))  ker (A.delta i)

view this post on Zulip Kenny Lau (Feb 20 2019 at 10:00):

(never mind)

view this post on Zulip Kenny Lau (Feb 20 2019 at 10:03):

also your code doesn't work because category_theory.instances.groups doesn't exist

view this post on Zulip Johan Commelin (Feb 20 2019 at 10:38):

Yes, I know. It exists on my machine. It's a pity it doesn't yet exist in mathlib.

view this post on Zulip Johan Commelin (Feb 20 2019 at 11:04):

Here is category_theory/instances/groups.lean:

/- Copyright (c) 2018 Johan Commelin. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Johan Commelin

Introduce Group -- the category of groups.

Currently only the basic setup.
Copied from monoids.lean.
-/

import category_theory.concrete_category
import category_theory.fully_faithful
import category_theory.adjunction
import data.finsupp

universes u v

open category_theory

namespace category_theory.instances

/-- The category of groups and group morphisms. -/
@[reducible] def Group : Type (u+1) := bundled group

instance (G : Group) : group G := G.str

instance concrete_is_group_hom :
  concrete_category @is_group_hom :=
by introsI α ia; apply_instance,
  by introsI α β γ ia ib ic f g hf hg; apply_instance

instance Group_hom_is_group_hom {G₁ G₂ : Group} (f : G₁  G₂) :
  is_group_hom (f : G₁  G₂) := f.2

instance : has_one Group := { α := punit, str := by tidy }

/-- The category of commutative groups and group morphisms. -/
@[reducible] def CommGroup : Type (u+1) := bundled comm_group

instance (x : CommGroup) : comm_group x := x.str

@[reducible] def is_comm_group_hom {α β} [comm_group α] [comm_group β] (f : α  β) : Prop :=
is_group_hom f

instance concrete_is_comm_group_hom : concrete_category @is_comm_group_hom :=
by introsI α ia; apply_instance,
  by introsI α β γ ia ib ic f g hf hg; apply_instance

instance CommGroup_hom_is_comm_group_hom {R S : CommGroup} (f : R  S) :
  is_comm_group_hom (f : R  S) := f.2

namespace CommGroup
/-- The forgetful functor from commutative groups to groups. -/
def forget_to_Group : CommGroup  Group :=
concrete_functor
  (by intros _ c; exact { ..c })
  (by introsI _ _ _ _ f i;  exact { ..i })

instance : faithful (forget_to_Group) := {}

instance : has_one CommGroup := { α := punit, str := by tidy }

end CommGroup

end category_theory.instances

view this post on Zulip Kevin Buzzard (Feb 20 2019 at 12:23):

What's the story as to why it's not in mathlib? My MSc student was going to use categories for doing schemes but we decided it wasn't a good idea because categories seemed to be happening too slowly

view this post on Zulip Johan Commelin (Feb 20 2019 at 14:51):

The story is that nobody copied the file about the category of monoids and did a search-replace s/monoid/group/. That's all.

view this post on Zulip Johan Commelin (Feb 26 2019 at 12:13):

My goal is to make things like this typecheck:

variable (A : sequence Group)

def is_complex :=
 (i : ), range (A.delta (i-1))  ker (A.delta i)

Does anyone have an idea how to make this work?
I think writing A.delta (i-1+1) is very very ugly.

view this post on Zulip Mario Carneiro (Feb 26 2019 at 12:14):

Why not use +1 instead of -1?

view this post on Zulip Mario Carneiro (Feb 26 2019 at 12:14):

it's over all integers

view this post on Zulip Mario Carneiro (Feb 26 2019 at 12:15):

Another way to flexify the indices for dependent types is to have an equality argument i+1 = j and have i on the left and j on the right

view this post on Zulip Johan Commelin (Feb 26 2019 at 12:15):

But can we make it transparent?

view this post on Zulip Mario Carneiro (Feb 26 2019 at 12:15):

don't know what you intend to do with this

view this post on Zulip Johan Commelin (Feb 26 2019 at 12:16):

Why not use +1 instead of -1?

I could do that here. But I think this issue will show up elsewhere as soon as we start looking in a broader range of indices.

view this post on Zulip Johan Commelin (Feb 26 2019 at 12:16):

don't know what you intend to do with this
For starters we could try to prove the snake lemma (-;

view this post on Zulip Mario Carneiro (Feb 26 2019 at 12:17):

More generally, you want an inductive family describing the allowable index combinations

view this post on Zulip Mario Carneiro (Feb 26 2019 at 12:17):

In this case it is just inductive next : nat -> nat -> Prop | mk (i) : next i (i+1)

view this post on Zulip Johan Commelin (Feb 26 2019 at 12:18):

Hmm, how do I use next?

view this post on Zulip Johan Commelin (Feb 26 2019 at 12:18):

Should I put that in my definition of delta?

view this post on Zulip Mario Carneiro (Feb 26 2019 at 12:18):

def is_complex :=
 (i j : ), next i j -> range (A.delta i)  ker (A.delta j)

view this post on Zulip Mario Carneiro (Feb 26 2019 at 12:19):

or are you looking somewhere else?

view this post on Zulip Johan Commelin (Feb 26 2019 at 12:22):

Aah, ok

view this post on Zulip Johan Commelin (Feb 26 2019 at 12:23):

But that means I have 3 explicit arguments. So I can't just write A.delta i

view this post on Zulip Johan Commelin (Feb 26 2019 at 12:24):

I would like to tell Lean: "If unification knows what j should be, use that. Otherwise, default to (i+1)."

view this post on Zulip Mario Carneiro (Feb 26 2019 at 12:24):

Yeah, I think so... it's just like with categories, you want the objects to be there before the morphisms, rather than extracting objects as the dom/cod of morphisms

view this post on Zulip Johan Commelin (Feb 26 2019 at 12:25):

And after that I say to Lean: "Hey, 95% of the time you can prove next i j by mk i. Otherwise, simplify the expression for j before doing that."

view this post on Zulip Johan Commelin (Feb 26 2019 at 12:25):

And so in 99% of the cases I can get away with just writing A.delta i. And in 1% of the cases I might to actually work on the proof obligation...

view this post on Zulip Johan Commelin (Feb 26 2019 at 12:26):

If something like that can work, that would be cool.

view this post on Zulip Mario Carneiro (Feb 26 2019 at 12:26):

So is_complex is actually talking about three objects....

view this post on Zulip Mario Carneiro (Feb 26 2019 at 12:27):

def is_complex :=
 {{i j k : }} (n1: next i j) (n2 : next j k), range (A.delta n1)  ker (A.delta n2)

view this post on Zulip Kenny Lau (Feb 26 2019 at 12:27):

what is {{}}?

view this post on Zulip Mario Carneiro (Feb 26 2019 at 12:28):

half implicit, too lazy to unicode

view this post on Zulip Mario Carneiro (Feb 26 2019 at 12:28):

I think it is working ascii notation though

view this post on Zulip Kenny Lau (Feb 26 2019 at 12:28):

what is half implicit?

view this post on Zulip Mario Carneiro (Feb 26 2019 at 12:28):

not applied unless you apply an argument after them

view this post on Zulip Mario Carneiro (Feb 26 2019 at 12:29):

like in the definition of subset

view this post on Zulip Kenny Lau (Feb 26 2019 at 12:29):

:o

view this post on Zulip Johan Commelin (Feb 26 2019 at 12:32):

Hmm, but I think you are working on the wrong part. The definition of delta has to change.

view this post on Zulip Johan Commelin (Feb 26 2019 at 12:33):

is_complex is just an example of something that doesn't typecheck with the current definition of delta.

view this post on Zulip Mario Carneiro (Feb 26 2019 at 12:33):

I did that... A.delta {i j} n1

view this post on Zulip Johan Commelin (Feb 26 2019 at 12:33):

Ooh, right. Ok.

view this post on Zulip Johan Commelin (Feb 26 2019 at 12:33):

But that means I can't write A.delta i, can I?

view this post on Zulip Mario Carneiro (Feb 26 2019 at 12:33):

although possibly i and j shouldn't be implicit - this will print a bit weird if n1 is not a simple term

view this post on Zulip Mario Carneiro (Feb 26 2019 at 12:34):

No, I'm claiming that's a bad idea

view this post on Zulip Mario Carneiro (Feb 26 2019 at 12:35):

If you don't have the objects lying around already, you can use +1 and -1 to access next elements, but if you ever want to link two of them together you need a variable for the common object

view this post on Zulip Mario Carneiro (Feb 26 2019 at 12:35):

is_complex is a good example of this - j is mediating the connection between i and k

view this post on Zulip Mario Carneiro (Feb 26 2019 at 12:35):

I know this looks silly but it's a DTT thing

view this post on Zulip Johan Commelin (Feb 26 2019 at 12:37):

This will be hard to explain to mathematicians...

view this post on Zulip Johan Commelin (Feb 26 2019 at 12:37):

Why can't automation help us here?

view this post on Zulip Mario Carneiro (Feb 26 2019 at 12:38):

because DTT doesn't like it when you try to prove defeqs

view this post on Zulip Johan Commelin (Feb 26 2019 at 12:38):

If Lean figures out j by unification, that's cool. If it didn't: use i+1.

view this post on Zulip Mario Carneiro (Feb 26 2019 at 12:38):

You want all rewriting and stuff to happen in prop land

view this post on Zulip Mario Carneiro (Feb 26 2019 at 12:38):

but delta is data, so it needs a general type

view this post on Zulip Mario Carneiro (Feb 26 2019 at 12:39):

it's not a question of figuring out the expressions, it's about making i+1-1 defeq to i

view this post on Zulip Johan Commelin (Feb 26 2019 at 12:44):

Hmmm, I think that I wouldn't mind if automation could also help us with providing data, and not only proofs.

view this post on Zulip Patrick Massot (Feb 26 2019 at 12:46):

I don't know if automation is the right word here, but it's pretty clear that proof assistants that require using this next trick are not ready for use by mathematicians

view this post on Zulip Mario Carneiro (Feb 26 2019 at 12:46):

It's about wrangling DTT issues

view this post on Zulip Mario Carneiro (Feb 26 2019 at 12:47):

You are causing equality of integers to propagate to equality of types, which is bad

view this post on Zulip Patrick Massot (Feb 26 2019 at 12:47):

I understand. It means we need either better wrangling tools or a better foundational framework. I'm not saying this is an easy question

view this post on Zulip Mario Carneiro (Feb 26 2019 at 12:47):

I am in favor of both of those

view this post on Zulip Patrick Massot (Feb 26 2019 at 12:48):

What a nice thesis topic!

view this post on Zulip Johan Commelin (Feb 26 2019 at 12:49):

Mario, I agree with Patrick. I understand the issues. But the issues are non-mathematical, so they should be hidden. Somehow...

view this post on Zulip Johan Commelin (Feb 26 2019 at 12:50):

In the end, DTT should be our assembly language. We want a Python on top of that.

view this post on Zulip Patrick Massot (Feb 26 2019 at 12:50):

You already have it: the tactic language

view this post on Zulip Mario Carneiro (Feb 26 2019 at 12:50):

DTT is a horrible assembly language

view this post on Zulip Mario Carneiro (Feb 26 2019 at 12:51):

it's like javascript - high level ish but used for low level things

view this post on Zulip Mario Carneiro (Feb 26 2019 at 12:51):

I know a much better proof assembly language, and it starts with M

view this post on Zulip Johan Commelin (Feb 26 2019 at 12:52):

Sure, but is there a Python on top of your M?

view this post on Zulip Johan Commelin (Feb 26 2019 at 12:52):

One that will let me define functors on objects and morphisms, and check that they are lawful in a completely transparent way?

view this post on Zulip Mario Carneiro (Feb 26 2019 at 12:58):

Proof automation is hard, and no one has a perfect solution. Lean could have the stuff you are talking about if it didn't have to fight its own foundation

view this post on Zulip Johan Commelin (Feb 26 2019 at 13:00):

What do you mean with that last sentence?

view this post on Zulip Mario Carneiro (Feb 26 2019 at 13:02):

You could just rewrite i+1-1 = i with the simplifier and we would all be happy

view this post on Zulip Johan Commelin (Feb 26 2019 at 13:22):

Sure, that's exactly what I would want. But what do you mean with:

Lean could have the stuff you are talking about if it didn't have to fight its own foundation
Is that an issue that can be solved, or is this fight some intrinsic DTT issue?

view this post on Zulip Mario Carneiro (Feb 26 2019 at 14:14):

it's an intrinsic DTT issue

view this post on Zulip Mario Carneiro (Feb 26 2019 at 14:14):

defeq matters, and tactics can't change that

view this post on Zulip Johan Commelin (Feb 26 2019 at 14:14):

Aah, so Lean will always be fighting its foundations.

view this post on Zulip Johan Commelin (Feb 26 2019 at 14:17):

So, why don't we write a Python-like on top of your assembly M? Do you think we would get further into state-of-the-art research level maths with a Python-like on top of M? Or is Lean just the best there is, and are we stuck with a system that fights its own foundations?

view this post on Zulip Mario Carneiro (Feb 26 2019 at 14:17):

You are hitting surprisingly close to my current research areas

view this post on Zulip Johan Commelin (Feb 26 2019 at 14:18):

That only means that I've been paying attention to what you've been saying on Zulip over the last couple of months (-;

view this post on Zulip Mario Carneiro (Feb 26 2019 at 14:19):

I think that the killer combo is untyped foundations (ZFC like) + good tactic language + metaprogramming

view this post on Zulip Mario Carneiro (Feb 26 2019 at 14:20):

as you can see lean has 2 out of 3

view this post on Zulip Mario Carneiro (Feb 26 2019 at 14:21):

Isabelle gets pretty close, but it's not quite untyped foundations and as a result they are stuck with some things

view this post on Zulip Johan Commelin (Feb 26 2019 at 14:21):

Hmmm, so why again did you give my colleagues that nlab blogpost on why type theory p0wns set theory?

view this post on Zulip Mario Carneiro (Feb 26 2019 at 14:22):

I didn't write it, and I don't really endorse most of nLab philosophy

view this post on Zulip Mario Carneiro (Feb 26 2019 at 14:22):

but it's a good place to find the philosophy when you want it

view this post on Zulip Johan Commelin (Feb 26 2019 at 17:56):

Why not use +1 instead of -1?

So, for is_complex I could do this. But for is_exact_at (i : int) you need to reference A.obj (i-1) at some point. You can't avoid the subtraction. (Unless you want to break with the indexing conventions, but that will just move the pain to the next page, where it will hit you twice as hard.)

view this post on Zulip Mario Carneiro (Feb 26 2019 at 18:01):

with the next thing, you can say \ex j, next i j /\ ...

view this post on Zulip Mario Carneiro (Feb 26 2019 at 18:02):

but depending on what you want to say just plain A.obj (i-1) might be best

view this post on Zulip Johan Commelin (Feb 26 2019 at 18:05):

So what is actually the benefit of next? Why can't I just write a condition (h : j = i+1) in the definition of delta?

view this post on Zulip Mario Carneiro (Feb 26 2019 at 18:05):

you can

view this post on Zulip Mario Carneiro (Feb 26 2019 at 18:05):

but it generalizes to more complicated index structures

view this post on Zulip Johan Commelin (Feb 26 2019 at 18:09):

I see...

view this post on Zulip Mario Carneiro (Feb 26 2019 at 18:09):

I'm not saying you should necessarily use it here

view this post on Zulip Reid Barton (Feb 26 2019 at 18:11):

Another example of this index business is (commutative / graded commutative) graded algebras

view this post on Zulip Reid Barton (Feb 26 2019 at 18:12):

where multiplication is a family of operations m:Ai×AjAi+jm : A_i \times A_j \to A_{i+j} and mm is supposed to be, say, associative, but stating that depends on the associativity of addition of indices

view this post on Zulip Johan Commelin (Feb 26 2019 at 18:13):

@Mario Carneiro Do you know how mathematicians write the predicate is_complex?
They just write A.delta \circ A.delta = 0
Now, I thought I should write \forall i, A.delta i \circ A.delta (i-1) = 0. But you are telling me I need 3 explicit arguments... it will probably take my psyche some time to adjust.

view this post on Zulip Johan Commelin (Feb 26 2019 at 18:15):

@Reid Barton Yeah, I was thinking about those a bit. (Because you can of course also do sequences as graded modules with a differential of degree 1.) I really don't know if the A_i should be an indexed family of types or an indexed family of subsets... We will probably need both...

view this post on Zulip Sebastien Gouezel (Feb 26 2019 at 19:15):

Mario Carneiro Do you know how mathematicians write the predicate is_complex?
They just write A.delta \circ A.delta = 0

You can also write it in this way in Lean if you think of the total space of your complex as a group/module/whatever (with an additional filtered structure), and A.deltaas a group/module/whatever morphism that, incidentally, happens to respect the filtration.

view this post on Zulip Johan Commelin (Feb 26 2019 at 19:23):

Yes, but I fear that will make talking about homogeneous elements a lot more awkward...


Last updated: May 12 2021 at 07:17 UTC