No arrow between distinct objects in DiscreteCategory

Stream: Is there code for X?

[Yiming Xu]

Is there a theorem saying there is no arrow between distinct objects in a discrete category? I would like to use it to kill the following subgoal:

M : Type u
inst✝ : Monoid M
X Y : Action (Type u) (MonCat.of Mᵐᵒᵖ)
p : X.V × Y.V
f : { as := WalkingPair.right } ⟶ { as := WalkingPair.left }
⊢ p.1 = ((pair X Y).map f).hom p.2

WalkingPair.right is clearly distinct from WalkingPair.left because they are the two constructors of the type WalkingPair.
I will be even happier if you tell me the best way to kill this subgoal.

[Junyan Xu]

Try cases f? Or post your code with imports.

[Yiming Xu]

cases f gives me something I do not know. Let me take 5 min to tidy it and post the code. (Code below to be copied and pasted.)

[Yiming Xu]

import Mathlib

import Mathlib.Algebra.Category.Grp.Basic
import Mathlib.CategoryTheory.SingleObj
import Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
import Mathlib.CategoryTheory.Limits.Preserves.Basic
import Mathlib.CategoryTheory.Adjunction.Limits
import Mathlib.CategoryTheory.Conj
set_option autoImplicit false
set_option diagnostics true
open CategoryTheory Limits
open MonoidalCategory
universe u
variable {M : Type u} [Monoid M]





def ActionEndfun' (X : Action (Type u) (MonCat.of (MulOpposite M)))
         (Y: Action (Type u) (MonCat.of (MulOpposite M)))
         (m : MulOpposite M): End (X.V × Y.V) := fun
           | .mk fst snd => ⟨ (X.ρ m) fst,Y.ρ m snd⟩


theorem ActionEndfun'_def (X : Action (Type u) (MonCat.of (MulOpposite M)))
         (Y: Action (Type u) (MonCat.of (MulOpposite M)))
         (m : MulOpposite M) (p : X.V × Y.V) :
          ActionEndfun' X Y m p = ⟨ (X.ρ m) p.fst,Y.ρ m p.snd⟩ := by rfl




def PairwiseV (X : Action (Type u) (MonCat.of (MulOpposite M)))
         (Y: Action (Type u) (MonCat.of (MulOpposite M))) := X.V × Y.V

theorem PairwiseV_def (X : Action (Type u) (MonCat.of (MulOpposite M)))
         (Y: Action (Type u) (MonCat.of (MulOpposite M))) :
        (PairwiseV X Y) = (X.V × Y.V) := rfl

instance PairwiseAction (X : Action (Type u) (MonCat.of (MulOpposite M)))
         (Y: Action (Type u) (MonCat.of (MulOpposite M))) :
        Action (Type u) (MonCat.of (MulOpposite M)) where
          V := PairwiseV X Y --makes sense since they are actions on a universe
          ρ := {
            toFun := fun opm => ActionEndfun' X Y opm
            map_one' := by
              simp
              funext ⟨x,y⟩
              simp[ActionEndfun'_def X Y 1]
            map_mul' := by
              intros x y
              simp
              apply funext
              intro p
              cases' p with x1 y1
              simp[ActionEndfun'_def X Y (x * y) (x1, y1)]
              rw [CategoryTheory.End.mul_def]
              rw [CategoryTheory.End.mul_def]
              simp
              simp[ActionEndfun'_def]
          }

theorem PairwiseV_def' (X : Action (Type u) (MonCat.of (MulOpposite M)))
         (Y: Action (Type u) (MonCat.of (MulOpposite M))) :
        (PairwiseAction X Y).V = (X.V × Y.V) := rfl




instance (X : Action (Type u) (MonCat.of (MulOpposite M)))
         (Y : Action (Type u) (MonCat.of (MulOpposite M))):
         Limits.LimitCone (Limits.pair X Y) where
           cone := {
             pt := PairwiseAction X Y
             π := {
               app := fun
                 | .mk as =>
                    match as with
                    | WalkingPair.left => {
                      hom := fun
                        | .mk fst snd => fst
                    }
                    | WalkingPair.right => {
                      hom := fun
                        | .mk fst snd => snd
                    }
               naturality := by
                simp
                intros l r f
                ext p
                dsimp [PairwiseV_def' X Y] at p
                --rw [PairwiseV_def' X Y] at p
                --rw [show ((PairwiseAction X Y).V = (X.V × Y.V)) by rfl] at p
                --rw [PairwiseV_def X Y] at p
                cases' r with as
                cases' as
                simp
                cases' l with as
                cases' as
                · dsimp
              -- have a : f = 𝟙 ({ as := WalkingPair.left }: Discrete WalkingPair) := rfl
                  have a : f = 𝟙 (Discrete.mk WalkingPair.left) := rfl
                  simp[a]
                · dsimp
                  sorry
                · cases' p with x y
                  cases' l with as
                  cases as
                  · sorry
                  · dsimp
                    have a : f = 𝟙 (Discrete.mk WalkingPair.right) := rfl
                    simp[a]
             }
           }
           isLimit := {
             lift := sorry
             fac := sorry
             uniq := sorry
           }

[Yiming Xu]

The problem happens between the lines:

· dsimp
                  sorry
                · cases' p with x y
                  cases' l with as
                  cases as
                  · sorry
                  · dsimp
                    have a : f = 𝟙 (Discrete.mk WalkingPair.right) := rfl
                    simp[a]

[Yiming Xu]

That are the sorries.

[Yiming Xu]

If I try:

cases' f with d
simp at d

Lean gives me:

M : Type u
inst✝ : Monoid M
X Y : Action (Type u) (MonCat.of Mᵐᵒᵖ)
p : X.V × Y.V
d✝ : PLift ({ as := WalkingPair.right }.as = { as := WalkingPair.left }.as)
d : PLift False
⊢ p.1 = ((pair X Y).map { down := d✝ }).hom p.2

[Yiming Xu]

In particular it keeps the d✝ and gives a new d, instead of replacing it.

[Yiming Xu]

I am confused. Why does the simplification give a Plift term?
I find the page https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#PLift
But I failed to find a documentation on how to use Plift terms.

[Mario Carneiro]

try nomatch f

[Mario Carneiro]

d is an empty type (it's a wrapper around False)

[Mario Carneiro]

so you are two cases away from finishing there, and nomatch will do all of them at once

[Yiming Xu]

Mario Carneiro said:

try nomatch f

Thanks! I confirm that this solves both of the goals! According to https://leanprover-community.github.io/mathlib4_docs/Lean/Parser/Term.html#Lean.Parser.Term.nomatch, I guess the tactic is trying to convince Lean that there is no constructor of terms of the that type.