Missing axioms for various injections into `Object`?

Stream: Analysis I

[Rado Kirov]

I was doing exercise 3.6.6 which asks to prove (a^b) * a^c = a^(b+c) using cardinality theorems, and for b + c I can't just use Fin b and Fin c since they are not disjoint. So I figured to use the cartesian product Fin c \cross Fin 1 which I know has the same cardinality and surely it is disjoint from Fin b.

But I seem to be blanking on how to prove that the object that OrderedPair.toObject produces is different from the one that the Nat_equiv injection from N for Fins produces. I am not even sure if that is provable in the current axiomatization or needs new axioms?

[Terence Tao]

I would instead split Fin (b+c) into a set in bijection with Fin b and a set in bijection with Fin c, using the identifications with Nat.

[Aaron Liu]

This is exactly the kind of nonsense that type theory spares you from. You can try defining a "disjoint union" of sets.

[Terence Tao]

In this custom set theory, perhaps the most natural disjoint union of A:Set and B:Set would be the slices of (A ∪ B) ×ˢ (Fin 2) coming from what is morally A ×ˢ {0} and B ×ˢ {1}. Because no information is provided about how ℕ is actually encoded in the set theory other than that it is an embedding, I don't think one can actually guarantee that Fin b is disjoint from Fin c ×ˢ Fin 1 (cf. the discussion on "junk theorems" in set theory in https://mathoverflow.net/questions/90820/set-theories-without-junk-theorems . Lean also has junk theorems, but they come from a different source, namely defining an operation to be total by assigning junk values to cases where mathematicians would ordinarily leave the operation undefined (e.g., division by zero).)

[Rado Kirov]

I would instead split Fin (b+c) into a set in bijection with Fin b and a set in bijection with Fin c, using the identifications with Nat.

That worked - https://github.com/rkirov/analysis/blob/main/analysis/Analysis/Section_3_6.lean#L2018-L2020, thanks!

[Rado Kirov]

This is exactly the kind of nonsense that type theory spares you from.

Agree, it's nice, but I am also paying for it by having to explicitly work with Subtype theorems. I assume if working in set theory based proof assistants (I haven't ever done that, just thinking by analogy with programming with type systems that have subtyping ) some of that will be more implicit and handled internally. One of my learnings on Lean so far from these exercises is that ↑ is just a visual shortcut, but it is really up to me to always hover over those and know and use the appropriate theorems to manupulate them. A lot of my original confusion was from the fact that ↑ can mean 4 different things in Chapter 3 - subtype.val, nat_equiv, function_to_object, etc. So kinda of 'no free lunch'.

[Aaron Liu]

You can always set_option pp.coercions false and not look at the ↑ at all

[Rado Kirov]

Yeah I was hoping the short syntax means “don’t worry about those”, but I leaned I need to very much understand and think about what’s behind the little arrows :)

[Aaron Liu]

For me I just don't worry about them and it's usually fine

[Aaron Liu]

since I've understood them already I know if it becomes a problem the fix is usually not too hard

[Rado Kirov]

Yeah, I am getting to the point where I have enough tricks in my bag to not be stuck moving around the various casts. What I find dissatisfying is that at the end more than half of the lines of my proofs is messing with the casts and injections, to the point one can hardly see the usually single mathematical idea behind the proof. Once done with the exercises I plan to go back and see whether we are missing some simp lemmas to hide that noise from the proofs (@Dan Abramov has been doing a much better job than me at that), but for now I like to just forge ahead - a proof is a proof.