Stream: new members

Topic: prod.map vs limits.prod.map

Jack J Garzella (Aug 02 2022 at 18:01):

Hello, I am yet again working on the thing discussed in #maths > Definition of presheaf of modules, and I believe I have reduced (a chunk of) the problem to showing a statement like the following:

MWE Lemma statement

I don't really know how one would go about comparing prod.map and limits.prod.map, does anyone know how to prove such at thing?

Jack J Garzella (Aug 02 2022 at 18:07):

Hmm, it seems I could also use advice on how to get code to properly highlight in a spoiler, if anyone knows.

Andrew Yang (Aug 02 2022 at 18:07):

I think ext1 could help? Or maybe docs#category_theory.limits.prod.hom_ext if ext found the wrong lemma.

Andrew Yang (Aug 02 2022 at 18:09):

It should be

Spoiler

You can click the view source on the top right to see how I wrote it.

Jack J Garzella (Aug 02 2022 at 19:25):

Ok, I ended up proving the lemma! Thanks!

Adam Topaz (Aug 02 2022 at 19:32):

I suspect by {ext1, simp} should close the goal. If not, then there are some simp lemmas missing.

Jack J Garzella (Aug 04 2022 at 01:09):

@Adam Topaz turns out, by {ext1, simp} does not close it. I don't quite know how ext1 works, but it seems to focus on the first, goal, and since there are two (one for each projection), it doesn't seem to work. There also seem to be some lemmas missing, simp doesn't even close the first goal.

Jack J Garzella (Aug 04 2022 at 01:11):

By using the strategy of "write a bunch of have statements that can be cleared by simp, and then use simp? to turn them into things of the form conv_lhs { simp only [...] }, I was able to come up with the following:

lemma prod_map_bpo_commutes (A B C D : Type u) (f : A ⟶ C) (g : B ⟶ D) :
as_hom (prod.map f g) ≫
(binary_product_iso C D).inv =
(binary_product_iso A B).inv ≫
limits.prod.map f g :=
begin
apply category_theory.limits.prod.hom_ext,
-- prod.fst, goal 1
apply funext, intros x,
conv_lhs {
simp only [category_theory.types_comp_apply,
category_theory.limits.types.binary_product_iso_inv_comp_fst_apply],
},
conv_rhs {
simp only [category_theory.limits.prod.map_fst,
category_theory.iso.cancel_iso_inv_left,
eq_self_iff_true,
category_theory.category.assoc],
simp only [category_theory.types_comp_apply,
eq_self_iff_true,
category_theory.limits.types.binary_product_iso_inv_comp_fst_apply]
},
refl,
-- prod.snd, goal 2
apply funext, intros x,
conv_lhs {
simp only [category_theory.types_comp_apply,
category_theory.limits.types.binary_product_iso_inv_comp_snd_apply],
},
conv_rhs {
simp only [category_theory.limits.prod.map_snd,
category_theory.iso.cancel_iso_inv_left,
eq_self_iff_true,
category_theory.category.assoc],
simp only [category_theory.types_comp_apply,
eq_self_iff_true,
category_theory.limits.types.binary_product_iso_inv_comp_snd_apply]
},
refl,
end


Adam Topaz (Aug 04 2022 at 01:46):

import category_theory.closed.cartesian
import category_theory.limits.types
import category_theory.limits.shapes.types
import category_theory.types

noncomputable theory

universes u v

open category_theory
-- open category_theory.limits
open category_theory.limits.types
open category_theory.concrete_category

instance : monoidal_category (Type u) :=
monoidal_of_has_finite_products (Type u)

@[simp, reassoc]
lemma fst_foo (A B : Type u) :
(binary_product_iso A B).inv ≫ limits.prod.fst = prod.fst :=
limits.prod.lift_fst _ _

@[simp, reassoc]
lemma snd_foo (A B : Type u) :
(binary_product_iso A B).inv ≫ limits.prod.snd = prod.snd :=
limits.prod.lift_snd _ _

lemma prod_map_bpo_commutes (A B C D : Type u) (f : A ⟶ C) (g : B ⟶ D) :
as_hom (prod.map f g) ≫
(binary_product_iso C D).inv =
(binary_product_iso A B).inv ≫
limits.prod.map f g :=
by { ext1; simpa }


Adam Topaz (Aug 04 2022 at 01:46):

not quite ext1, simp, but close ;)

Jack J Garzella (Aug 04 2022 at 04:53):

When I change the final semicolon to a comma, Lean complains because there are two goals and only the first one gets solved. Can you explain why simp works when there is a semicolon, but if I change that to a comma it complains?

Jireh Loreaux (Aug 04 2022 at 05:03):

A semicolon means: apply the next tactic to all the goals. So, in your case, the tactic after the semicolon solves both goals, but when you change it to a comma, that last tactic only acts on the 1st goal (it solves it, but there's still one leftover).

Last updated: Dec 20 2023 at 11:08 UTC