prod.map vs limits.prod.map

Stream: new members

[Jack J Garzella]

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

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)

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 :=
sorry

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]

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

[Andrew Yang]

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

[Andrew Yang]

It should be

Spoiler

example foo := sorry

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

[Jack J Garzella]

Ok, I ended up proving the lemma! Thanks!

[Adam Topaz]

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

[Jack J Garzella]

@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]

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

[Mario Carneiro]

you should use braces to delimit subgoals instead of comments

[Adam Topaz]

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]

not quite ext1, simp, but close ;)

[Jack J Garzella]

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]

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).