structures

Stream: general

[Kevin Buzzard]

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]

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]

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

[Kenny Lau]

congr or ext

[Johan Commelin]

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

[Kenny Lau]

oh no

[Kenny Lau]

cases cat

[Kenny Lau]

then dsimp

[Johan Commelin]

aha

[Kenny Lau]

I'm not sure because this is not an MWE

[Johan Commelin]

congr failed, and ext did nothing.

[Kenny Lau]

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

[Kenny Lau]

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

[Johan Commelin]

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!

[Johan Commelin]

That worked.

[Johan Commelin]

Thanks!

[Kenny Lau]

nice

[Chris Hughes]

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

[Kenny Lau]

add group?

[Chris Hughes]

What's the question?

[Kenny Lau]

you're replying to the message from March

[Chris Hughes]

I see.

[Patrick Massot]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Patrick Massot]

Do you have a MWE I could try?

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Kevin Buzzard]

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]

Is unfreezing a bad thing to do?

[Scott Morrison]

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]

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]

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]

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

[Mario Carneiro]

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]

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

[Scott Morrison]

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]

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]

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]

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