Lean not finding an instance of `category` from a `bundled`

Stream: general

[Jack Crawford]

I'm having a small spot of trouble constructing an instance of a category. We covered the Eilenberg-Steenrod axioms in my Algebraic Topology class earlier today and I wanted to have a crack at them. I've been fiddling around trying to define the category of topological pairs, and after a few messier attempts decided to try mimicking the approach from topology.category.Top.basic.

I've defined a class topological_pair (α : Type u) extends topological_space α := (subset : set α), @[reducible] def Pairs : Type (u+1) := bundled topological_pair , and even an instance concrete_category_pair_map : unbundled_hom @pair_map, but then on the subsequent few lines it seems that Lean is still failing to find an instance of category Pairs (and has_hom Pairs, and category_struct Pairs), although I was under the impression that it was supposed to be able to infer this from its definition as a bundled topological_pair (there is an instance : category (bundled c) in category_theory.concrete_category.bundled_hom, which I have imported). Lean seems to have no trouble finding an instance of category Top just fine in topology.category.Top.basic, which has a near-identical setup, so I'm not sure where I'm going wrong.

I've been fiddling with things for the last hour trying to fix this -- what am I misunderstanding?

The errors are the -- TODO lines in this teeny file: https://github.com/jjcrawford/leanprover_experiments/blob/master/src/Eilenberg-Steenrod.lean

[Johan Commelin]

First thought: use embedding

[Johan Commelin]

You probably don't want to tie yourself down to subsets

[Jack Crawford]

Thanks, this seems like good advice! I didn't know about embedding, and set just seemed sufficient for a first attempt (I expected to probably have to re-engineer it a few times later anyway). I'll try rewriting it in terms of embedding soon.

[Kevin Buzzard]

Another thought -- if you use embedding (and I like Johan think it's a good idea) then your pair_map could be a structure consisting of a map alpha->beta (why not just use regular maths notation like X and Y for this regular maths stuff?) and also a map U -> V for the two subsets plus a proof that the diagram commutes.

[Kevin Buzzard]

As for the category theory stuff, I was hoping I could make some quick useful comment but I've never used categories seriously before so I can't. I can tell you what the error is though -- I think. As far as I can see Pairs is just some random type, I am not sure if it has a category structure, so when you start using the category theory arrows Lean doesn't know what to do with them.

[Jack Crawford]

^ yeah, this is definitely the case. I'm just not sure why Lean can't see the instance : category (bundled c) from category_theory.concrete_category.bundled_hom, since my Pairs is defined as a bundled topological_pair (and is even @[reducible]).

[Jack Crawford]

The category structure should come for free, at least, this is how it seemed to work for the definition of Top

[Jack Crawford]

@Scott Morrison Could I bother you to have a quick look and see if you can identify why this isn't working?

[Keeley Hoek]

puts on Scott voice I think you need a topological_space instance for topological_pairs

[Scott Morrison]

No, it's that you've written Type instead of Type u in a few places.

[Jack Crawford]

oh! I was wondering whether it might have to be some silly universe thing that was eluding me, thanks!

[Jack Crawford]

That absolutely did the job. I'll have to keep track of my Types a little more closely.

[Scott Morrison]

You had only described the morphisms in the special case of pairs in the actual universe, but then you wanted to talk about the category of pairs in some ridiculous imaginary universe. One solution to this is to only use universe variables when you need to... (which might include contributing to mathlib, where you never know if someone will later want to use ridiculous universes. :-)

[Scott Morrison]

The other solution is to get in the habit of using arbitrary universes from the beginning.

[Jack Crawford]

Maybe the next time I have a problem I'll just use the chaotic evil Type _ ;~)

[Reid Barton]

I think this class topological_pair (α : Type u) extends topological_space α := (subset : set α) is going to be too weird to use in practice. This is like saying: $X$ is a topological pair if it's a topological space and also it has some distinguished subset $A$. But when you want to state the axioms you're going to need to consider the same space $X$ with two different subspaces and it will be awkward to express.

[Reid Barton]

It's probably better to define a structure like https://github.com/rwbarton/lean-homotopy-theory/blob/lean-3.4.2/src/homotopy_theory/topological_spaces/pair.lean#L22 (or you can use embeddings if you like) and construct the category instance manually

[Reid Barton]

Also, you probably want to use AddCommGroup not CommGroup