[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
⊢ Category.{?u.2036, u₁} (Skeleton C)
[PROOFSTEP]
apply InducedCategory.category
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
⊢ Full (fromSkeleton C)
[PROOFSTEP]
apply InducedCategory.full
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
⊢ Faithful (fromSkeleton C)
[PROOFSTEP]
apply InducedCategory.faithful
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
⊢ Skeletal (Skeleton C)
[PROOFSTEP]
rintro X Y ⟨h⟩
[GOAL]
case intro
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
X Y : Skeleton C
h : X ≅ Y
⊢ X = Y
[PROOFSTEP]
have : X.out ≈ Y.out := ⟨(fromSkeleton C).mapIso h⟩
[GOAL]
case intro
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
X Y : Skeleton C
h : X ≅ Y
this : Quotient.out X ≈ Quotient.out Y
⊢ X = Y
[PROOFSTEP]
simpa using Quotient.sound this
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
⊢ ∀ (a₁ b₁ a₂ b₂ : C), a₁ ≈ a₂ → b₁ ≈ b₂ → (fun X Y => Nonempty (X ⟶ Y)) a₁ b₁ = (fun X Y => Nonempty (X ⟶ Y)) a₂ b₂
[PROOFSTEP]
rintro _ _ _ _ ⟨i₁⟩ ⟨i₂⟩
[GOAL]
case intro.intro
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
a₁✝ b₁✝ a₂✝ b₂✝ : C
i₁ : a₁✝ ≅ a₂✝
i₂ : b₁✝ ≅ b₂✝
⊢ (fun X Y => Nonempty (X ⟶ Y)) a₁✝ b₁✝ = (fun X Y => Nonempty (X ⟶ Y)) a₂✝ b₂✝
[PROOFSTEP]
exact propext ⟨Nonempty.map fun f => i₁.inv ≫ f ≫ i₂.hom, Nonempty.map fun f => i₁.hom ≫ f ≫ i₂.inv⟩
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
⊢ ∀ (a : ThinSkeleton C), a ≤ a
[PROOFSTEP]
refine' Quotient.ind fun a => _
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
a : C
⊢ Quotient.mk (isIsomorphicSetoid C) a ≤ Quotient.mk (isIsomorphicSetoid C) a
[PROOFSTEP]
exact ⟨𝟙 _⟩
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
x✝¹ x✝ : ThinSkeleton C
⊢ ∀ (a b : x✝¹ ⟶ x✝), a = b
[PROOFSTEP]
rintro ⟨⟨f₁⟩⟩ ⟨⟨_⟩⟩
[GOAL]
case up.up.up.up
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
x✝¹ x✝ : ThinSkeleton C
f₁ down✝ : x✝¹ ≤ x✝
⊢ { down := { down := f₁ } } = { down := { down := down✝ } }
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Quiver.IsThin C
src✝ : Preorder (ThinSkeleton C) := preorder C
⊢ ∀ (a b : C),
    Quotient.mk (isIsomorphicSetoid C) a ≤ Quotient.mk (isIsomorphicSetoid C) b →
      Quotient.mk (isIsomorphicSetoid C) b ≤ Quotient.mk (isIsomorphicSetoid C) a →
        Quotient.mk (isIsomorphicSetoid C) a = Quotient.mk (isIsomorphicSetoid C) b
[PROOFSTEP]
rintro _ _ ⟨f⟩ ⟨g⟩
[GOAL]
case intro.intro
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Quiver.IsThin C
src✝ : Preorder (ThinSkeleton C) := preorder C
a✝ b✝ : C
f : a✝ ⟶ b✝
g : b✝ ⟶ a✝
⊢ Quotient.mk (isIsomorphicSetoid C) a✝ = Quotient.mk (isIsomorphicSetoid C) b✝
[PROOFSTEP]
apply Quotient.sound (equiv_of_both_ways f g)
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
R : D ⥤ C
L : C ⥤ D
h : L ⊣ R
X : ThinSkeleton C
⊢ (𝟭 (ThinSkeleton C)).obj X ⟶ (map L ⋙ map R).obj X
[PROOFSTEP]
letI := isIsomorphicSetoid C
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
R : D ⥤ C
L : C ⥤ D
h : L ⊣ R
X : ThinSkeleton C
this : Setoid C := isIsomorphicSetoid C
⊢ (𝟭 (ThinSkeleton C)).obj X ⟶ (map L ⋙ map R).obj X
[PROOFSTEP]
refine' Quotient.recOnSubsingleton X fun x => homOfLE ⟨h.unit.app x⟩
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
R : D ⥤ C
L : C ⥤ D
h : L ⊣ R
X : ThinSkeleton D
⊢ (map R ⋙ map L).obj X ⟶ (𝟭 (ThinSkeleton D)).obj X
[PROOFSTEP]
letI := isIsomorphicSetoid D
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
R : D ⥤ C
L : C ⥤ D
h : L ⊣ R
X : ThinSkeleton D
this : Setoid D := isIsomorphicSetoid D
⊢ (map R ⋙ map L).obj X ⟶ (𝟭 (ThinSkeleton D)).obj X
[PROOFSTEP]
refine' Quotient.recOnSubsingleton X fun x => homOfLE ⟨h.counit.app x⟩
