Zulip Chat Archive

Stream: new members

Topic: rewriting and propositional equalities

Robin Carlier (Jun 26 2021 at 10:35):

Hey, so I have an hypothesis of the form f : x \hom y, for some x y in a category, now I also have some equalities h_x : x = foo and h_y: y = bar, which are propositional equalities rather than definitional (if I understand that distinction well), so that when I try rw h_x at f I end up with a duplicate of f, of the form f : stuff \hom y, if I try to rewrite again it rewrite on that duplicate as well.
Now I also have an hypothesis mono f, but this one don't get duplicated during my rewritings (if I dedup after the rewritings, I have some f_1: foo \hom bar, but still have mono f but no mono f_1. Is there a way to tell Lean to change hypotheses involving f when rewriting like this?

Eric Wieser (Jun 26 2021 at 10:39):

subst h_x may work better

Eric Wieser (Jun 26 2021 at 10:40):

Which means roughly "replace x with foo everywhere"

Eric Wieser (Jun 26 2021 at 10:41):

Your problem is that there are other hypotheses or a goal whose type depends on f, and when you rw ... at f these terms are not also rewritten

Robin Carlier (Jun 26 2021 at 10:45):

Mmh, now that's weird since lean tells me that h_x is not of the form x = t or t = xwhile it clearly is (at least in my example). Thanks for the command subst, which I did not know before, I think that this new issue has to do with my particular setup so I'll think about it a bit!

Robin Carlier (Jun 26 2021 at 10:46):

Mmh alright I see why Lean doesn't like subst in my case, it's because somehow foo depends on x itself

Robin Carlier (Jun 26 2021 at 10:47):

foo is basically of the form h^{-1}(h(x)) for some h, so it can't just replace x everywhere without troubles

Eric Rodriguez (Jun 26 2021 at 11:01):

may not work in this case, but subst is an option you can sometimes try (and the related rintro rfl, etc)

Robin Carlier (Jun 26 2021 at 11:03):

Yeah I'll remember subst anyway, it's quite useful!

Robin Carlier (Jun 26 2021 at 11:11):

So, do you think there's a way out of my situation (where foo depends on x)? Basically I have this f : x \hom y, with hyp mono f, and the same theorem I want already proved for f of the form h(stuff) \hom h(other _stuff), and I simply thought I could say "well just apply it to stuff = h^{-1}(x) and other _stuff = h^{-1}(y)", but runs into problems like this. Sounds like it' just me not really understanding how the lean rewriting works.

Eric Rodriguez (Jun 26 2021 at 11:11):

can you make a #mwe that shows an example of what's going on?

Robin Carlier (Jun 26 2021 at 11:12):

Yup, I'll try, it'll definitely be more clear.

Robin Carlier (Jun 26 2021 at 11:18):

import algebraic_topology.simplex_category

universe variables u
open category_theory

namespace simplex_category

namespace epi_mono

 localized "notation `[`n`]` := simplex_category.mk n" in simplicial

lemma mono_le_card {n m : } {f : [n]  [m]} : (category_theory.mono f)  (n  m) := begin

lemma mono_le_length {x y : simplex_category} {f : x  y} : (category_theory.mono f)  (x.len  y.len) := begin
  set n := x.len with def_n,
  set m := y.len with def_m,
  intro h_f_mono,
  have x_eq_n : x = [n] := by {rw def_n, exact (mk_len x).symm},
  have y_eq_m : y = [m] := by {rw def_m, exact (mk_len y).symm},
  -- subst x_eq_n <- does not work
  -- type_check @mono_le_card n m f <-- Does not type check since f should be [n] ⟶ [m] rather than x ⟶ y
  -- rw x_eq_n at f <- create a duplicate of f, but doesn't get that this dupe will be a mono from h_f_mono.

end epi_mono

end simplex_category

Kevin Buzzard (Jun 26 2021 at 11:33):

Maybe mono_le_card is too weak because it you can only use for objects which are equal to [n] and equality is evil in category theory. mono_le_length is the correct thing to prove and probably it should not be deduced from mono_le_card but done directly. It should follow from stuff which ideally would already be in the API, but who knows. You would want to prove that the category is concrete, that the mono is injective on the underlying types, and that the size of the underlying type of x is equal to x.len, and then it will be a fact from the library.

To deduce mono_le_length from mono_le_card I guess I would try to prove that every x : simplex_category was isomorphic to some [n] because that is not an evil statement.

Probably any comments from people who know more about category theory and this category in general should be taken more seriously than mine. @Scott Morrison @Reid Barton @Bhavik Mehta @Johan Commelin ?

Robin Carlier (Jun 26 2021 at 11:39):

Thanks for your insight. I've already proved that a mono induces an injection on the underlying type, but once again in the case f is from some [m] to some [n], I agree that the right statement is the one about length but somehow I thought going through the more concrete one first would ease the proof (since one of the nice point of the simplex category is there's no non-identity isos), but since the rewriting isn't that easy, I'll probably do as you suggest.

Robin Carlier (Jun 26 2021 at 11:46):

Proving that any x : simplex_categoryis iso to some [n] shouldn't be too hard from the fact they're equal, hopefully.

Kevin Buzzard (Jun 26 2021 at 11:53):

My mental model of category theory is that you should be aware that at any moment the developers might replace a category by an equivalent category, so we can't guarantee that any x is equal to an [n], and the result you want should probably be supplied for you in the simplicial set API. But I might be completely wrong about this

Mario Carneiro (Jun 26 2021 at 11:56):

rather than transferring across an equiv, it's usually easier to just modify the original proof to work in the desired generality

Mario Carneiro (Jun 26 2021 at 11:57):

that is, prove mono_le_length first and deduce mono_le_card as a consequence

Robin Carlier (Jun 26 2021 at 12:01):

I'll do that then!

Robin Carlier (Jun 26 2021 at 12:21):

Worked like a charm as you suggested, thanks a lot for the help!

Last updated: Dec 20 2023 at 11:08 UTC