## Stream: general

### Topic: structures

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

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


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

#### Kenny Lau (Aug 02 2018 at 07:58):

congr or ext

#### Johan Commelin (Aug 02 2018 at 07:59):

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

oh no

#### Kenny Lau (Aug 02 2018 at 07:59):

cases cat

#### Kenny Lau (Aug 02 2018 at 07:59):

then dsimp

aha

#### Kenny Lau (Aug 02 2018 at 07:59):

I'm not sure because this is not an MWE

#### Johan Commelin (Aug 02 2018 at 07:59):

congr failed, and ext did nothing.

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

#### Kenny Lau (Aug 02 2018 at 08:00):

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

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


That worked.

Thanks!

nice

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

#### Chris Hughes (Aug 02 2018 at 08:16):

What's the question?

#### Kenny Lau (Aug 02 2018 at 08:16):

you're replying to the message from March

I see.

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

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

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

#### Patrick Massot (Aug 02 2018 at 09:09):

Do you have a MWE I could try?

#### Johan Commelin (Aug 02 2018 at 09:09):

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

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

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

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

#### Johan Commelin (Aug 02 2018 at 09:51):

Is unfreezing a bad thing to do?

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

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

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

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

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

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

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

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

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

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