rewriting and propositional equalities

Stream: new members

[Robin Carlier]

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]

subst h_x may work better

[Eric Wieser]

Which means roughly "replace x with foo everywhere"

[Eric Wieser]

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]

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]

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

[Robin Carlier]

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]

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

[Robin Carlier]

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

[Robin Carlier]

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]

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

[Robin Carlier]

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

[Robin Carlier]

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
  sorry,
end

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

end epi_mono

end simplex_category

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

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]

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

[Mario Carneiro]

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

[Robin Carlier]

I'll do that then!

[Robin Carlier]

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