Zulip Chat Archive

Stream: general

Topic: structures


view this post on Zulip Kevin Buzzard (Mar 08 2018 at 19:49):

When I was building the complexes, I think I tried to make them a field all in one go, and there were problems which perhaps were something to do with neg or sub. @Mario Carneiro showed me how to fix these problems by showing first that the complexes were an additive group and then only afterwards that they were a field. But I cannot remember what the problems were. Can anyone here guess? Was it something to do with defining sub or neg myself vs letting the system somehow do it for me? I now cannot really imagine how the system would do it for me.

view this post on Zulip Johan Commelin (Aug 02 2018 at 07:58):

How am I supposed to finish of this triviality?

C : Type u,
cat : category C
 {Hom := category.Hom cat,
     identity := 𝟙,
     compose := category.compose cat,
     left_identity := _,
     right_identity := _,
     associativity := _} =
    cat

view this post on Zulip Johan Commelin (Aug 02 2018 at 07:58):

It is just asking me whether sum structure cat is equal to the structure built from the fields of cat.

view this post on Zulip Kenny Lau (Aug 02 2018 at 07:58):

congr or ext

view this post on Zulip Johan Commelin (Aug 02 2018 at 07:59):

To which I reply: "Yes! Of course it is."

view this post on Zulip Kenny Lau (Aug 02 2018 at 07:59):

oh no

view this post on Zulip Kenny Lau (Aug 02 2018 at 07:59):

cases cat

view this post on Zulip Kenny Lau (Aug 02 2018 at 07:59):

then dsimp

view this post on Zulip Johan Commelin (Aug 02 2018 at 07:59):

aha

view this post on Zulip Kenny Lau (Aug 02 2018 at 07:59):

I'm not sure because this is not an MWE

view this post on Zulip Johan Commelin (Aug 02 2018 at 07:59):

congr failed, and ext did nothing.

view this post on Zulip Kenny Lau (Aug 02 2018 at 08:00):

if ext did nothing, then it is because you don't have an extensionality lemma, i.e. the interface

view this post on Zulip Kenny Lau (Aug 02 2018 at 08:00):

@[extensionality] lemma category.ext : ...

view this post on Zulip Johan Commelin (Aug 02 2018 at 08:02):

lemma op_op' : @opposites.Opposite C (@opposites.Opposite C cat) = cat :=
begin
  tactic.unfreeze_local_instances,
  cases cat,
  dsimp [opposites.Opposite],
  congr
end -- We win!

view this post on Zulip Johan Commelin (Aug 02 2018 at 08:02):

That worked.

view this post on Zulip Johan Commelin (Aug 02 2018 at 08:02):

Thanks!

view this post on Zulip Kenny Lau (Aug 02 2018 at 08:02):

nice

view this post on Zulip Chris Hughes (Aug 02 2018 at 08:14):

My guess is that perhaps you wanted the add_group axioms to prove some other the other field axioms

view this post on Zulip Kenny Lau (Aug 02 2018 at 08:15):

add group?

view this post on Zulip Chris Hughes (Aug 02 2018 at 08:16):

What's the question?

view this post on Zulip Kenny Lau (Aug 02 2018 at 08:16):

you're replying to the message from March

view this post on Zulip Chris Hughes (Aug 02 2018 at 08:17):

I see.

view this post on Zulip Patrick Massot (Aug 02 2018 at 09:07):

Johan, I think you shouldn't need to directly call unfreeze_local_instances. What are you trying to do?

view this post on Zulip Johan Commelin (Aug 02 2018 at 09:08):

Well, I tried to do the cases cat and it complained... it told me to unfreeze stuff, and I happily complied.

view this post on Zulip Johan Commelin (Aug 02 2018 at 09:09):

I am trying to investigate how far the double op of a category C is from being defeq to C.

view this post on Zulip Patrick Massot (Aug 02 2018 at 09:09):

Do you have a MWE I could try?

view this post on Zulip Johan Commelin (Aug 02 2018 at 09:09):

Hmm, it depends on an old version of Scott's PR...

view this post on Zulip Johan Commelin (Aug 02 2018 at 09:09):

If you have his PR checked out somewhere, I suppose you could copy paste my latest snippet.

view this post on Zulip Johan Commelin (Aug 02 2018 at 09:46):

@Patrick Massot https://github.com/jcommelin/lean-homotopy-theory/blob/playground/src/categories/op_op.lean

view this post on Zulip Johan Commelin (Aug 02 2018 at 09:47):

That's a file in a fork of a project by Reid, depending on an old version of Scott's PR.

view this post on Zulip Kevin Buzzard (Aug 02 2018 at 09:49):

If you're being asked to unfreeze local instances then it's probably because you're doing cases on some random class -- that's when this happens to me. I think the last time it happened, Chris pointed out that I had access to all the things I wanted, with cat.foo, cat.bar etc, so I didn't need to unfreeze anything.

view this post on Zulip Johan Commelin (Aug 02 2018 at 09:51):

Is unfreezing a bad thing to do?

view this post on Zulip Scott Morrison (Aug 02 2018 at 09:55):

Opposite (Opposite C) isn't going to be defeq to C. It's going to be provably equal, or isomorphic, but since we know those are both evil notions, in the end we probably just want to prove it's equivalent. (My intuition is that even proving the equality is just going to invite trouble later, when you rewrite along the equality.)

view this post on Zulip Johan Commelin (Aug 02 2018 at 09:56):

Right. But it's pretty close to being defeq (whatever that means). As expected, there is nothing going into the proofs I just linked to.

view this post on Zulip Kevin Buzzard (Aug 02 2018 at 10:01):

The CS people love stuff being defeq but because categories are one level up in the mathematical hierarchy from sets, it's basically never the right question to ask if they're isomorphic, let alone defeq

view this post on Zulip Johan Commelin (Aug 02 2018 at 10:04):

Sure. But op op is somewhat special right? And I can imagine it would help a lot, in this special case.

view this post on Zulip Mario Carneiro (Aug 04 2018 at 06:30):

I don't think there is any harm in proving an equality of categories when it happens to be true. Of course there should be theorems saying equality implies isomorphism and isomorphism implies equivalence

view this post on Zulip Mario Carneiro (Aug 04 2018 at 06:31):

the main point is to not expect that equality is much stronger or easier to work with than these other two notions

view this post on Zulip Scott Morrison (Aug 04 2018 at 06:31):

I agree. Just don't rewrite the source or target of a functor/natural transformation by an equation of categories and expect to be happy later. :-)

view this post on Zulip Mario Carneiro (Aug 04 2018 at 06:34):

I think one way to handle this is to use a have subproof to show that some equality of categories holds (say an embedded op op cancellation), and then use cast h as a functor and have theorems about it

view this post on Zulip Kevin Buzzard (Aug 04 2018 at 08:16):

I don't think there is any harm in proving an equality of categories when it happens to be true. Of course there should be theorems saying equality implies isomorphism and isomorphism implies equivalence

Maybe the CS experience is different, but it's very rare for categories to be isomorphic in "real life" maths.

view this post on Zulip Mario Carneiro (Aug 04 2018 at 08:16):

I think it's about as common as equality of categories, like in this case


Last updated: May 06 2021 at 21:09 UTC