Iso.lean autoParam Question

Stream: mathlib4

[Mason McBride]

import Mathlib.CategoryTheory.Category.Basic
import Mathlib.CategoryTheory.Iso

open CategoryTheory
variable {C : Type*} [Category C]

class Initial (i : C) :=
(unique : ∀ {c : C} (α β : i ⟶ c), α = β)

theorem exercise_10 {i i' : C} [Initial i] [Initial i'] (i_end: i⟶i) (i'_end: i'⟶i')
(h1: i_end = 𝟙 i) (h2: i'_end = 𝟙 i') (a : i⟶i') (b: i'⟶i)
: Iso i i' := by
  constructor

In this example, I am trying to prove there is an isomorphism between the two objects but when I use constructor there is this autoParam (?hom ≫ ?inv = 𝟙 i) _auto✝ goal that gets created and I don't know what this is saying? What do I have to do?

[Kyle Miller]

First, when defining data, if you want to do it in tactic mode it's usually fconstructor is better since it doesn't reorder the goals.

The autoParam corresponds to fields that Lean will try to solve using a tactic. You can ignore everything but the ?hom ≫ ?inv = 𝟙 i (unfold autoParam removes it completely).

But, I would use a where to define the data.

def exercise_10 {i i' : C} [Initial i] [Initial i'] (i_end: i⟶i) (i'_end: i'⟶i')
(h1: i_end = 𝟙 i) (h2: i'_end = 𝟙 i') (a : i⟶i') (b: i'⟶i)
: Iso i i' where
  hom := sorry
  inv := sorry
  hom_inv_id := sorry
  inv_hom_id := sorry

(Notice also, def instead of theorem since an Iso is data, not a proof.)

[Kyle Miller]

You can generate that by putting := _ where that where was. Then a blue lightbulb pops up in VS Code for a code action, and you can do "generate maximal skeleton".

Once you define hom and inv, you can try your luck and delete the remaining fields to see if that auto-param tactic will auto-solve them.

[Mason McBride]

Thanks, it was not able to solve it automatically because aesop couldn't figure out that a \gg b = i_end and b \gg a = i'_end. Maybe if I defined by exercise better it could or maybe this proof is necessary to prove that i and i' are isomoprhic

[Richard Copley]

This doesn't make a real difference, but there is no need for the new names i_end and i'_end: you can just call those entities by their existing names 𝟙 i and 𝟙 i'.

[Notification Bot]

A message was moved here from #mathlib4 > synthesis failure on non-preferred parent by Richard Copley.

[Mason McBride]

I thought that i \hom i was not necessarily the identity morphism (but it is a left identity) so I made those hypotheses what do you think

[Richard Copley]

The following seems equally expressive to me, and it is solvable in the same way.

def exercise_10 {i i' : C} [Initial i] [Initial i']
    (a : i ⟶ i') (b: i' ⟶ i) :
    Iso i i' where

[Mason McBride]

variable {C : Type*} [Category C]

class Initial (i : C) :=
(unique : ∀ {c : C} (α β : i ⟶ c), α = β)

namespace exercise_10

variable {i i' : C} (i_end: i⟶i) (i'_end: i'⟶i') (a : i⟶i') (b: i'⟶i)
theorem exercise_10  [Initial i] [Initial i'] : Iso i i' := by
  fconstructor
  exact a
  exact b
  unfold autoParam; exact Initial.unique (a ≫ b) (𝟙 i)
  unfold autoParam; exact Initial.unique (b ≫ a) (𝟙 i')

end exercise_10

[Richard Copley]

Note that i_end and i'_end are unused.

[Mason McBride]

so you only have to assume there is a map between i and i'

[Kim Morrison]

I would say your definition of Initial is wrong: it needs to assert existence as well as uniqueness.

[Mason McBride]

variable {C : Type*} [Category C]

class Initial (i : C) :=
(to : (c : C), f: i⟶c)
(unique : ∀ {c : C} (α β : i ⟶ c), α = β)

I agree with you. I want something like to that gives a hom between the object I give it and i. Do you knokw how?

[Kim Morrison]

import Mathlib

set_option autoImplicit true

open CategoryTheory Limits

namespace exercise_10

variable [Category C] {X Y : C}

def exercise_10 (hX : IsInitial X) (hY : IsInitial Y) : Iso X Y where
hom := hX.to Y
inv := hY.to X

end exercise_10

[Mason McBride]

I'm trying to find where IsInitial.to is defined in Mathlib, but I can't

[Matt Diamond]

docs#CategoryTheory.Limits.IsInitial.to

[Kim Morrison]

You should just be able to press F12 with you cursor on the to?

[Mason McBride]

Ah, I clicked into the Cocone thank you

[Mason McBride]

Is there any way to define in my way without a cocone? I don't know what a cocone is yet

[Mason McBride]

import Mathlib.CategoryTheory.Category.Basic
import Mathlib.CategoryTheory.Iso
import Mathlib.CategoryTheory.Limits.Shapes.Terminal

open CategoryTheory
open CategoryTheory Limits
variable {C : Type*} [Category C]
namespace exercise_9_and_10

variable {i i' c : C}
theorem exercise_9 (hi: IsInitial i) (l : i ⟶ i) (α : i ⟶ c)
: l ≫ α = α := by exact hi.hom_ext (l ≫ α) α

def exercise_10  (hi:IsInitial i) (hi':IsInitial i') : Iso i i' where
  hom := hi.to i'
  inv := hi'.to i

end exercise_9_and_10