Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl.
/-
Copyright (c) 2018 Scott Morrison. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Scott Morrison

! This file was ported from Lean 3 source module category_theory.functor.fully_faithful
! leanprover-community/mathlib commit 70d50ecfd4900dd6d328da39ab7ebd516abe4025
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.CategoryTheory.NatIso
import Mathlib.Logic.Equiv.Defs

/-!
# Full and faithful functors

We define typeclasses `Full` and `Faithful`, decorating functors.

## Main definitions and results
* Use `F.map_injective` to retrieve the fact that `F.map` is injective when `[Faithful F]`.
* Similarly, `F.map_surjective` states that `F.map` is surjective when `[Full F]`.
* Use `F.preimage` to obtain preimages of morphisms when `[Full F]`.
* We prove some basic "cancellation" lemmas for full and/or faithful functors, as well as a
  construction for "dividing" a functor by a faithful functor, see `Faithful.div`.
* `Full F` carries data, so definitional properties of the preimage can be used when using
  `F.preimage`. To obtain an instance of `Full F` non-constructively, you can use `fullOfExists`
  and `fullOfSurjective`.

See `CategoryTheory.Equivalence.of_fullyFaithful_ess_surj` for the fact that a functor is an
equivalence if and only if it is fully faithful and essentially surjective.

-/


-- declare the `v`'s first; see `CategoryTheory.Category` for an explanation
universe v₁ v₂ v₃ u₁ u₂ u₃

namespace CategoryTheory

variable {
C: Type u₁
C
:
Type u₁: Type (u₁+1)
Type u₁
} [
Category: Type ?u.4 → Type (max?u.4(v₁+1))
Category
.{v₁}
C: Type u₁
C
] {
D: Type u₂
D
:
Type u₂: Type (u₂+1)
Type u₂
} [
Category: Type ?u.9 → Type (max?u.9(v₂+1))
Category
.{v₂}
D: Type u₂
D
] /-- A functor `F : C ⥤ D` is full if for each `X Y : C`, `F.map` is surjective. In fact, we use a constructive definition, so the `Full F` typeclass contains data, specifying a particular preimage of each `f : F.obj X ⟶ F.obj Y`. See . -/ class
Full: {C : Type u₁} → [inst : Category C] → {D : Type u₂} → [inst_1 : Category D] → {F : C ⥤ D} → (preimage : {X Y : C} → (F.obj X ⟶ F.obj Y) → (X ⟶ Y)) → autoParam (∀ {X Y : C} (f : F.obj X ⟶ F.obj Y), F.map (preimage f) = f) _auto✝ → Full F
Full
(
F: C ⥤ D
F
:
C: Type u₁
C
⥤
D: Type u₂
D
) where /-- The data of a preimage for every `f : F.obj X ⟶ F.obj Y`. -/
preimage: {C : Type u₁} → [inst : Category C] → {D : Type u₂} → [inst_1 : Category D] → {F : C ⥤ D} → [self : Full F] → {X Y : C} → (F.obj X ⟶ F.obj Y) → (X ⟶ Y)
preimage
: ∀ {
X: C
X
Y: C
Y
:
C: Type u₁
C
} (
_: F.obj X ⟶ F.obj Y
_
:
F: C ⥤ D
F
.
obj: {V : Type ?u.132} → [inst : Quiver V] → {W : Type ?u.131} → [inst_1 : Quiver W] → V ⥤q W → V → W
obj
X: C
X
⟶
F: C ⥤ D
F
.
obj: {V : Type ?u.182} → [inst : Quiver V] → {W : Type ?u.181} → [inst_1 : Quiver W] → V ⥤q W → V → W
obj
Y: C
Y
),
X: C
X
⟶
Y: C
Y
/-- The property that `Full.preimage f` of maps to `f` via `F.map`. -/
witness: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {F : C ⥤ D} [self : Full F] {X Y : C} (f : F.obj X ⟶ F.obj Y), F.map (Full.preimage f) = f
witness
: ∀ {
X: C
X
Y: C
Y
:
C: Type u₁
C
} (
f: F.obj X ⟶ F.obj Y
f
:
F: C ⥤ D
F
.
obj: {V : Type ?u.276} → [inst : Quiver V] → {W : Type ?u.275} → [inst_1 : Quiver W] → V ⥤q W → V → W
obj
X: C
X
⟶
F: C ⥤ D
F
.
obj: {V : Type ?u.296} → [inst : Quiver V] → {W : Type ?u.295} → [inst_1 : Quiver W] → V ⥤q W → V → W
obj
Y: C
Y
),
F: C ⥤ D
F
.
map: {V : Type ?u.336} → [inst : Quiver V] → {W : Type ?u.335} → [inst_1 : Quiver W] → (self : V ⥤q W) → {X Y : V} → (X ⟶ Y) → (self.obj X ⟶ self.obj Y)
map
(
preimage: {X Y : C} → (F.obj X ⟶ F.obj Y) → (X ⟶ Y)
preimage
f: F.obj X ⟶ F.obj Y
f
) =
f: F.obj X ⟶ F.obj Y
f
:= by aesop_cat #align category_theory.full
CategoryTheory.Full: {C : Type u₁} → [inst : Category C] → {D : Type u₂} → [inst_1 : Category D] → C ⥤ D → Type (max(maxu₁v₁)v₂)
CategoryTheory.Full
#align category_theory.full.witness
CategoryTheory.Full.witness: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {F : C ⥤ D} [self : Full F] {X Y : C} (f : F.obj X ⟶ F.obj Y), F.map (Full.preimage f) = f
CategoryTheory.Full.witness
attribute [simp]
Full.witness: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {F : C ⥤ D} [self : Full F] {X Y : C} (f : F.obj X ⟶ F.obj Y), F.map (Full.preimage f) = f
Full.witness
/- ./././Mathport/Syntax/Translate/Command.lean:379:30: infer kinds are unsupported in Lean 4: #[`map_injective'] [] -/ /-- A functor `F : C ⥤ D` is faithful if for each `X Y : C`, `F.map` is injective. See . -/ class
Faithful: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {F : C ⥤ D}, autoParam (∀ {X Y : C}, Function.Injective F.map) _auto✝ → Faithful F
Faithful
(
F: C ⥤ D
F
:
C: Type u₁
C
⥤
D: Type u₂
D
) :
Prop: Type
Prop
where /-- `F.map` is injective for each `X Y : C`. -/
map_injective: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {F : C ⥤ D} [self : Faithful F] {X Y : C}, Function.Injective F.map
map_injective
: ∀ {
X: C
X
Y: C
Y
:
C: Type u₁
C
},
Function.Injective: {α : Sort ?u.497} → {β : Sort ?u.496} → (α → β) → Prop
Function.Injective
(
F: C ⥤ D
F
.
map: {V : Type ?u.654} → [inst : Quiver V] → {W : Type ?u.653} → [inst_1 : Quiver W] → (self : V ⥤q W) → {X Y : V} → (X ⟶ Y) → (self.obj X ⟶ self.obj Y)
map
: (
X: C
X
⟶
Y: C
Y
) → (
F: C ⥤ D
F
.
obj: {V : Type ?u.567} → [inst : Quiver V] → {W : Type ?u.566} → [inst_1 : Quiver W] → V ⥤q W → V → W
obj
X: C
X
⟶
F: C ⥤ D
F
.
obj: {V : Type ?u.616} → [inst : Quiver V] → {W : Type ?u.615} → [inst_1 : Quiver W] → V ⥤q W → V → W
obj
Y: C
Y
)) := by aesop_cat #align category_theory.faithful
CategoryTheory.Faithful: {C : Type u₁} → [inst : Category C] → {D : Type u₂} → [inst_1 : Category D] → C ⥤ D → Prop
CategoryTheory.Faithful
#align category_theory.faithful.map_injective
CategoryTheory.Faithful.map_injective: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {F : C ⥤ D} [self : Faithful F] {X Y : C}, Function.Injective F.map
CategoryTheory.Faithful.map_injective
namespace Functor variable {
X: C
X
Y: C
Y
:
C: Type u₁
C
} theorem
map_injective: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {X Y : C} (F : C ⥤ D) [inst_2 : Faithful F], Function.Injective F.map
map_injective
(
F: C ⥤ D
F
:
C: Type u₁
C
⥤
D: Type u₂
D
) [
Faithful: {C : Type ?u.734} → [inst : Category C] → {D : Type ?u.733} → [inst_1 : Category D] → C ⥤ D → Prop
Faithful
F: C ⥤ D
F
] :
Function.Injective: {α : Sort ?u.776} → {β : Sort ?u.775} → (α → β) → Prop
Function.Injective
<| (
F: C ⥤ D
F
.
map: {V : Type ?u.925} → [inst : Quiver V] → {W : Type ?u.924} → [inst_1 : Quiver W] → (self : V ⥤q W) → {X Y : V} → (X ⟶ Y) → (self.obj X ⟶ self.obj Y)
map
: (
X: C
X
⟶
Y: C
Y
) → (
F: C ⥤ D
F
.
obj: {V : Type ?u.838} → [inst : Quiver V] → {W : Type ?u.837} → [inst_1 : Quiver W] → V ⥤q W → V → W
obj
X: C
X
⟶
F: C ⥤ D
F
.
obj: {V : Type ?u.887} → [inst : Quiver V] → {W : Type ?u.886} → [inst_1 : Quiver W] → V ⥤q W → V → W
obj
Y: C
Y
)) :=
Faithful.map_injective: ∀ {C : Type ?u.950} [inst : Category C] {D : Type ?u.949} [inst_1 : Category D] {F : C ⥤ D} [self : Faithful F] {X Y : C}, Function.Injective F.map
Faithful.map_injective
#align category_theory.functor.map_injective
CategoryTheory.Functor.map_injective: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {X Y : C} (F : C ⥤ D) [inst_2 : Faithful F], Function.Injective F.map
CategoryTheory.Functor.map_injective
theorem
mapIso_injective: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {X Y : C} (F : C ⥤ D) [inst_2 : Faithful F], Function.Injective F.mapIso
mapIso_injective
(
F: C ⥤ D
F
:
C: Type u₁
C
⥤
D: Type u₂
D
) [
Faithful: {C : Type ?u.1059} → [inst : Category C] → {D : Type ?u.1058} → [inst_1 : Category D] → C ⥤ D → Prop
Faithful
F: C ⥤ D
F
] :
Function.Injective: {α : Sort ?u.1101} → {β : Sort ?u.1100} → (α → β) → Prop
Function.Injective
<| (
F: C ⥤ D
F
.
mapIso: {C : Type ?u.1213} → [inst : Category C] → {D : Type ?u.1212} → [inst_1 : Category D] → (F : C ⥤ D) → {X Y : C} → (X ≅ Y) → (F.obj X ≅ F.obj Y)
mapIso
: (
X: C
X
≅
Y: C
Y
) → (
F: C ⥤ D
F
.
obj: {V : Type ?u.1149} → [inst : Quiver V] → {W : Type ?u.1148} → [inst_1 : Quiver W] → V ⥤q W → V → W
obj
X: C
X
≅
F: C ⥤ D
F
.
obj: {V : Type ?u.1199} → [inst : Quiver V] → {W : Type ?u.1198} → [inst_1 : Quiver W] → V ⥤q W → V → W
obj
Y: C
Y
)) := fun
_: ?m.1249
_
_: ?m.1252
_
h: ?m.1255
h
=>
Iso.ext: ∀ {C : Type ?u.1257} [inst : Category C] {X Y : C} ⦃α β : X ≅ Y⦄, α.hom = β.hom → α = β
Iso.ext
(
map_injective: ∀ {C : Type ?u.1283} [inst : Category C] {D : Type ?u.1282} [inst_1 : Category D] {X Y : C} (F : C ⥤ D) [inst_2 : Faithful F], Function.Injective F.map
map_injective
F: C ⥤ D
F
(
congr_arg: ∀ {α : Sort ?u.1316} {β : Sort ?u.1315} {a₁ a₂ : α} (f : α → β), a₁ = a₂ → f a₁ = f a₂
congr_arg
Iso.hom: {C : Type ?u.1321} → [inst : Category C] → {X Y : C} → (X ≅ Y) → (X ⟶ Y)
Iso.hom
h: ?m.1255
h
:
_: Sort ?u.1313
_
)) #align category_theory.functor.map_iso_injective
CategoryTheory.Functor.mapIso_injective: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {X Y : C} (F : C ⥤ D) [inst_2 : Faithful F], Function.Injective F.mapIso
CategoryTheory.Functor.mapIso_injective
/-- The specified preimage of a morphism under a full functor. -/ def
preimage: {C : Type u₁} → [inst : Category C] → {D : Type u₂} → [inst_1 : Category D] → {X Y : C} → (F : C ⥤ D) → [inst_2 : Full F] → (F.obj X ⟶ F.obj Y) → (X ⟶ Y)
preimage
(
F: C ⥤ D
F
:
C: Type u₁
C
⥤
D: Type u₂
D
) [
Full: {C : Type ?u.1404} → [inst : Category C] → {D : Type ?u.1403} → [inst_1 : Category D] → C ⥤ D → Type (max(max?u.1404?u.1406)?u.1405)
Full
F: C ⥤ D
F
] (
f: F.obj X ⟶ F.obj Y
f
:
F: C ⥤ D
F
.
obj: {V : Type ?u.1470} → [inst : Quiver V] → {W : Type ?u.1469} → [inst_1 : Quiver W] → V ⥤q W → V → W
obj
X: C
X
⟶
F: C ⥤ D
F
.
obj: {V : Type ?u.1520} → [inst : Quiver V] → {W : Type ?u.1519} → [inst_1 : Quiver W] → V ⥤q W → V → W
obj
Y: C
Y
) :
X: C
X
⟶
Y: C
Y
:=
Full.preimage: {C : Type ?u.1587} → [inst : Category C] → {D : Type ?u.1586} → [inst_1 : Category D] → {F : C ⥤ D} → [self : Full F] → {X Y : C} → (F.obj X ⟶ F.obj Y) → (X ⟶ Y)
Full.preimage
.{v₁, v₂}
f: F.obj X ⟶ F.obj Y
f
#align category_theory.functor.preimage
CategoryTheory.Functor.preimage: {C : Type u₁} → [inst : Category C] → {D : Type u₂} → [inst_1 : Category D] → {X Y : C} → (F : C ⥤ D) → [inst_2 : Full F] → (F.obj X ⟶ F.obj Y) → (X ⟶ Y)
CategoryTheory.Functor.preimage
pp_extended_field_notation
preimage: {C : Type u₁} → [inst : Category C] → {D : Type u₂} → [inst_1 : Category D] → {X Y : C} → (F : C ⥤ D) → [inst_2 : Full F] → (F.obj X ⟶ F.obj Y) → (X ⟶ Y)
preimage
@[simp] theorem
image_preimage: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] (F : C ⥤ D) [inst_2 : Full F] {X Y : C} (f : F.obj X ⟶ F.obj Y), F.map (F.preimage f) = f
image_preimage
(
F: C ⥤ D
F
:
C: Type u₁
C
⥤
D: Type u₂
D
) [
Full: {C : Type ?u.9143} → [inst : Category C] → {D : Type ?u.9142} → [inst_1 : Category D] → C ⥤ D → Type (max(max?u.9143?u.9145)?u.9144)
Full
F: C ⥤ D
F
] {
X: C
X
Y: C
Y
:
C: Type u₁
C
} (
f: F.obj X ⟶ F.obj Y
f
:
F: C ⥤ D
F
.
obj: {V : Type ?u.9213} → [inst : Quiver V] → {W : Type ?u.9212} → [inst_1 : Quiver W] → V ⥤q W → V → W
obj
X: C
X
⟶
F: C ⥤ D
F
.
obj: {V : Type ?u.9263} → [inst : Quiver V] → {W : Type ?u.9262} → [inst_1 : Quiver W] → V ⥤q W → V → W
obj
Y: C
Y
) :
F: C ⥤ D
F
.
map: {V : Type ?u.9304} → [inst : Quiver V] → {W : Type ?u.9303} → [inst_1 : Quiver W] → (self : V ⥤q W) → {X Y : V} → (X ⟶ Y) → (self.obj X ⟶ self.obj Y)
map
(
preimage: {C : Type ?u.9316} → [inst : Category C] → {D : Type ?u.9315} → [inst_1 : Category D] → {X Y : C} → (F : C ⥤ D) → [inst_2 : Full F] → (F.obj X ⟶ F.obj Y) → (X ⟶ Y)
preimage
F: C ⥤ D
F
f: F.obj X ⟶ F.obj Y
f
) =
f: F.obj X ⟶ F.obj Y
f
:=

Goals accomplished! 🐙
C: Type u₁

inst✝²: Category C

D: Type u₂

inst✝¹: Category D

X✝, Y✝: C

F: C ⥤ D

inst✝: Full F

X, Y: C

f: F.obj X ⟶ F.obj Y


F.map (F.preimage f) = f
C: Type u₁

inst✝²: Category C

D: Type u₂

inst✝¹: Category D

X✝, Y✝: C

F: C ⥤ D

inst✝: Full F

X, Y: C

f: F.obj X ⟶ F.obj Y


F.map (Full.preimage f) = f
C: Type u₁

inst✝²: Category C

D: Type u₂

inst✝¹: Category D

X✝, Y✝: C

F: C ⥤ D

inst✝: Full F

X, Y: C

f: F.obj X ⟶ F.obj Y


F.map (Full.preimage f) = f
C: Type u₁

inst✝²: Category C

D: Type u₂

inst✝¹: Category D

X✝, Y✝: C

F: C ⥤ D

inst✝: Full F

X, Y: C

f: F.obj X ⟶ F.obj Y


F.map (F.preimage f) = f

Goals accomplished! 🐙
#align category_theory.functor.image_preimage
CategoryTheory.Functor.image_preimage: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] (F : C ⥤ D) [inst_2 : Full F] {X Y : C} (f : F.obj X ⟶ F.obj Y), F.map (F.preimage f) = f
CategoryTheory.Functor.image_preimage
theorem
map_surjective: ∀ (F : C ⥤ D) [inst : Full F], Function.Surjective F.map
map_surjective
(
F: C ⥤ D
F
:
C: Type u₁
C
⥤
D: Type u₂
D
) [
Full: {C : Type ?u.9770} → [inst : Category C] → {D : Type ?u.9769} → [inst_1 : Category D] → C ⥤ D → Type (max(max?u.9770?u.9772)?u.9771)
Full
F: C ⥤ D
F
] :
Function.Surjective: {α : Sort ?u.9812} → {β : Sort ?u.9811} → (α → β) → Prop
Function.Surjective
(
F: C ⥤ D
F
.
map: {V : Type ?u.9961} → [inst : Quiver V] → {W : Type ?u.9960} → [inst_1 : Quiver W] → (self : V ⥤q W) → {X Y : V} → (X ⟶ Y) → (self.obj X ⟶ self.obj Y)
map
: (
X: C
X
⟶
Y: C
Y
) → (
F: C ⥤ D
F
.
obj: {V : Type ?u.9874} → [inst : Quiver V] → {W : Type ?u.9873} → [inst_1 : Quiver W] → V ⥤q W → V → W
obj
X: C
X
⟶
F: C ⥤ D
F
.
obj: {V : Type ?u.9923} → [inst : Quiver V] → {W : Type ?u.9922} → [inst_1 : Quiver W] → V ⥤q W → V → W
obj
Y: C
Y
)) := fun
f: ?m.9987
f
=> ⟨
F: C ⥤ D
F
.
preimage: {C : Type ?u.10002} → [inst : Category C] → {D : Type ?u.10001} → [inst_1 : Category D] → {X Y : C} → (F : C ⥤ D) → [inst_2 : Full F] → (F.obj X ⟶ F.obj Y) → (X ⟶ Y)
preimage
f: ?m.9987
f
,
F: C ⥤ D
F
.
image_preimage: ∀ {C : Type ?u.10032} [inst : Category C] {D : Type ?u.10031} [inst_1 : Category D] (F : C ⥤ D) [inst_2 : Full F] {X Y : C} (f : F.obj X ⟶ F.obj Y), F.map (F.preimage f) = f
image_preimage
f: ?m.9987
f
⟩ #align category_theory.functor.map_surjective
CategoryTheory.Functor.map_surjective: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {X Y : C} (F : C ⥤ D) [inst_2 : Full F], Function.Surjective F.map
CategoryTheory.Functor.map_surjective
/-- Deduce that `F` is full from the existence of preimages, using choice. -/ noncomputable def
fullOfExists: {C : Type u₁} → [inst : Category C] → {D : Type u₂} → [inst_1 : Category D] → (F : C ⥤ D) → (∀ (X Y : C) (f : F.obj X ⟶ F.obj Y), ∃ p, F.map p = f) → Full F
fullOfExists
(
F: C ⥤ D
F
:
C: Type u₁
C
⥤
D: Type u₂
D
) (
h: ∀ (X Y : C) (f : F.obj X ⟶ F.obj Y), ∃ p, F.map p = f
h
: ∀ (
X: C
X
Y: C
Y
:
C: Type u₁
C
) (
f: F.obj X ⟶ F.obj Y
f
:
F: C ⥤ D
F
.
obj: {V : Type ?u.10144} → [inst : Quiver V] → {W : Type ?u.10143} → [inst_1 : Quiver W] → V ⥤q W → V → W
obj
X: C
X
⟶
F: C ⥤ D
F
.
obj: {V : Type ?u.10194} → [inst : Quiver V] → {W : Type ?u.10193} → [inst_1 : Quiver W] → V ⥤q W → V → W
obj
Y: C
Y
), ∃
p: ?m.10226
p
,
F: C ⥤ D
F
.
map: {V : Type ?u.10240} → [inst : Quiver V] → {W : Type ?u.10239} → [inst_1 : Quiver W] → (self : V ⥤q W) → {X Y : V} → (X ⟶ Y) → (self.obj X ⟶ self.obj Y)
map
p: ?m.10226
p
=
f: F.obj X ⟶ F.obj Y
f
) :
Full: {C : Type ?u.10307} → [inst : Category C] → {D : Type ?u.10306} → [inst_1 : Category D] → C ⥤ D → Type (max(max?u.10307?u.10309)?u.10308)
Full
F: C ⥤ D
F
:=

Goals accomplished! 🐙
C: Type u₁

inst✝¹: Category C

D: Type u₂

inst✝: Category D

X, Y: C

F: C ⥤ D

h: ∀ (X Y : C) (f : F.obj X ⟶ F.obj Y), ∃ p, F.map p = f


C: Type u₁

inst✝¹: Category C

D: Type u₂

inst✝: Category D

X, Y: C

F: C ⥤ D

p: (X Y : C) → (F.obj X ⟶ F.obj Y) → (X ⟶ Y)

hp: ∀ (X Y : C) (f : F.obj X ⟶ F.obj Y), F.map (p X Y f) = f


C: Type u₁

inst✝¹: Category C

D: Type u₂

inst✝: Category D

X, Y: C

F: C ⥤ D

h: ∀ (X Y : C) (f : F.obj X ⟶ F.obj Y), ∃ p, F.map p = f



Goals accomplished! 🐙
#align category_theory.functor.full_of_exists
CategoryTheory.Functor.fullOfExists: {C : Type u₁} → [inst : Category C] → {D : Type u₂} → [inst_1 : Category D] → (F : C ⥤ D) → (∀ (X Y : C) (f : F.obj X ⟶ F.obj Y), ∃ p, F.map p = f) → Full F
CategoryTheory.Functor.fullOfExists
/-- Deduce that `F` is full from surjectivity of `F.map`, using choice. -/ noncomputable def
fullOfSurjective: {C : Type u₁} → [inst : Category C] → {D : Type u₂} → [inst_1 : Category D] → (F : C ⥤ D) → (∀ (X Y : C), Function.Surjective F.map) → Full F
fullOfSurjective
(
F: C ⥤ D
F
:
C: Type u₁
C
⥤
D: Type u₂
D
) (
h: ∀ (X Y : C), Function.Surjective F.map
h
: ∀
X: C
X
Y: C
Y
:
C: Type u₁
C
,
Function.Surjective: {α : Sort ?u.10517} → {β : Sort ?u.10516} → (α → β) → Prop
Function.Surjective
(
F: C ⥤ D
F
.
map: {V : Type ?u.10672} → [inst : Quiver V] → {W : Type ?u.10671} → [inst_1 : Quiver W] → (self : V ⥤q W) → {X Y : V} → (X ⟶ Y) → (self.obj X ⟶ self.obj Y)
map
: (
X: C
X
⟶
Y: C
Y
) → (
F: C ⥤ D
F
.
obj: {V : Type ?u.10585} → [inst : Quiver V] → {W : Type ?u.10584} → [inst_1 : Quiver W] → V ⥤q W → V → W
obj
X: C
X
⟶
F: C ⥤ D
F
.
obj: {V : Type ?u.10634} → [inst : Quiver V] → {W : Type ?u.10633} → [inst_1 : Quiver W] → V ⥤q W → V → W
obj
Y: C
Y
))) :
Full: {C : Type ?u.10697} → [inst : Category C] → {D : Type ?u.10696} → [inst_1 : Category D] → C ⥤ D → Type (max(max?u.10697?u.10699)?u.10698)
Full
F: C ⥤ D
F
:=
fullOfExists: {C : Type ?u.10735} → [inst : Category C] → {D : Type ?u.10734} → [inst_1 : Category D] → (F : C ⥤ D) → (∀ (X Y : C) (f : F.obj X ⟶ F.obj Y), ∃ p, F.map p = f) → Full F
fullOfExists
_: ?m.10738 ⥤ ?m.10740
_
h: ∀ (X Y : C), Function.Surjective F.map
h
#align category_theory.functor.full_of_surjective
CategoryTheory.Functor.fullOfSurjective: {C : Type u₁} → [inst : Category C] → {D : Type u₂} → [inst_1 : Category D] → (F : C ⥤ D) → (∀ (X Y : C), Function.Surjective F.map) → Full F
CategoryTheory.Functor.fullOfSurjective
end Functor section variable {
F: C ⥤ D
F
:
C: Type u₁
C
⥤
D: Type u₂
D
} [
Full: {C : Type ?u.11454} → [inst : Category C] → {D : Type ?u.11453} → [inst_1 : Category D] → C ⥤ D → Type (max(max?u.11454?u.11456)?u.11455)
Full
F: C ⥤ D
F
] [
Faithful: {C : Type ?u.12751} → [inst : Category C] → {D : Type ?u.12750} → [inst_1 : Category D] → C ⥤ D → Prop
Faithful
F: C ⥤ D
F
] {
X: C
X
Y: C
Y
Z: C
Z
:
C: Type u₁
C
} @[simp] theorem
preimage_id: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {F : C ⥤ D} [inst_2 : Full F] [inst_3 : Faithful F] {X : C}, F.preimage (𝟙 (F.obj X)) = 𝟙 X
preimage_id
:
F: C ⥤ D
F
.
preimage: {C : Type ?u.11020} → [inst : Category C] → {D : Type ?u.11019} → [inst_1 : Category D] → {X Y : C} → (F : C ⥤ D) → [inst_2 : Full F] → (F.obj X ⟶ F.obj Y) → (X ⟶ Y)
preimage
(
𝟙: (X : ?m.11047) → X ⟶ X
𝟙
(
F: C ⥤ D
F
.
obj: {V : Type ?u.11081} → [inst : Quiver V] → {W : Type ?u.11080} → [inst_1 : Quiver W] → V ⥤q W → V → W
obj
X: C
X
)) =
𝟙: (X : ?m.11157) → X ⟶ X
𝟙
X: C
X
:=
F: C ⥤ D
F
.
map_injective: ∀ {C : Type ?u.11186} [inst : Category C] {D : Type ?u.11185} [inst_1 : Category D] {X Y : C} (F : C ⥤ D) [inst_2 : Faithful F], Function.Injective F.map
map_injective
(

Goals accomplished! 🐙
C: Type u₁

inst✝³: Category C

D: Type u₂

inst✝²: Category D

F: C ⥤ D

inst✝¹: Full F

inst✝: Faithful F

X, Y, Z: C


F.map (F.preimage (𝟙 (F.obj X))) = F.map (𝟙 X)

Goals accomplished! 🐙
) #align category_theory.preimage_id
CategoryTheory.preimage_id: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {F : C ⥤ D} [inst_2 : Full F] [inst_3 : Faithful F] {X : C}, F.preimage (𝟙 (F.obj X)) = 𝟙 X
CategoryTheory.preimage_id
@[simp] theorem
preimage_comp: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {F : C ⥤ D} [inst_2 : Full F] [inst_3 : Faithful F] {X Y Z : C} (f : F.obj X ⟶ F.obj Y) (g : F.obj Y ⟶ F.obj Z), F.preimage (f ≫ g) = F.preimage f ≫ F.preimage g
preimage_comp
(
f: F.obj X ⟶ F.obj Y
f
:
F: C ⥤ D
F
.
obj: {V : Type ?u.11570} → [inst : Quiver V] → {W : Type ?u.11569} → [inst_1 : Quiver W] → V ⥤q W → V → W
obj
X: C
X
⟶
F: C ⥤ D
F
.
obj: {V : Type ?u.11620} → [inst : Quiver V] → {W : Type ?u.11619} → [inst_1 : Quiver W] → V ⥤q W → V → W
obj
Y: C
Y
) (
g: F.obj Y ⟶ F.obj Z
g
:
F: C ⥤ D
F
.
obj: {V : Type ?u.11672} → [inst : Quiver V] → {W : Type ?u.11671} → [inst_1 : Quiver W] → V ⥤q W → V → W
obj
Y: C
Y
⟶
F: C ⥤ D
F
.
obj: {V : Type ?u.11692} → [inst : Quiver V] → {W : Type ?u.11691} → [inst_1 : Quiver W] → V ⥤q W → V → W
obj
Z: C
Z
) :
F: C ⥤ D
F
.
preimage: {C : Type ?u.11722} → [inst : Category C] → {D : Type ?u.11721} → [inst_1 : Category D] → {X Y : C} → (F : C ⥤ D) → [inst_2 : Full F] → (F.obj X ⟶ F.obj Y) → (X ⟶ Y)
preimage
(
f: F.obj X ⟶ F.obj Y
f
≫
g: F.obj Y ⟶ F.obj Z
g
) =
F: C ⥤ D
F
.
preimage: {C : Type ?u.11807} → [inst : Category C] → {D : Type ?u.11806} → [inst_1 : Category D] → {X Y : C} → (F : C ⥤ D) → [inst_2 : Full F] → (F.obj X ⟶ F.obj Y) → (X ⟶ Y)
preimage
f: F.obj X ⟶ F.obj Y
f
≫
F: C ⥤ D
F
.
preimage: {C : Type ?u.11842} → [inst : Category C] → {D : Type ?u.11841} → [inst_1 : Category D] → {X Y : C} → (F : C ⥤ D) → [inst_2 : Full F] → (F.obj X ⟶ F.obj Y) → (X ⟶ Y)
preimage
g: F.obj Y ⟶ F.obj Z
g
:=
F: C ⥤ D
F
.
map_injective: ∀ {C : Type ?u.11877} [inst : Category C] {D : Type ?u.11876} [inst_1 : Category D] {X Y : C} (F : C ⥤ D) [inst_2 : Faithful F], Function.Injective F.map
map_injective
(

Goals accomplished! 🐙
C: Type u₁

inst✝³: Category C

D: Type u₂

inst✝²: Category D

F: C ⥤ D

inst✝¹: Full F

inst✝: Faithful F

X, Y, Z: C

f: F.obj X ⟶ F.obj Y

g: F.obj Y ⟶ F.obj Z


F.map (F.preimage (f ≫ g)) = F.map (F.preimage f ≫ F.preimage g)

Goals accomplished! 🐙
) #align category_theory.preimage_comp
CategoryTheory.preimage_comp: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {F : C ⥤ D} [inst_2 : Full F] [inst_3 : Faithful F] {X Y Z : C} (f : F.obj X ⟶ F.obj Y) (g : F.obj Y ⟶ F.obj Z), F.preimage (f ≫ g) = F.preimage f ≫ F.preimage g
CategoryTheory.preimage_comp
@[simp] theorem
preimage_map: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {F : C ⥤ D} [inst_2 : Full F] [inst_3 : Faithful F] {X Y : C} (f : X ⟶ Y), F.preimage (F.map f) = f
preimage_map
(
f: X ⟶ Y
f
:
X: C
X
⟶
Y: C
Y
) :
F: C ⥤ D
F
.
preimage: {C : Type ?u.12378} → [inst : Category C] → {D : Type ?u.12377} → [inst_1 : Category D] → {X Y : C} → (F : C ⥤ D) → [inst_2 : Full F] → (F.obj X ⟶ F.obj Y) → (X ⟶ Y)
preimage
(
F: C ⥤ D
F
.
map: {V : Type ?u.12419} → [inst : Quiver V] → {W : Type ?u.12418} → [inst_1 : Quiver W] → (self : V ⥤q W) → {X Y : V} → (X ⟶ Y) → (self.obj X ⟶ self.obj Y)
map
f: X ⟶ Y
f
) =
f: X ⟶ Y
f
:=
F: C ⥤ D
F
.
map_injective: ∀ {C : Type ?u.12488} [inst : Category C] {D : Type ?u.12487} [inst_1 : Category D] {X Y : C} (F : C ⥤ D) [inst_2 : Faithful F], Function.Injective F.map
map_injective
(

Goals accomplished! 🐙
C: Type u₁

inst✝³: Category C

D: Type u₂

inst✝²: Category D

F: C ⥤ D

inst✝¹: Full F

inst✝: Faithful F

X, Y, Z: C

f: X ⟶ Y


F.map (F.preimage (F.map f)) = F.map f

Goals accomplished! 🐙
) #align category_theory.preimage_map
CategoryTheory.preimage_map: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {F : C ⥤ D} [inst_2 : Full F] [inst_3 : Faithful F] {X Y : C} (f : X ⟶ Y), F.preimage (F.map f) = f
CategoryTheory.preimage_map
variable (
F: ?m.12792
F
) namespace Functor /-- If `F : C ⥤ D` is fully faithful, every isomorphism `F.obj X ≅ F.obj Y` has a preimage. -/ @[
simps: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] (F : C ⥤ D) [inst_2 : Full F] [inst_3 : Faithful F] {X Y : C} (f : F.obj X ≅ F.obj Y), (preimageIso F f).inv = F.preimage f.inv
simps
] def
preimageIso: (F.obj X ≅ F.obj Y) → (X ≅ Y)
preimageIso
(
f: F.obj X ≅ F.obj Y
f
:
F: C ⥤ D
F
.
obj: {V : Type ?u.12939} → [inst : Quiver V] → {W : Type ?u.12938} → [inst_1 : Quiver W] → V ⥤q W → V → W
obj
X: C
X
≅
F: C ⥤ D
F
.
obj: {V : Type ?u.12989} → [inst : Quiver V] → {W : Type ?u.12988} → [inst_1 : Quiver W] → V ⥤q W → V → W
obj
Y: C
Y
) :
X: C
X
≅
Y: C
Y
where hom :=
F: C ⥤ D
F
.
preimage: {C : Type ?u.13033} → [inst : Category C] → {D : Type ?u.13032} → [inst_1 : Category D] → {X Y : C} → (F : C ⥤ D) → [inst_2 : Full F] → (F.obj X ⟶ F.obj Y) → (X ⟶ Y)
preimage
f: F.obj X ≅ F.obj Y
f
.
hom: {C : Type ?u.13069} → [inst : Category C] → {X Y : C} → (X ≅ Y) → (X ⟶ Y)
hom
inv :=
F: C ⥤ D
F
.
preimage: {C : Type ?u.13081} → [inst : Category C] → {D : Type ?u.13080} → [inst_1 : Category D] → {X Y : C} → (F : C ⥤ D) → [inst_2 : Full F] → (F.obj X ⟶ F.obj Y) → (X ⟶ Y)
preimage
f: F.obj X ≅ F.obj Y
f
.
inv: {C : Type ?u.13102} → [inst : Category C] → {X Y : C} → (X ≅ Y) → (Y ⟶ X)
inv
hom_inv_id :=
F: C ⥤ D
F
.
map_injective: ∀ {C : Type ?u.13110} [inst : Category C] {D : Type ?u.13109} [inst_1 : Category D] {X Y : C} (F : C ⥤ D) [inst_2 : Faithful F], Function.Injective F.map
map_injective
(

Goals accomplished! 🐙
C: Type u₁

inst✝³: Category C

D: Type u₂

inst✝²: Category D

F: C ⥤ D

inst✝¹: Full F

inst✝: Faithful F

X, Y, Z: C

f: F.obj X ≅ F.obj Y


F.map (F.preimage f.hom ≫ F.preimage f.inv) = F.map (𝟙 X)

Goals accomplished! 🐙
) inv_hom_id :=
F: C ⥤ D
F
.
map_injective: ∀ {C : Type ?u.13151} [inst : Category C] {D : Type ?u.13150} [inst_1 : Category D] {X Y : C} (F : C ⥤ D) [inst_2 : Faithful F], Function.Injective F.map
map_injective
(

Goals accomplished! 🐙
C: Type u₁

inst✝³: Category C

D: Type u₂

inst✝²: Category D

F: C ⥤ D

inst✝¹: Full F

inst✝: Faithful F

X, Y, Z: C

f: F.obj X ≅ F.obj Y


F.map (F.preimage f.inv ≫ F.preimage f.hom) = F.map (𝟙 Y)

Goals accomplished! 🐙
) #align category_theory.functor.preimage_iso
CategoryTheory.Functor.preimageIso: {C : Type u₁} → [inst : Category C] → {D : Type u₂} → [inst_1 : Category D] → (F : C ⥤ D) → [inst_2 : Full F] → [inst_3 : Faithful F] → {X Y : C} → (F.obj X ≅ F.obj Y) → (X ≅ Y)
CategoryTheory.Functor.preimageIso
#align category_theory.functor.preimage_iso_inv
CategoryTheory.Functor.preimageIso_inv: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] (F : C ⥤ D) [inst_2 : Full F] [inst_3 : Faithful F] {X Y : C} (f : F.obj X ≅ F.obj Y), (preimageIso F f).inv = F.preimage f.inv
CategoryTheory.Functor.preimageIso_inv
#align category_theory.functor.preimage_iso_hom
CategoryTheory.Functor.preimageIso_hom: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] (F : C ⥤ D) [inst_2 : Full F] [inst_3 : Faithful F] {X Y : C} (f : F.obj X ≅ F.obj Y), (preimageIso F f).hom = F.preimage f.hom
CategoryTheory.Functor.preimageIso_hom
@[simp] theorem
preimageIso_mapIso: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] (F : C ⥤ D) [inst_2 : Full F] [inst_3 : Faithful F] {X Y : C} (f : X ≅ Y), preimageIso F (F.mapIso f) = f
preimageIso_mapIso
(
f: X ≅ Y
f
:
X: C
X
≅
Y: C
Y
) :
F: C ⥤ D
F
.
preimageIso: {C : Type ?u.13998} → [inst : Category C] → {D : Type ?u.13997} → [inst_1 : Category D] → (F : C ⥤ D) → [inst_2 : Full F] → [inst_3 : Faithful F] → {X Y : C} → (F.obj X ≅ F.obj Y) → (X ≅ Y)
preimageIso
(
F: C ⥤ D
F
.
mapIso: {C : Type ?u.14027} → [inst : Category C] → {D : Type ?u.14026} → [inst_1 : Category D] → (F : C ⥤ D) → {X Y : C} → (X ≅ Y) → (F.obj X ≅ F.obj Y)
mapIso
f: X ≅ Y
f
) =
f: X ≅ Y
f
:=

Goals accomplished! 🐙
C: Type u₁

inst✝³: Category C

D: Type u₂

inst✝²: Category D

F: C ⥤ D

inst✝¹: Full F

inst✝: Faithful F

X, Y, Z: C

f: X ≅ Y


preimageIso F (F.mapIso f) = f
C: Type u₁

inst✝³: Category C

D: Type u₂

inst✝²: Category D

F: C ⥤ D

inst✝¹: Full F

inst✝: Faithful F

X, Y, Z: C

f: X ≅ Y


w
(preimageIso F (F.mapIso f)).hom = f.hom
C: Type u₁

inst✝³: Category C

D: Type u₂

inst✝²: Category D

F: C ⥤ D

inst✝¹: Full F

inst✝: Faithful F

X, Y, Z: C

f: X ≅ Y


preimageIso F (F.mapIso f) = f

Goals accomplished! 🐙
#align category_theory.functor.preimage_iso_map_iso
CategoryTheory.Functor.preimageIso_mapIso: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] (F : C ⥤ D) [inst_2 : Full F] [inst_3 : Faithful F] {X Y : C} (f : X ≅ Y), preimageIso F (F.mapIso f) = f
CategoryTheory.Functor.preimageIso_mapIso
end Functor /-- If the image of a morphism under a fully faithful functor in an isomorphism, then the original morphisms is also an isomorphism. -/ theorem
isIso_of_fully_faithful: ∀ (f : X ⟶ Y) [inst : IsIso (F.map f)], IsIso f
isIso_of_fully_faithful
(
f: X ⟶ Y
f
:
X: C
X
⟶
Y: C
Y
) [
IsIso: {C : Type ?u.14582} → [inst : Category C] → {X Y : C} → (X ⟶ Y) → Prop
IsIso
(
F: C ⥤ D
F
.
map: {V : Type ?u.14617} → [inst : Quiver V] → {W : Type ?u.14616} → [inst_1 : Quiver W] → (self : V ⥤q W) → {X Y : V} → (X ⟶ Y) → (self.obj X ⟶ self.obj Y)
map
f: X ⟶ Y
f
)] :
IsIso: {C : Type ?u.14670} → [inst : Category C] → {X Y : C} → (X ⟶ Y) → Prop
IsIso
f: X ⟶ Y
f
:= ⟨⟨
F: C ⥤ D
F
.
preimage: {C : Type ?u.14737} → [inst : Category C] → {D : Type ?u.14736} → [inst_1 : Category D] → {X Y : C} → (F : C ⥤ D) → [inst_2 : Full F] → (F.obj X ⟶ F.obj Y) → (X ⟶ Y)
preimage
(
inv: {C : Type ?u.14771} → [inst : Category C] → {X Y : C} → (f : X ⟶ Y) → [I : IsIso f] → Y ⟶ X
inv
(
F: C ⥤ D
F
.
map: {V : Type ?u.14804} → [inst : Quiver V] → {W : Type ?u.14803} → [inst_1 : Quiver W] → (self : V ⥤q W) → {X Y : V} → (X ⟶ Y) → (self.obj X ⟶ self.obj Y)
map
f: X ⟶ Y
f
)), ⟨
F: C ⥤ D
F
.
map_injective: ∀ {C : Type ?u.14859} [inst : Category C] {D : Type ?u.14858} [inst_1 : Category D] {X Y : C} (F : C ⥤ D) [inst_2 : Faithful F], Function.Injective F.map
map_injective
(

Goals accomplished! 🐙
C: Type u₁

inst✝⁴: Category C

D: Type u₂

inst✝³: Category D

F: C ⥤ D

inst✝²: Full F

inst✝¹: Faithful F

X, Y, Z: C

f: X ⟶ Y

inst✝: IsIso (F.map f)


F.map (f ≫ F.preimage (inv (F.map f))) = F.map (𝟙 X)

Goals accomplished! 🐙
),
F: C ⥤ D
F
.
map_injective: ∀ {C : Type ?u.14900} [inst : Category C] {D : Type ?u.14899} [inst_1 : Category D] {X Y : C} (F : C ⥤ D) [inst_2 : Faithful F], Function.Injective F.map
map_injective
(

Goals accomplished! 🐙
C: Type u₁

inst✝⁴: Category C

D: Type u₂

inst✝³: Category D

F: C ⥤ D

inst✝²: Full F

inst✝¹: Faithful F

X, Y, Z: C

f: X ⟶ Y

inst✝: IsIso (F.map f)


F.map (F.preimage (inv (F.map f)) ≫ f) = F.map (𝟙 Y)

Goals accomplished! 🐙
)⟩⟩⟩ #align category_theory.is_iso_of_fully_faithful
CategoryTheory.isIso_of_fully_faithful: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] (F : C ⥤ D) [inst_2 : Full F] [inst_3 : Faithful F] {X Y : C} (f : X ⟶ Y) [inst_4 : IsIso (F.map f)], IsIso f
CategoryTheory.isIso_of_fully_faithful
/-- If `F` is fully faithful, we have an equivalence of hom-sets `X ⟶ Y` and `F X ⟶ F Y`. -/ @[
simps: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] (F : C ⥤ D) [inst_2 : Full F] [inst_3 : Faithful F] {X Y : C} (f : F.obj X ⟶ F.obj Y), ↑(equivOfFullyFaithful F).symm f = F.preimage f
simps
] def
equivOfFullyFaithful: {C : Type u₁} → [inst : Category C] → {D : Type u₂} → [inst_1 : Category D] → (F : C ⥤ D) → [inst_2 : Full F] → [inst_3 : Faithful F] → {X Y : C} → (X ⟶ Y) ≃ (F.obj X ⟶ F.obj Y)
equivOfFullyFaithful
{
X: ?m.15514
X
Y: ?m.15517
Y
} : (
X: ?m.15514
X
⟶
Y: ?m.15517
Y
) ≃ (
F: C ⥤ D
F
.
obj: {V : Type ?u.15582} → [inst : Quiver V] → {W : Type ?u.15581} → [inst_1 : Quiver W] → V ⥤q W → V → W
obj
X: ?m.15514
X
⟶
F: C ⥤ D
F
.
obj: {V : Type ?u.15632} → [inst : Quiver V] → {W : Type ?u.15631} → [inst_1 : Quiver W] → V ⥤q W → V → W
obj
Y: ?m.15517
Y
) where toFun
f: ?m.15687
f
:=
F: C ⥤ D
F
.
map: {V : Type ?u.15700} → [inst : Quiver V] → {W : Type ?u.15699} → [inst_1 : Quiver W] → (self : V ⥤q W) → {X Y : V} → (X ⟶ Y) → (self.obj X ⟶ self.obj Y)
map
f: ?m.15687
f
invFun
f: ?m.15724
f
:=
F: C ⥤ D
F
.
preimage: {C : Type ?u.15727} → [inst : Category C] → {D : Type ?u.15726} → [inst_1 : Category D] → {X Y : C} → (F : C ⥤ D) → [inst_2 : Full F] → (F.obj X ⟶ F.obj Y) → (X ⟶ Y)
preimage
f: ?m.15724
f
left_inv
f: ?m.15766
f
:=

Goals accomplished! 🐙
C: Type u₁

inst✝³: Category C

D: Type u₂

inst✝²: Category D

F: C ⥤ D

inst✝¹: Full F

inst✝: Faithful F

X✝, Y✝, Z, X, Y: C

f: X ⟶ Y


(fun f => F.preimage f) ((fun f => F.map f) f) = f

Goals accomplished! 🐙
right_inv
f: ?m.15772
f
:=

Goals accomplished! 🐙
C: Type u₁

inst✝³: Category C

D: Type u₂

inst✝²: Category D

F: C ⥤ D

inst✝¹: Full F

inst✝: Faithful F

X✝, Y✝, Z, X, Y: C

f: F.obj X ⟶ F.obj Y


(fun f => F.map f) ((fun f => F.preimage f) f) = f

Goals accomplished! 🐙
#align category_theory.equiv_of_fully_faithful
CategoryTheory.equivOfFullyFaithful: {C : Type u₁} → [inst : Category C] → {D : Type u₂} → [inst_1 : Category D] → (F : C ⥤ D) → [inst_2 : Full F] → [inst_3 : Faithful F] → {X Y : C} → (X ⟶ Y) ≃ (F.obj X ⟶ F.obj Y)
CategoryTheory.equivOfFullyFaithful
#align category_theory.equiv_of_fully_faithful_apply
CategoryTheory.equivOfFullyFaithful_apply: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] (F : C ⥤ D) [inst_2 : Full F] [inst_3 : Faithful F] {X Y : C} (f : X ⟶ Y), ↑(equivOfFullyFaithful F) f = F.map f
CategoryTheory.equivOfFullyFaithful_apply
#align category_theory.equiv_of_fully_faithful_symm_apply
CategoryTheory.equivOfFullyFaithful_symm_apply: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] (F : C ⥤ D) [inst_2 : Full F] [inst_3 : Faithful F] {X Y : C} (f : F.obj X ⟶ F.obj Y), ↑(equivOfFullyFaithful F).symm f = F.preimage f
CategoryTheory.equivOfFullyFaithful_symm_apply
/-- If `F` is fully faithful, we have an equivalence of iso-sets `X ≅ Y` and `F X ≅ F Y`. -/ @[
simps: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] (F : C ⥤ D) [inst_2 : Full F] [inst_3 : Faithful F] {X Y : C} (f : F.obj X ≅ F.obj Y), ↑(isoEquivOfFullyFaithful F).symm f = Functor.preimageIso F f
simps
] def
isoEquivOfFullyFaithful: {X Y : C} → (X ≅ Y) ≃ (F.obj X ≅ F.obj Y)
isoEquivOfFullyFaithful
{
X: C
X
Y: ?m.16316
Y
} : (
X: ?m.16313
X
≅
Y: ?m.16316
Y
) ≃ (
F: C ⥤ D
F
.
obj: {V : Type ?u.16385} → [inst : Quiver V] → {W : Type ?u.16384} → [inst_1 : Quiver W] → V ⥤q W → V → W
obj
X: ?m.16313
X
≅
F: C ⥤ D
F
.
obj: {V : Type ?u.16435} → [inst : Quiver V] → {W : Type ?u.16434} → [inst_1 : Quiver W] → V ⥤q W → V → W
obj
Y: ?m.16316
Y
) where toFun
f: ?m.16460
f
:=
F: C ⥤ D
F
.
mapIso: {C : Type ?u.16464} → [inst : Category C] → {D : Type ?u.16463} → [inst_1 : Category D] → (F : C ⥤ D) → {X Y : C} → (X ≅ Y) → (F.obj X ≅ F.obj Y)
mapIso
f: ?m.16460
f
invFun
f: ?m.16499
f
:=
F: C ⥤ D
F
.
preimageIso: {C : Type ?u.16502} → [inst : Category C] → {D : Type ?u.16501} → [inst_1 : Category D] → (F : C ⥤ D) → [inst_2 : Full F] → [inst_3 : Faithful F] → {X Y : C} → (F.obj X ≅ F.obj Y) → (X ≅ Y)
preimageIso
f: ?m.16499
f
left_inv
f: ?m.16550
f
:=

Goals accomplished! 🐙
C: Type u₁

inst✝³: Category C

D: Type u₂

inst✝²: Category D

F: C ⥤ D

inst✝¹: Full F

inst✝: Faithful F

X✝, Y✝, Z, X, Y: C

f: X ≅ Y


(fun f => Functor.preimageIso F f) ((fun f => F.mapIso f) f) = f

Goals accomplished! 🐙
right_inv
f: ?m.16556
f
:=

Goals accomplished! 🐙
C: Type u₁

inst✝³: Category C

D: Type u₂

inst✝²: Category D

F: C ⥤ D

inst✝¹: Full F

inst✝: Faithful F

X✝, Y✝, Z, X, Y: C

f: F.obj X ≅ F.obj Y


(fun f => F.mapIso f) ((fun f => Functor.preimageIso F f) f) = f
C: Type u₁

inst✝³: Category C

D: Type u₂

inst✝²: Category D

F: C ⥤ D

inst✝¹: Full F

inst✝: Faithful F

X✝, Y✝, Z, X, Y: C

f: F.obj X ≅ F.obj Y


w
((fun f => F.mapIso f) ((fun f => Functor.preimageIso F f) f)).hom = f.hom
C: Type u₁

inst✝³: Category C

D: Type u₂

inst✝²: Category D

F: C ⥤ D

inst✝¹: Full F

inst✝: Faithful F

X✝, Y✝, Z, X, Y: C

f: F.obj X ≅ F.obj Y


(fun f => F.mapIso f) ((fun f => Functor.preimageIso F f) f) = f

Goals accomplished! 🐙
#align category_theory.iso_equiv_of_fully_faithful
CategoryTheory.isoEquivOfFullyFaithful: {C : Type u₁} → [inst : Category C] → {D : Type u₂} → [inst_1 : Category D] → (F : C ⥤ D) → [inst_2 : Full F] → [inst_3 : Faithful F] → {X Y : C} → (X ≅ Y) ≃ (F.obj X ≅ F.obj Y)
CategoryTheory.isoEquivOfFullyFaithful
#align category_theory.iso_equiv_of_fully_faithful_symm_apply
CategoryTheory.isoEquivOfFullyFaithful_symm_apply: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] (F : C ⥤ D) [inst_2 : Full F] [inst_3 : Faithful F] {X Y : C} (f : F.obj X ≅ F.obj Y), ↑(isoEquivOfFullyFaithful F).symm f = Functor.preimageIso F f
CategoryTheory.isoEquivOfFullyFaithful_symm_apply
#align category_theory.iso_equiv_of_fully_faithful_apply
CategoryTheory.isoEquivOfFullyFaithful_apply: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] (F : C ⥤ D) [inst_2 : Full F] [inst_3 : Faithful F] {X Y : C} (f : X ≅ Y), ↑(isoEquivOfFullyFaithful F) f = F.mapIso f
CategoryTheory.isoEquivOfFullyFaithful_apply
end section variable {
E: Type ?u.17178
E
:
Type _: Type (?u.17178+1)
Type _
} [
Category: Type ?u.17181 → Type (max?u.17181(?u.17182+1))
Category
E: Type ?u.17318
E
] {
F: C ⥤ D
F
G: C ⥤ D
G
:
C: Type u₁
C
⥤
D: Type u₂
D
} (
H: D ⥤ E
H
:
D: Type u₂
D
⥤
E: Type ?u.17318
E
) [
Full: {C : Type ?u.22200} → [inst : Category C] → {D : Type ?u.22199} → [inst_1 : Category D] → C ⥤ D → Type (max(max?u.22200?u.22202)?u.22201)
Full
H: D ⥤ E
H
] [
Faithful: {C : Type ?u.17273} → [inst : Category C] → {D : Type ?u.17272} → [inst_1 : Category D] → C ⥤ D → Prop
Faithful
H: D ⥤ E
H
] /-- We can construct a natural transformation between functors by constructing a natural transformation between those functors composed with a fully faithful functor. -/ @[
simps: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {E : Type u_1} [inst_2 : Category E] {F G : C ⥤ D} (H : D ⥤ E) [inst_3 : Full H] [inst_4 : Faithful H] (α : F ⋙ H ⟶ G ⋙ H) (X : C), (natTransOfCompFullyFaithful H α).app X = ↑(equivOfFullyFaithful H).symm (α.app X)
simps
] def
natTransOfCompFullyFaithful: {C : Type u₁} → [inst : Category C] → {D : Type u₂} → [inst_1 : Category D] → {E : Type u_1} → [inst_2 : Category E] → {F G : C ⥤ D} → (H : D ⥤ E) → [inst_3 : Full H] → [inst_4 : Faithful H] → (F ⋙ H ⟶ G ⋙ H) → (F ⟶ G)
natTransOfCompFullyFaithful
(
α: F ⋙ H ⟶ G ⋙ H
α
:
F: C ⥤ D
F
⋙
H: D ⥤ E
H
⟶
G: C ⥤ D
G
⋙
H: D ⥤ E
H
) :
F: C ⥤ D
F
⟶
G: C ⥤ D
G
where app
X: ?m.17684
X
:= (
equivOfFullyFaithful: {C : Type ?u.17687} → [inst : Category C] → {D : Type ?u.17686} → [inst_1 : Category D] → (F : C ⥤ D) → [inst_2 : Full F] → [inst_3 : Faithful F] → {X Y : C} → (X ⟶ Y) ≃ (F.obj X ⟶ F.obj Y)
equivOfFullyFaithful
H: D ⥤ E
H
).
symm: {α : Sort ?u.17727} → {β : Sort ?u.17726} → α ≃ β → β ≃ α
symm
(
α: F ⋙ H ⟶ G ⋙ H
α
.
app: {C : Type ?u.17803} → [inst : Category C] → {D : Type ?u.17802} → [inst_1 : Category D] → {F G : C ⥤ D} → NatTrans F G → (X : C) → F.obj X ⟶ G.obj X
app
X: ?m.17684
X
) naturality
X: ?m.17840
X
Y: ?m.17843
Y
f: ?m.17846
f
:=

Goals accomplished! 🐙
C: Type u₁

inst✝⁴: Category C

D: Type u₂

inst✝³: Category D

E: Type ?u.17318

inst✝²: Category E

F, G: C ⥤ D

H: D ⥤ E

inst✝¹: Full H

inst✝: Faithful H

α: F ⋙ H ⟶ G ⋙ H

X, Y: C

f: X ⟶ Y


F.map f ≫ (fun X => ↑(equivOfFullyFaithful H).symm (α.app X)) Y = (fun X => ↑(equivOfFullyFaithful H).symm (α.app X)) X ≫ G.map f
C: Type u₁

inst✝⁴: Category C

D: Type u₂

inst✝³: Category D

E: Type ?u.17318

inst✝²: Category E

F, G: C ⥤ D

H: D ⥤ E

inst✝¹: Full H

inst✝: Faithful H

α: F ⋙ H ⟶ G ⋙ H

X, Y: C

f: X ⟶ Y


F.map f ≫ H.preimage (α.app Y) = H.preimage (α.app X) ≫ G.map f
C: Type u₁

inst✝⁴: Category C

D: Type u₂

inst✝³: Category D

E: Type ?u.17318

inst✝²: Category E

F, G: C ⥤ D

H: D ⥤ E

inst✝¹: Full H

inst✝: Faithful H

α: F ⋙ H ⟶ G ⋙ H

X, Y: C

f: X ⟶ Y


F.map f ≫ (fun X => ↑(equivOfFullyFaithful H).symm (α.app X)) Y = (fun X => ↑(equivOfFullyFaithful H).symm (α.app X)) X ≫ G.map f
C: Type u₁

inst✝⁴: Category C

D: Type u₂

inst✝³: Category D

E: Type ?u.17318

inst✝²: Category E

F, G: C ⥤ D

H: D ⥤ E

inst✝¹: Full H

inst✝: Faithful H

α: F ⋙ H ⟶ G ⋙ H

X, Y: C

f: X ⟶ Y


a
H.map (F.map f ≫ H.preimage (α.app Y)) = H.map (H.preimage (α.app X) ≫ G.map f)
C: Type u₁

inst✝⁴: Category C

D: Type u₂

inst✝³: Category D

E: Type ?u.17318

inst✝²: Category E

F, G: C ⥤ D

H: D ⥤ E

inst✝¹: Full H

inst✝: Faithful H

α: F ⋙ H ⟶ G ⋙ H

X, Y: C

f: X ⟶ Y


F.map f ≫ (fun X => ↑(equivOfFullyFaithful H).symm (α.app X)) Y = (fun X => ↑(equivOfFullyFaithful H).symm (α.app X)) X ≫ G.map f

Goals accomplished! 🐙
#align category_theory.nat_trans_of_comp_fully_faithful
CategoryTheory.natTransOfCompFullyFaithful: {C : Type u₁} → [inst : Category C] → {D : Type u₂} → [inst_1 : Category D] → {E : Type u_1} → [inst_2 : Category E] → {F G : C ⥤ D} → (H : D ⥤ E) → [inst_3 : Full H] → [inst_4 : Faithful H] → (F ⋙ H ⟶ G ⋙ H) → (F ⟶ G)
CategoryTheory.natTransOfCompFullyFaithful
#align category_theory.nat_trans_of_comp_fully_faithful_app
CategoryTheory.natTransOfCompFullyFaithful_app: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {E : Type u_1} [inst_2 : Category E] {F G : C ⥤ D} (H : D ⥤ E) [inst_3 : Full H] [inst_4 : Faithful H] (α : F ⋙ H ⟶ G ⋙ H) (X : C), (natTransOfCompFullyFaithful H α).app X = ↑(equivOfFullyFaithful H).symm (α.app X)
CategoryTheory.natTransOfCompFullyFaithful_app
/-- We can construct a natural isomorphism between functors by constructing a natural isomorphism between those functors composed with a fully faithful functor. -/ @[simps!] def
natIsoOfCompFullyFaithful: {C : Type u₁} → [inst : Category C] → {D : Type u₂} → [inst_1 : Category D] → {E : Type u_1} → [inst_2 : Category E] → {F G : C ⥤ D} → (H : D ⥤ E) → [inst_3 : Full H] → [inst_4 : Faithful H] → (F ⋙ H ≅ G ⋙ H) → (F ≅ G)
natIsoOfCompFullyFaithful
(
i: F ⋙ H ≅ G ⋙ H
i
:
F: C ⥤ D
F
⋙
H: D ⥤ E
H
≅
G: C ⥤ D
G
⋙
H: D ⥤ E
H
) :
F: C ⥤ D
F
≅
G: C ⥤ D
G
:=
NatIso.ofComponents: {C : Type ?u.19746} → [inst : Category C] → {D : Type ?u.19745} → [inst_1 : Category D] → {F G : C ⥤ D} → (app : (X : C) → F.obj X ≅ G.obj X) → (∀ {X Y : C} (f : X ⟶ Y), F.map f ≫ (app Y).hom = (app X).hom ≫ G.map f) → (F ≅ G)
NatIso.ofComponents
(fun
X: ?m.19788
X
=> (
isoEquivOfFullyFaithful: {C : Type ?u.19791} → [inst : Category C] → {D : Type ?u.19790} → [inst_1 : Category D] → (F : C ⥤ D) → [inst_2 : Full F] → [inst_3 : Faithful F] → {X Y : C} → (X ≅ Y) ≃ (F.obj X ≅ F.obj Y)
isoEquivOfFullyFaithful
H: D ⥤ E
H
).
symm: {α : Sort ?u.19831} → {β : Sort ?u.19830} → α ≃ β → β ≃ α
symm
(
i: F ⋙ H ≅ G ⋙ H
i
.
app: {C : Type ?u.19907} → [inst : Category C] → {D : Type ?u.19906} → [inst_1 : Category D] → {F G : C ⥤ D} → (F ≅ G) → (X : C) → F.obj X ≅ G.obj X
app
X: ?m.19788
X
)) fun
f: ?m.19962
f
=>

Goals accomplished! 🐙
C: Type u₁

inst✝⁴: Category C

D: Type u₂

inst✝³: Category D

E: Type ?u.19429

inst✝²: Category E

F, G: C ⥤ D

H: D ⥤ E

inst✝¹: Full H

inst✝: Faithful H

i: F ⋙ H ≅ G ⋙ H

X✝, Y✝: C

f: X✝ ⟶ Y✝


F.map f ≫ ((fun X => ↑(isoEquivOfFullyFaithful H).symm (i.app X)) Y✝).hom = ((fun X => ↑(isoEquivOfFullyFaithful H).symm (i.app X)) X✝).hom ≫ G.map f
C: Type u₁

inst✝⁴: Category C

D: Type u₂

inst✝³: Category D

E: Type ?u.19429

inst✝²: Category E

F, G: C ⥤ D

H: D ⥤ E

inst✝¹: Full H

inst✝: Faithful H

i: F ⋙ H ≅ G ⋙ H

X✝, Y✝: C

f: X✝ ⟶ Y✝


F.map f ≫ H.preimage (i.hom.app Y✝) = H.preimage (i.hom.app X✝) ≫ G.map f
C: Type u₁

inst✝⁴: Category C

D: Type u₂

inst✝³: Category D

E: Type ?u.19429

inst✝²: Category E

F, G: C ⥤ D

H: D ⥤ E

inst✝¹: Full H

inst✝: Faithful H

i: F ⋙ H ≅ G ⋙ H

X✝, Y✝: C

f: X✝ ⟶ Y✝


F.map f ≫ ((fun X => ↑(isoEquivOfFullyFaithful H).symm (i.app X)) Y✝).hom = ((fun X => ↑(isoEquivOfFullyFaithful H).symm (i.app X)) X✝).hom ≫ G.map f
C: Type u₁

inst✝⁴: Category C

D: Type u₂

inst✝³: Category D

E: Type ?u.19429

inst✝²: Category E

F, G: C ⥤ D

H: D ⥤ E

inst✝¹: Full H

inst✝: Faithful H

i: F ⋙ H ≅ G ⋙ H

X✝, Y✝: C

f: X✝ ⟶ Y✝


a
H.map (F.map f ≫ H.preimage (i.hom.app Y✝)) = H.map (H.preimage (i.hom.app X✝) ≫ G.map f)
C: Type u₁

inst✝⁴: Category C

D: Type u₂

inst✝³: Category D

E: Type ?u.19429

inst✝²: Category E

F, G: C ⥤ D

H: D ⥤ E

inst✝¹: Full H

inst✝: Faithful H

i: F ⋙ H ≅ G ⋙ H

X✝, Y✝: C

f: X✝ ⟶ Y✝


F.map f ≫ ((fun X => ↑(isoEquivOfFullyFaithful H).symm (i.app X)) Y✝).hom = ((fun X => ↑(isoEquivOfFullyFaithful H).symm (i.app X)) X✝).hom ≫ G.map f

Goals accomplished! 🐙
#align category_theory.nat_iso_of_comp_fully_faithful
CategoryTheory.natIsoOfCompFullyFaithful: {C : Type u₁} → [inst : Category C] → {D : Type u₂} → [inst_1 : Category D] → {E : Type u_1} → [inst_2 : Category E] → {F G : C ⥤ D} → (H : D ⥤ E) → [inst_3 : Full H] → [inst_4 : Faithful H] → (F ⋙ H ≅ G ⋙ H) → (F ≅ G)
CategoryTheory.natIsoOfCompFullyFaithful
#align category_theory.nat_iso_of_comp_fully_faithful_hom_app
CategoryTheory.natIsoOfCompFullyFaithful_hom_app: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {E : Type u_1} [inst_2 : Category E] {F G : C ⥤ D} (H : D ⥤ E) [inst_3 : Full H] [inst_4 : Faithful H] (i : F ⋙ H ≅ G ⋙ H) (X : C), (natIsoOfCompFullyFaithful H i).hom.app X = H.preimage (i.hom.app X)
CategoryTheory.natIsoOfCompFullyFaithful_hom_app
#align category_theory.nat_iso_of_comp_fully_faithful_inv_app
CategoryTheory.natIsoOfCompFullyFaithful_inv_app: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {E : Type u_1} [inst_2 : Category E] {F G : C ⥤ D} (H : D ⥤ E) [inst_3 : Full H] [inst_4 : Faithful H] (i : F ⋙ H ≅ G ⋙ H) (X : C), (natIsoOfCompFullyFaithful H i).inv.app X = H.preimage (i.inv.app X)
CategoryTheory.natIsoOfCompFullyFaithful_inv_app
theorem
natIsoOfCompFullyFaithful_hom: ∀ (i : F ⋙ H ≅ G ⋙ H), (natIsoOfCompFullyFaithful H i).hom = natTransOfCompFullyFaithful H i.hom
natIsoOfCompFullyFaithful_hom
(
i: F ⋙ H ≅ G ⋙ H
i
:
F: C ⥤ D
F
⋙
H: D ⥤ E
H
≅
G: C ⥤ D
G
⋙
H: D ⥤ E
H
) : (
natIsoOfCompFullyFaithful: {C : Type ?u.22433} → [inst : Category C] → {D : Type ?u.22432} → [inst_1 : Category D] → {E : Type ?u.22431} → [inst_2 : Category E] → {F G : C ⥤ D} → (H : D ⥤ E) → [inst_3 : Full H] → [inst_4 : Faithful H] → (F ⋙ H ≅ G ⋙ H) → (F ≅ G)
natIsoOfCompFullyFaithful
H: D ⥤ E
H
i: F ⋙ H ≅ G ⋙ H
i
).
hom: {C : Type ?u.22503} → [inst : Category C] → {X Y : C} → (X ≅ Y) → (X ⟶ Y)
hom
=
natTransOfCompFullyFaithful: {C : Type ?u.22535} → [inst : Category C] → {D : Type ?u.22534} → [inst_1 : Category D] → {E : Type ?u.22533} → [inst_2 : Category E] → {F G : C ⥤ D} → (H : D ⥤ E) → [inst_3 : Full H] → [inst_4 : Faithful H] → (F ⋙ H ⟶ G ⋙ H) → (F ⟶ G)
natTransOfCompFullyFaithful
H: D ⥤ E
H
i: F ⋙ H ≅ G ⋙ H
i
.
hom: {C : Type ?u.22554} → [inst : Category C] → {X Y : C} → (X ≅ Y) → (X ⟶ Y)
hom
:=

Goals accomplished! 🐙
C: Type u₁

inst✝⁴: Category C

D: Type u₂

inst✝³: Category D

E: Type u_2

inst✝²: Category E

F, G: C ⥤ D

H: D ⥤ E

inst✝¹: Full H

inst✝: Faithful H

i: F ⋙ H ≅ G ⋙ H


C: Type u₁

inst✝⁴: Category C

D: Type u₂

inst✝³: Category D

E: Type u_2

inst✝²: Category E

F, G: C ⥤ D

H: D ⥤ E

inst✝¹: Full H

inst✝: Faithful H

i: F ⋙ H ≅ G ⋙ H

x✝: C


w.h
(natIsoOfCompFullyFaithful H i).hom.app x✝ = (natTransOfCompFullyFaithful H i.hom).app x✝
C: Type u₁

inst✝⁴: Category C

D: Type u₂

inst✝³: Category D

E: Type u_2

inst✝²: Category E

F, G: C ⥤ D

H: D ⥤ E

inst✝¹: Full H

inst✝: Faithful H

i: F ⋙ H ≅ G ⋙ H



Goals accomplished! 🐙
#align category_theory.nat_iso_of_comp_fully_faithful_hom
CategoryTheory.natIsoOfCompFullyFaithful_hom: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {E : Type u_2} [inst_2 : Category E] {F G : C ⥤ D} (H : D ⥤ E) [inst_3 : Full H] [inst_4 : Faithful H] (i : F ⋙ H ≅ G ⋙ H), (natIsoOfCompFullyFaithful H i).hom = natTransOfCompFullyFaithful H i.hom
CategoryTheory.natIsoOfCompFullyFaithful_hom
theorem
natIsoOfCompFullyFaithful_inv: ∀ (i : F ⋙ H ≅ G ⋙ H), (natIsoOfCompFullyFaithful H i).inv = natTransOfCompFullyFaithful H i.inv
natIsoOfCompFullyFaithful_inv
(
i: F ⋙ H ≅ G ⋙ H
i
:
F: C ⥤ D
F
⋙
H: D ⥤ E
H
≅
G: C ⥤ D
G
⋙
H: D ⥤ E
H
) : (
natIsoOfCompFullyFaithful: {C : Type ?u.24093} → [inst : Category C] → {D : Type ?u.24092} → [inst_1 : Category D] → {E : Type ?u.24091} → [inst_2 : Category E] → {F G : C ⥤ D} → (H : D ⥤ E) → [inst_3 : Full H] → [inst_4 : Faithful H] → (F ⋙ H ≅ G ⋙ H) → (F ≅ G)
natIsoOfCompFullyFaithful
H: D ⥤ E
H
i: F ⋙ H ≅ G ⋙ H
i
).
inv: {C : Type ?u.24163} → [inst : Category C] → {X Y : C} → (X ≅ Y) → (Y ⟶ X)
inv
=
natTransOfCompFullyFaithful: {C : Type ?u.24195} → [inst : Category C] → {D : Type ?u.24194} → [inst_1 : Category D] → {E : Type ?u.24193} → [inst_2 : Category E] → {F G : C ⥤ D} → (H : D ⥤ E) → [inst_3 : Full H] → [inst_4 : Faithful H] → (F ⋙ H ⟶ G ⋙ H) → (F ⟶ G)
natTransOfCompFullyFaithful
H: D ⥤ E
H
i: F ⋙ H ≅ G ⋙ H
i
.
inv: {C : Type ?u.24214} → [inst : Category C] → {X Y : C} → (X ≅ Y) → (Y ⟶ X)
inv
:=

Goals accomplished! 🐙
C: Type u₁

inst✝⁴: Category C

D: Type u₂

inst✝³: Category D

E: Type u_2

inst✝²: Category E

F, G: C ⥤ D

H: D ⥤ E

inst✝¹: Full H

inst✝: Faithful H

i: F ⋙ H ≅ G ⋙ H


C: Type u₁

inst✝⁴: Category C

D: Type u₂

inst✝³: Category D

E: Type u_2

inst✝²: Category E

F, G: C ⥤ D

H: D ⥤ E

inst✝¹: Full H

inst✝: Faithful H

i: F ⋙ H ≅ G ⋙ H

x✝: C


w.h
(natIsoOfCompFullyFaithful H i).inv.app x✝ = (natTransOfCompFullyFaithful H i.inv).app x✝
C: Type u₁

inst✝⁴: Category C

D: Type u₂

inst✝³: Category D

E: Type u_2

inst✝²: Category E

F, G: C ⥤ D

H: D ⥤ E

inst✝¹: Full H

inst✝: Faithful H

i: F ⋙ H ≅ G ⋙ H



Goals accomplished! 🐙
#align category_theory.nat_iso_of_comp_fully_faithful_inv
CategoryTheory.natIsoOfCompFullyFaithful_inv: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {E : Type u_2} [inst_2 : Category E] {F G : C ⥤ D} (H : D ⥤ E) [inst_3 : Full H] [inst_4 : Faithful H] (i : F ⋙ H ≅ G ⋙ H), (natIsoOfCompFullyFaithful H i).inv = natTransOfCompFullyFaithful H i.inv
CategoryTheory.natIsoOfCompFullyFaithful_inv
/-- Horizontal composition with a fully faithful functor induces a bijection on natural transformations. -/ @[
simps: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {E : Type u_1} [inst_2 : Category E] {F G : C ⥤ D} (H : D ⥤ E) [inst_3 : Full H] [inst_4 : Faithful H] (α : F ⋙ H ⟶ G ⋙ H), ↑(equivOfCompFullyFaithful H).symm α = natTransOfCompFullyFaithful H α
simps
] def
NatTrans.equivOfCompFullyFaithful: {C : Type u₁} → [inst : Category C] → {D : Type u₂} → [inst_1 : Category D] → {E : Type u_1} → [inst_2 : Category E] → {F G : C ⥤ D} → (H : D ⥤ E) → [inst_3 : Full H] → [inst_4 : Faithful H] → (F ⟶ G) ≃ (F ⋙ H ⟶ G ⋙ H)
NatTrans.equivOfCompFullyFaithful
: (
F: C ⥤ D
F
⟶
G: C ⥤ D
G
) ≃ (
F: C ⥤ D
F
⋙
H: D ⥤ E
H
⟶
G: C ⥤ D
G
⋙
H: D ⥤ E
H
) where toFun
α: ?m.25281
α
:=
α: ?m.25281
α
◫
𝟙: (X : ?m.25347) → X ⟶ X
𝟙
H: D ⥤ E
H
invFun :=
natTransOfCompFullyFaithful: {C : Type ?u.25398} → [inst : Category C] → {D : Type ?u.25397} → [inst_1 : Category D] → {E : Type ?u.25396} → [inst_2 : Category E] → {F G : C ⥤ D} → (H : D ⥤ E) → [inst_3 : Full H] → [inst_4 : Faithful H] → (F ⋙ H ⟶ G ⋙ H) → (F ⟶ G)
natTransOfCompFullyFaithful
H: D ⥤ E
H
left_inv :=

Goals accomplished! 🐙
C: Type u₁

inst✝⁴: Category C

D: Type u₂

inst✝³: Category D

E: Type ?u.24929

inst✝²: Category E

F, G: C ⥤ D

H: D ⥤ E

inst✝¹: Full H

inst✝: Faithful H



Goals accomplished! 🐙
right_inv :=

Goals accomplished! 🐙
C: Type u₁

inst✝⁴: Category C

D: Type u₂

inst✝³: Category D

E: Type ?u.24929

inst✝²: Category E

F, G: C ⥤ D

H: D ⥤ E

inst✝¹: Full H

inst✝: Faithful H



Goals accomplished! 🐙
#align category_theory.nat_trans.equiv_of_comp_fully_faithful
CategoryTheory.NatTrans.equivOfCompFullyFaithful: {C : Type u₁} → [inst : Category C] → {D : Type u₂} → [inst_1 : Category D] → {E : Type u_1} → [inst_2 : Category E] → {F G : C ⥤ D} → (H : D ⥤ E) → [inst_3 : Full H] → [inst_4 : Faithful H] → (F ⟶ G) ≃ (F ⋙ H ⟶ G ⋙ H)
CategoryTheory.NatTrans.equivOfCompFullyFaithful
#align category_theory.nat_trans.equiv_of_comp_fully_faithful_apply
CategoryTheory.NatTrans.equivOfCompFullyFaithful_apply: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {E : Type u_1} [inst_2 : Category E] {F G : C ⥤ D} (H : D ⥤ E) [inst_3 : Full H] [inst_4 : Faithful H] (α : F ⟶ G), ↑(NatTrans.equivOfCompFullyFaithful H) α = α ◫ 𝟙 H
CategoryTheory.NatTrans.equivOfCompFullyFaithful_apply
#align category_theory.nat_trans.equiv_of_comp_fully_faithful_symm_apply
CategoryTheory.NatTrans.equivOfCompFullyFaithful_symm_apply: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {E : Type u_1} [inst_2 : Category E] {F G : C ⥤ D} (H : D ⥤ E) [inst_3 : Full H] [inst_4 : Faithful H] (α : F ⋙ H ⟶ G ⋙ H), ↑(NatTrans.equivOfCompFullyFaithful H).symm α = natTransOfCompFullyFaithful H α
CategoryTheory.NatTrans.equivOfCompFullyFaithful_symm_apply
/-- Horizontal composition with a fully faithful functor induces a bijection on natural isomorphisms. -/ @[
simps: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {E : Type u_1} [inst_2 : Category E] {F G : C ⥤ D} (H : D ⥤ E) [inst_3 : Full H] [inst_4 : Faithful H] (e : F ≅ G), ↑(equivOfCompFullyFaithful H) e = hcomp e (Iso.refl H)
simps
] def
NatIso.equivOfCompFullyFaithful: {C : Type u₁} → [inst : Category C] → {D : Type u₂} → [inst_1 : Category D] → {E : Type u_1} → [inst_2 : Category E] → {F G : C ⥤ D} → (H : D ⥤ E) → [inst_3 : Full H] → [inst_4 : Faithful H] → (F ≅ G) ≃ (F ⋙ H ≅ G ⋙ H)
NatIso.equivOfCompFullyFaithful
: (
F: C ⥤ D
F
≅
G: C ⥤ D
G
) ≃ (
F: C ⥤ D
F
⋙
H: D ⥤ E
H
≅
G: C ⥤ D
G
⋙
H: D ⥤ E
H
) where toFun
e: ?m.28637
e
:=
NatIso.hcomp: {C : Type ?u.28641} → [inst : Category C] → {D : Type ?u.28640} → [inst_1 : Category D] → {E : Type ?u.28639} → [inst_2 : Category E] → {F G : C ⥤ D} → {H I : D ⥤ E} → (F ≅ G) → (H ≅ I) → (F ⋙ H ≅ G ⋙ I)
NatIso.hcomp
e: ?m.28637
e
(
Iso.refl: {C : Type ?u.28705} → [inst : Category C] → (X : C) → X ≅ X
Iso.refl
H: D ⥤ E
H
) invFun :=
natIsoOfCompFullyFaithful: {C : Type ?u.28740} → [inst : Category C] → {D : Type ?u.28739} → [inst_1 : Category D] → {E : Type ?u.28738} → [inst_2 : Category E] → {F G : C ⥤ D} → (H : D ⥤ E) → [inst_3 : Full H] → [inst_4 : Faithful H] → (F ⋙ H ≅ G ⋙ H) → (F ≅ G)
natIsoOfCompFullyFaithful
H: D ⥤ E
H
left_inv :=

Goals accomplished! 🐙
C: Type u₁

inst✝⁴: Category C

D: Type u₂

inst✝³: Category D

E: Type ?u.28315

inst✝²: Category E

F, G: C ⥤ D

H: D ⥤ E

inst✝¹: Full H

inst✝: Faithful H



Goals accomplished! 🐙
right_inv :=

Goals accomplished! 🐙
C: Type u₁

inst✝⁴: Category C

D: Type u₂

inst✝³: Category D

E: Type ?u.28315

inst✝²: Category E

F, G: C ⥤ D

H: D ⥤ E

inst✝¹: Full H

inst✝: Faithful H



Goals accomplished! 🐙
#align category_theory.nat_iso.equiv_of_comp_fully_faithful
CategoryTheory.NatIso.equivOfCompFullyFaithful: {C : Type u₁} → [inst : Category C] → {D : Type u₂} → [inst_1 : Category D] → {E : Type u_1} → [inst_2 : Category E] → {F G : C ⥤ D} → (H : D ⥤ E) → [inst_3 : Full H] → [inst_4 : Faithful H] → (F ≅ G) ≃ (F ⋙ H ≅ G ⋙ H)
CategoryTheory.NatIso.equivOfCompFullyFaithful
#align category_theory.nat_iso.equiv_of_comp_fully_faithful_symm_apply
CategoryTheory.NatIso.equivOfCompFullyFaithful_symm_apply: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {E : Type u_1} [inst_2 : Category E] {F G : C ⥤ D} (H : D ⥤ E) [inst_3 : Full H] [inst_4 : Faithful H] (i : F ⋙ H ≅ G ⋙ H), ↑(NatIso.equivOfCompFullyFaithful H).symm i = natIsoOfCompFullyFaithful H i
CategoryTheory.NatIso.equivOfCompFullyFaithful_symm_apply
#align category_theory.nat_iso.equiv_of_comp_fully_faithful_apply
CategoryTheory.NatIso.equivOfCompFullyFaithful_apply: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {E : Type u_1} [inst_2 : Category E] {F G : C ⥤ D} (H : D ⥤ E) [inst_3 : Full H] [inst_4 : Faithful H] (e : F ≅ G), ↑(NatIso.equivOfCompFullyFaithful H) e = NatIso.hcomp e (Iso.refl H)
CategoryTheory.NatIso.equivOfCompFullyFaithful_apply
end end CategoryTheory namespace CategoryTheory variable {
C: Type u₁
C
:
Type u₁: Type (u₁+1)
Type u₁
} [
Category: Type ?u.34795 → Type (max?u.34795(v₁+1))
Category
.{v₁}
C: Type u₁
C
] instance
Full.id: Full (𝟭 C)
Full.id
:
Full: {C : Type ?u.31765} → [inst : Category C] → {D : Type ?u.31764} → [inst_1 : Category D] → C ⥤ D → Type (max(max?u.31765?u.31767)?u.31766)
Full
(
𝟭: (C : Type ?u.31790) → [inst : Category C] → C ⥤ C
𝟭
C: Type u₁
C
) where preimage
f: ?m.31831
f
:=
f: ?m.31831
f
#align category_theory.full.id
CategoryTheory.Full.id: {C : Type u₁} → [inst : Category C] → Full (𝟭 C)
CategoryTheory.Full.id
instance
Faithful.id: ∀ {C : Type u₁} [inst : Category C], Faithful (𝟭 C)
Faithful.id
:
Faithful: {C : Type ?u.32209} → [inst : Category C] → {D : Type ?u.32208} → [inst_1 : Category D] → C ⥤ D → Prop
Faithful
(
𝟭: (C : Type ?u.32234) → [inst : Category C] → C ⥤ C
𝟭
C: Type u₁
C
) :=
{ }: Faithful ?m.32346
{ }
#align category_theory.faithful.id
CategoryTheory.Faithful.id: ∀ {C : Type u₁} [inst : Category C], Faithful (𝟭 C)
CategoryTheory.Faithful.id
variable {
D: Type u₂
D
:
Type u₂: Type (u₂+1)
Type u₂
} [
Category: Type ?u.33275 → Type (max?u.33275(v₂+1))
Category
.{v₂}
D: Type u₂
D
] {
E: Type u₃
E
:
Type u₃: Type (u₃+1)
Type u₃
} [
Category: Type ?u.33280 → Type (max?u.33280(v₃+1))
Category
.{v₃}
E: Type u₃
E
] variable (
F: C ⥤ D
F
F': C ⥤ D
F'
:
C: Type u₁
C
⥤
D: Type u₂
D
) (
G: D ⥤ E
G
:
D: Type u₂
D
⥤
E: Type u₃
E
) instance
Faithful.comp: ∀ [inst : Faithful F] [inst : Faithful G], Faithful (F ⋙ G)
Faithful.comp
[
Faithful: {C : Type ?u.32881} → [inst : Category C] → {D : Type ?u.32880} → [inst_1 : Category D] → C ⥤ D → Prop
Faithful
F: C ⥤ D
F
] [
Faithful: {C : Type ?u.32925} → [inst : Category C] → {D : Type ?u.32924} → [inst_1 : Category D] → C ⥤ D → Prop
Faithful
G: D ⥤ E
G
] :
Faithful: {C : Type ?u.32967} → [inst : Category C] → {D : Type ?u.32966} → [inst_1 : Category D] → C ⥤ D → Prop
Faithful
(
F: C ⥤ D
F
⋙
G: D ⥤ E
G
) where map_injective
p: ?m.33081
p
:=
F: C ⥤ D
F
.
map_injective: ∀ {C : Type ?u.33084} [inst : Category C] {D : Type ?u.33083} [inst_1 : Category D] {X Y : C} (F : C ⥤ D) [inst_2 : Faithful F], Function.Injective F.map
map_injective
(
G: D ⥤ E
G
.
map_injective: ∀ {C : Type ?u.33129} [inst : Category C] {D : Type ?u.33128} [inst_1 : Category D] {X Y : C} (F : C ⥤ D) [inst_2 : Faithful F], Function.Injective F.map
map_injective
p: ?m.33081
p
) #align category_theory.faithful.comp
CategoryTheory.Faithful.comp: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {E : Type u₃} [inst_2 : Category E] (F : C ⥤ D) (G : D ⥤ E) [inst_3 : Faithful F] [inst_4 : Faithful G], Faithful (F ⋙ G)
CategoryTheory.Faithful.comp
theorem
Faithful.of_comp: ∀ [inst : Faithful (F ⋙ G)], Faithful F
Faithful.of_comp
[
Faithful: {C : Type ?u.33329} → [inst : Category C] → {D : Type ?u.33328} → [inst_1 : Category D] → C ⥤ D → Prop
Faithful
<|
F: C ⥤ D
F
⋙
G: D ⥤ E
G
] :
Faithful: {C : Type ?u.33434} → [inst : Category C] → {D : Type ?u.33433} → [inst_1 : Category D] → C ⥤ D → Prop
Faithful
F: C ⥤ D
F
:= -- Porting note: (F ⋙ G).map_injective.of_comp has the incorrect type { map_injective := fun {
_: ?m.33488
_
_: ?m.33491
_
} =>
Function.Injective.of_comp: ∀ {α : Sort ?u.33495} {β : Sort ?u.33494} {γ : Sort ?u.33493} {f : α → β} {g : γ → α}, Function.Injective (f ∘ g) → Function.Injective g
Function.Injective.of_comp
(
F: C ⥤ D
F
⋙
G: D ⥤ E
G
).
map_injective: ∀ {C : Type ?u.33534} [inst : Category C] {D : Type ?u.33533} [inst_1 : Category D] {X Y : C} (F : C ⥤ D) [inst_2 : Faithful F], Function.Injective F.map
map_injective
} #align category_theory.faithful.of_comp
CategoryTheory.Faithful.of_comp: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {E : Type u₃} [inst_2 : Category E] (F : C ⥤ D) (G : D ⥤ E) [inst_3 : Faithful (F ⋙ G)], Faithful F
CategoryTheory.Faithful.of_comp
section variable {
F: ?m.33662
F
F': ?m.33665
F'
} /-- If `F` is full, and naturally isomorphic to some `F'`, then `F'` is also full. -/ def
Full.ofIso: [inst : Full F] → (F ≅ F') → Full F'
Full.ofIso
[
Full: {C : Type ?u.33729} → [inst : Category C] → {D : Type ?u.33728} → [inst_1 : Category D] → C ⥤ D → Type (max(max?u.33729?u.33731)?u.33730)
Full
F: C ⥤ D
F
] (
α: F ≅ F'
α
:
F: C ⥤ D
F
≅
F': C ⥤ D
F'
) :
Full: {C : Type ?u.33808} → [inst : Category C] → {D : Type ?u.33807} → [inst_1 : Category D] → C ⥤ D → Type (max(max?u.33808?u.33810)?u.33809)
Full
F': C ⥤ D
F'
where preimage {
X: ?m.33863
X
Y: ?m.33866
Y
}
f: ?m.33869
f
:=
F: C ⥤ D
F
.
preimage: {C : Type ?u.33872} → [inst : Category C] → {D : Type ?u.33871} → [inst_1 : Category D] → {X Y : C} → (F : C ⥤ D) → [inst_2 : Full F] → (F.obj X ⟶ F.obj Y) → (X ⟶ Y)
preimage
((
α: F ≅ F'
α
.
app: {C : Type ?u.33933} → [inst : Category C] → {D : Type ?u.33932} → [inst_1 : Category D] → {F G : C ⥤ D} → (F ≅ G) → (X : C) → F.obj X ≅ G.obj X
app
X: ?m.33863
X
).
hom: {C : Type ?u.33964} → [inst : Category C] → {X Y : C} → (X ≅ Y) → (X ⟶ Y)
hom
≫
f: ?m.33869
f
≫ (
α: F ≅ F'
α
.
app: {C : Type ?u.34006} → [inst : Category C] → {D : Type ?u.34005} → [inst_1 : Category D] → {F G : C ⥤ D} → (F ≅ G) → (X : C) → F.obj X ≅ G.obj X
app
Y: ?m.33866
Y
).
inv: {C : Type ?u.34029} → [inst : Category C] → {X Y : C} → (X ≅ Y) → (Y ⟶ X)
inv
) witness
f: ?m.34051
f
:=

Goals accomplished! 🐙
C: Type u₁

inst✝³: Category C

D: Type u₂

inst✝²: Category D

E: Type u₃

inst✝¹: Category E

F, F': C ⥤ D

G: D ⥤ E

inst✝: Full F

α: F ≅ F'

X✝, Y✝: C

f: F'.obj X✝ ⟶ F'.obj Y✝


F'.map ((fun {X Y} f => F.preimage ((α.app X).hom ≫ f ≫ (α.app Y).inv)) f) = f

Goals accomplished! 🐙
#align category_theory.full.of_iso
CategoryTheory.Full.ofIso: {C : Type u₁} → [inst : Category C] → {D : Type u₂} → [inst_1 : Category D] → {F F' : C ⥤ D} → [inst_2 : Full F] → (F ≅ F') → Full F'
CategoryTheory.Full.ofIso
theorem
Faithful.of_iso: ∀ [inst : Faithful F], (F ≅ F') → Faithful F'
Faithful.of_iso
[
Faithful: {C : Type ?u.34854} → [inst : Category C] → {D : Type ?u.34853} → [inst_1 : Category D] → C ⥤ D → Prop
Faithful
F: C ⥤ D
F
] (
α: F ≅ F'
α
:
F: C ⥤ D
F
≅
F': C ⥤ D
F'
) :
Faithful: {C : Type ?u.34933} → [inst : Category C] → {D : Type ?u.34932} → [inst_1 : Category D] → C ⥤ D → Prop
Faithful
F': C ⥤ D
F'
:= { map_injective := fun
h: ?m.34992
h
=>
F: C ⥤ D
F
.
map_injective: ∀ {C : Type ?u.34995} [inst : Category C] {D : Type ?u.34994} [inst_1 : Category D] {X Y : C} (F : C ⥤ D) [inst_2 : Faithful F], Function.Injective F.map
map_injective
(

Goals accomplished! 🐙
C: Type u₁

inst✝³: Category C

D: Type u₂

inst✝²: Category D

E: Type u₃

inst✝¹: Category E

F, F': C ⥤ D

G: D ⥤ E

inst✝: Faithful F

α: F ≅ F'

X✝, Y✝: C

a₁✝, a₂✝: X✝ ⟶ Y✝

h: F'.map a₁✝ = F'.map a₂✝


F.map a₁✝ = F.map a₂✝
C: Type u₁

inst✝³: Category C

D: Type u₂

inst✝²: Category D

E: Type u₃

inst✝¹: Category E

F, F': C ⥤ D

G: D ⥤ E

inst✝: Faithful F

α: F ≅ F'

X✝, Y✝: C

a₁✝, a₂✝: X✝ ⟶ Y✝

h: F'.map a₁✝ = F'.map a₂✝


F.map a₁✝ = F.map a₂✝
C: Type u₁

inst✝³: Category C

D: Type u₂

inst✝²: Category D

E: Type u₃

inst✝¹: Category E

F, F': C ⥤ D

G: D ⥤ E

inst✝: Faithful F

α: F ≅ F'

X✝, Y✝: C

a₁✝, a₂✝: X✝ ⟶ Y✝

h: F'.map a₁✝ = F'.map a₂✝


α.symm.inv.app X✝ ≫ F'.map a₁✝ ≫ α.symm.hom.app Y✝ = F.map a₂✝
C: Type u₁

inst✝³: Category C

D: Type u₂

inst✝²: Category D

E: Type u₃

inst✝¹: Category E

F, F': C ⥤ D

G: D ⥤ E

inst✝: Faithful F

α: F ≅ F'

X✝, Y✝: C

a₁✝, a₂✝: X✝ ⟶ Y✝

h: F'.map a₁✝ = F'.map a₂✝


F.map a₁✝ = F.map a₂✝
C: Type u₁

inst✝³: Category C

D: Type u₂

inst✝²: Category D

E: Type u₃

inst✝¹: Category E

F, F': C ⥤ D

G: D ⥤ E

inst✝: Faithful F

α: F ≅ F'

X✝, Y✝: C

a₁✝, a₂✝: X✝ ⟶ Y✝

h: F'.map a₁✝ = F'.map a₂✝


α.symm.inv.app X✝ ≫ F'.map a₂✝ ≫ α.symm.hom.app Y✝ = F.map a₂✝
C: Type u₁

inst✝³: Category C

D: Type u₂

inst✝²: Category D

E: Type u₃

inst✝¹: Category E

F, F': C ⥤ D

G: D ⥤ E

inst✝: Faithful F

α: F ≅ F'

X✝, Y✝: C

a₁✝, a₂✝: X✝ ⟶ Y✝

h: F'.map a₁✝ = F'.map a₂✝


F.map a₁✝ = F.map a₂✝
C: Type u₁

inst✝³: Category C

D: Type u₂

inst✝²: Category D

E: Type u₃

inst✝¹: Category E

F, F': C ⥤ D

G: D ⥤ E

inst✝: Faithful F

α: F ≅ F'

X✝, Y✝: C

a₁✝, a₂✝: X✝ ⟶ Y✝

h: F'.map a₁✝ = F'.map a₂✝


F.map a₂✝ = F.map a₂✝

Goals accomplished! 🐙
) } #align category_theory.faithful.of_iso
CategoryTheory.Faithful.of_iso: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {F F' : C ⥤ D} [inst_2 : Faithful F], (F ≅ F') → Faithful F'
CategoryTheory.Faithful.of_iso
end variable {
F: ?m.35253
F
G: ?m.35256
G
} theorem
Faithful.of_comp_iso: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {E : Type u₃} [inst_2 : Category E] {F : C ⥤ D} {G : D ⥤ E} {H : C ⥤ E} [inst_3 : Faithful H], (F ⋙ G ≅ H) → Faithful F
Faithful.of_comp_iso
{
H: C ⥤ E
H
:
C: Type u₁
C
⥤
E: Type u₃
E
} [
Faithful: {C : Type ?u.35336} → [inst : Category C] → {D : Type ?u.35335} → [inst_1 : Category D] → C ⥤ D → Prop
Faithful
H: C ⥤ E
H
] (
h: F ⋙ G ≅ H
h
:
F: C ⥤ D
F
⋙
G: D ⥤ E
G
≅
H: C ⥤ E
H
) :
Faithful: {C : Type ?u.35476} → [inst : Category C] → {D : Type ?u.35475} → [inst_1 : Category D] → C ⥤ D → Prop
Faithful
F: C ⥤ D
F
:= @
Faithful.of_comp: ∀ {C : Type ?u.35513} [inst : Category C] {D : Type ?u.35512} [inst_1 : Category D] {E : Type ?u.35511} [inst_2 : Category E] (F : C ⥤ D) (G : D ⥤ E) [inst_3 : Faithful (F ⋙ G)], Faithful F
Faithful.of_comp
_: Type ?u.35513
_
_
_: Type ?u.35512
_
_
_: Type ?u.35511
_
_
F: C ⥤ D
F
G: D ⥤ E
G
(
Faithful.of_iso: ∀ {C : Type ?u.35551} [inst : Category C] {D : Type ?u.35550} [inst_1 : Category D] {F F' : C ⥤ D} [inst_2 : Faithful F], (F ≅ F') → Faithful F'
Faithful.of_iso
h: F ⋙ G ≅ H
h
.
symm: {C : Type ?u.35600} → [inst : Category C] → {X Y : C} → (X ≅ Y) → (Y ≅ X)
symm
) #align category_theory.faithful.of_comp_iso
CategoryTheory.Faithful.of_comp_iso: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {E : Type u₃} [inst_2 : Category E] {F : C ⥤ D} {G : D ⥤ E} {H : C ⥤ E} [inst_3 : Faithful H], (F ⋙ G ≅ H) → Faithful F
CategoryTheory.Faithful.of_comp_iso
alias
Faithful.of_comp_iso: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {E : Type u₃} [inst_2 : Category E] {F : C ⥤ D} {G : D ⥤ E} {H : C ⥤ E} [inst_3 : Faithful H], (F ⋙ G ≅ H) → Faithful F
Faithful.of_comp_iso
←
_root_.CategoryTheory.Iso.faithful_of_comp: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {E : Type u₃} [inst_2 : Category E] {F : C ⥤ D} {G : D ⥤ E} {H : C ⥤ E} [inst_3 : Faithful H], (F ⋙ G ≅ H) → Faithful F
_root_.CategoryTheory.Iso.faithful_of_comp
#align category_theory.iso.faithful_of_comp
CategoryTheory.Iso.faithful_of_comp: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {E : Type u₃} [inst_2 : Category E] {F : C ⥤ D} {G : D ⥤ E} {H : C ⥤ E} [inst_3 : Faithful H], (F ⋙ G ≅ H) → Faithful F
CategoryTheory.Iso.faithful_of_comp
-- We could prove this from `Faithful.of_comp_iso` using `eq_to_iso`, -- but that would introduce a cyclic import. theorem
Faithful.of_comp_eq: ∀ {H : C ⥤ E} [ℋ : Faithful H], F ⋙ G = H → Faithful F
Faithful.of_comp_eq
{
H: C ⥤ E
H
:
C: Type u₁
C
⥤
E: Type u₃
E
} [
ℋ: Faithful H
ℋ
:
Faithful: {C : Type ?u.35724} → [inst : Category C] → {D : Type ?u.35723} → [inst_1 : Category D] → C ⥤ D → Prop
Faithful
H: C ⥤ E
H
] (
h: F ⋙ G = H
h
:
F: C ⥤ D
F
⋙
G: D ⥤ E
G
=
H: C ⥤ E
H
) :
Faithful: {C : Type ?u.35806} → [inst : Category C] → {D : Type ?u.35805} → [inst_1 : Category D] → C ⥤ D → Prop
Faithful
F: C ⥤ D
F
:= @
Faithful.of_comp: ∀ {C : Type ?u.35843} [inst : Category C] {D : Type ?u.35842} [inst_1 : Category D] {E : Type ?u.35841} [inst_2 : Category E] (F : C ⥤ D) (G : D ⥤ E) [inst_3 : Faithful (F ⋙ G)], Faithful F
Faithful.of_comp
_: Type ?u.35843
_
_
_: Type ?u.35842
_
_
_: Type ?u.35841
_
_
F: C ⥤ D
F
G: D ⥤ E
G
(
h: F ⋙ G = H
h
.
symm: ∀ {α : Sort ?u.35880} {a b : α}, a = b → b = a
symm
▸
ℋ: Faithful H
ℋ
) #align category_theory.faithful.of_comp_eq
CategoryTheory.Faithful.of_comp_eq: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {E : Type u₃} [inst_2 : Category E] {F : C ⥤ D} {G : D ⥤ E} {H : C ⥤ E} [ℋ : Faithful H], F ⋙ G = H → Faithful F
CategoryTheory.Faithful.of_comp_eq
alias
Faithful.of_comp_eq: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {E : Type u₃} [inst_2 : Category E] {F : C ⥤ D} {G : D ⥤ E} {H : C ⥤ E} [ℋ : Faithful H], F ⋙ G = H → Faithful F
Faithful.of_comp_eq
←
_root_.Eq.faithful_of_comp: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {E : Type u₃} [inst_2 : Category E] {F : C ⥤ D} {G : D ⥤ E} {H : C ⥤ E} [ℋ : Faithful H], F ⋙ G = H → Faithful F
_root_.Eq.faithful_of_comp
#align eq.faithful_of_comp
Eq.faithful_of_comp: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {E : Type u₃} [inst_2 : Category E] {F : C ⥤ D} {G : D ⥤ E} {H : C ⥤ E} [ℋ : Faithful H], F ⋙ G = H → Faithful F
Eq.faithful_of_comp
variable (
F: ?m.35979
F
G: ?m.35982
G
) /-- “Divide” a functor by a faithful functor. -/ protected def
Faithful.div: {C : Type u₁} → [inst : Category C] → {D : Type u₂} → [inst_1 : Category D] → {E : Type u₃} → [inst_2 : Category E] → (F : C ⥤ E) → (G : D ⥤ E) → [inst_3 : Faithful G] → (obj : C → D) → (∀ (X : C), G.obj (obj X) = F.obj X) → (map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)) → (∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)) → C ⥤ D
Faithful.div
(
F: C ⥤ E
F
:
C: Type u₁
C
⥤
E: Type u₃
E
) (
G: D ⥤ E
G
:
D: Type u₂
D
⥤
E: Type u₃
E
) [
Faithful: {C : Type ?u.36077} → [inst : Category C] → {D : Type ?u.36076} → [inst_1 : Category D] → C ⥤ D → Prop
Faithful
G: D ⥤ E
G
] (
obj: C → D
obj
:
C: Type u₁
C
→
D: Type u₂
D
) (
h_obj: ∀ (X : C), G.obj (obj X) = F.obj X
h_obj
: ∀
X: ?m.36123
X
,
G: D ⥤ E
G
.
obj: {V : Type ?u.36140} → [inst : Quiver V] → {W : Type ?u.36139} → [inst_1 : Quiver W] → V ⥤q W → V → W
obj
(
obj: C → D
obj
X: ?m.36123
X
) =
F: C ⥤ E
F
.
obj: {V : Type ?u.36196} → [inst : Quiver V] → {W : Type ?u.36195} → [inst_1 : Quiver W] → V ⥤q W → V → W
obj
X: ?m.36123
X
) (
map: {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
map
: ∀ {
X: ?m.36226
X
Y: ?m.36229
Y
}, (
X: ?m.36226
X
⟶
Y: ?m.36229
Y
) → (
obj: C → D
obj
X: ?m.36226
X
⟶
obj: C → D
obj
Y: ?m.36229
Y
)) (
h_map: ∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)
h_map
: ∀ {
X: ?m.36298
X
Y: ?m.36301
Y
} {
f: X ⟶ Y
f
:
X: ?m.36298
X
⟶
Y: ?m.36301
Y
},
HEq: {α : Sort ?u.36333} → α → {β : Sort ?u.36333} → β → Prop
HEq
(
G: D ⥤ E
G
.
map: {V : Type ?u.36346} → [inst : Quiver V] → {W : Type ?u.36345} → [inst_1 : Quiver W] → (self : V ⥤q W) → {X Y : V} → (X ⟶ Y) → (self.obj X ⟶ self.obj Y)
map
(
map: {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
map
f: X ⟶ Y
f
)) (
F: C ⥤ E
F
.
map: {V : Type ?u.36440} → [inst : Quiver V] → {W : Type ?u.36439} → [inst_1 : Quiver W] → (self : V ⥤q W) → {X Y : V} → (X ⟶ Y) → (self.obj X ⟶ self.obj Y)
map
f: X ⟶ Y
f
)) :
C: Type u₁
C
⥤
D: Type u₂
D
:= { obj, map := @
map: {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
map
, map_id :=

Goals accomplished! 🐙
C: Type u₁

inst✝³: Category C

D: Type u₂

inst✝²: Category D

E: Type u₃

inst✝¹: Category E

F✝, F': C ⥤ D

G✝: D ⥤ E

F: C ⥤ E

G: D ⥤ E

inst✝: Faithful G

obj: C → D

h_obj: ∀ (X : C), G.obj (obj X) = F.obj X

map: {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)

h_map: ∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)


∀ (X : C), { obj := obj, map := map }.map (𝟙 X) = 𝟙 ({ obj := obj, map := map }.obj X)
C: Type u₁

inst✝³: Category C

D: Type u₂

inst✝²: Category D

E: Type u₃

inst✝¹: Category E

F✝, F': C ⥤ D

G✝: D ⥤ E

F: C ⥤ E

G: D ⥤ E

inst✝: Faithful G

obj: C → D

h_obj: ∀ (X : C), G.obj (obj X) = F.obj X

map: {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)

h_map: ∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)

X: C


{ obj := obj, map := map }.map (𝟙 X) = 𝟙 ({ obj := obj, map := map }.obj X)
C: Type u₁

inst✝³: Category C

D: Type u₂

inst✝²: Category D

E: Type u₃

inst✝¹: Category E

F✝, F': C ⥤ D

G✝: D ⥤ E

F: C ⥤ E

G: D ⥤ E

inst✝: Faithful G

obj: C → D

h_obj: ∀ (X : C), G.obj (obj X) = F.obj X

map: {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)

h_map: ∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)


∀ (X : C), { obj := obj, map := map }.map (𝟙 X) = 𝟙 ({ obj := obj, map := map }.obj X)
C: Type u₁

inst✝³: Category C

D: Type u₂

inst✝²: Category D

E: Type u₃

inst✝¹: Category E

F✝, F': C ⥤ D

G✝: D ⥤ E

F: C ⥤ E

G: D ⥤ E

inst✝: Faithful G

obj: C → D

h_obj: ∀ (X : C), G.obj (obj X) = F.obj X

map: {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)

h_map: ∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)

X: C


a
G.map ({ obj := obj, map := map }.map (𝟙 X)) = G.map (𝟙 ({ obj := obj, map := map }.obj X))
C: Type u₁

inst✝³: Category C

D: Type u₂

inst✝²: Category D

E: Type u₃

inst✝¹: Category E

F✝, F': C ⥤ D

G✝: D ⥤ E

F: C ⥤ E

G: D ⥤ E

inst✝: Faithful G

obj: C → D

h_obj: ∀ (X : C), G.obj (obj X) = F.obj X

map: {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)

h_map: ∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)


∀ (X : C), { obj := obj, map := map }.map (𝟙 X) = 𝟙 ({ obj := obj, map := map }.obj X)
C: Type u₁

inst✝³: Category C

D: Type u₂

inst✝²: Category D

E: Type u₃

inst✝¹: Category E

F✝, F': C ⥤ D

G✝: D ⥤ E

F: C ⥤ E

G: D ⥤ E

inst✝: Faithful G

obj: C → D

h_obj: ∀ (X : C), G.obj (obj X) = F.obj X

map: {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)

h_map: ∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)

X: C


a.h
HEq (G.map ({ obj := obj, map := map }.map (𝟙 X))) (G.map (𝟙 ({ obj := obj, map := map }.obj X)))
C: Type u₁

inst✝³: Category C

D: Type u₂

inst✝²: Category D

E: Type u₃

inst✝¹: Category E

F✝, F': C ⥤ D

G✝: D ⥤ E

F: C ⥤ E

G: D ⥤ E

inst✝: Faithful G

obj: C → D

h_obj: ∀ (X : C), G.obj (obj X) = F.obj X

map: {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)

h_map: ∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)


∀ (X : C), { obj := obj, map := map }.map (𝟙 X) = 𝟙 ({ obj := obj, map := map }.obj X)
C: Type u₁

inst✝³: Category C

D: Type u₂

inst✝²: Category D

E: Type u₃

inst✝¹: Category E

F✝, F': C ⥤ D

G✝: D ⥤ E

F: C ⥤ E

G: D ⥤ E

inst✝: Faithful G

obj: C → D

h_obj: ∀ (X : C), G.obj (obj X) = F.obj X

map: {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)

h_map: ∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)

X: C


HEq (G.map ({ obj := obj, map := map }.map (𝟙 X))) (F.map (𝟙 X))
C: Type u₁

inst✝³: Category C

D: Type u₂

inst✝²: Category D

E: Type u₃

inst✝¹: Category E

F✝, F': C ⥤ D

G✝: D ⥤ E

F: C ⥤ E

G: D ⥤ E

inst✝: Faithful G

obj: C → D

h_obj: ∀ (X : C), G.obj (obj X) = F.obj X

map: {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)

h_map: ∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)

X: C


HEq (F.map (𝟙 X)) (G.map (𝟙 ({ obj := obj, map := map }.obj X)))
C: Type u₁

inst✝³: Category C

D: Type u₂

inst✝²: Category D

E: Type u₃

inst✝¹: Category E

F✝, F': C ⥤ D

G✝: D ⥤ E

F: C ⥤ E

G: D ⥤ E

inst✝: Faithful G

obj: C → D

h_obj: ∀ (X : C), G.obj (obj X) = F.obj X

map: {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)

h_map: ∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)


∀ (X : C), { obj := obj, map := map }.map (𝟙 X) = 𝟙 ({ obj := obj, map := map }.obj X)
C: Type u₁

inst✝³: Category C

D: Type u₂

inst✝²: Category D

E: Type u₃

inst✝¹: Category E

F✝, F': C ⥤ D

G✝: D ⥤ E

F: C ⥤ E

G: D ⥤ E

inst✝: Faithful G

obj: C → D

h_obj: ∀ (X : C), G.obj (obj X) = F.obj X

map: {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)

h_map: ∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)

X: C


HEq (G.map ({ obj := obj, map := map }.map (𝟙 X))) (F.map (𝟙 X))
C: Type u₁

inst✝³: Category C

D: Type u₂

inst✝²: Category D

E: Type u₃

inst✝¹: Category E

F✝, F': C ⥤ D

G✝: D ⥤ E

F: C ⥤ E

G: D ⥤ E

inst✝: Faithful G

obj: C → D

h_obj: ∀ (X : C), G.obj (obj X) = F.obj X

map: {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)

h_map: ∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)

X: C


HEq (G.map ({ obj := obj, map := map }.map (𝟙 X))) (F.map (𝟙 X))
C: Type u₁

inst✝³: Category C

D: Type u₂

inst✝²: Category D

E: Type u₃

inst✝¹: Category E

F✝, F': C ⥤ D

G✝: D ⥤ E

F: C ⥤ E

G: D ⥤ E

inst✝: Faithful G

obj: C → D

h_obj: ∀ (X : C), G.obj (obj X) = F.obj X

map: {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)

h_map: ∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)

X: C


HEq (F.map (𝟙 X)) (G.map (𝟙 ({ obj := obj, map := map }.obj X)))

Goals accomplished! 🐙
C: Type u₁

inst✝³: Category C

D: Type u₂

inst✝²: Category D

E: Type u₃

inst✝¹: Category E

F✝, F': C ⥤ D

G✝: D ⥤ E

F: C ⥤ E

G: D ⥤ E

inst✝: Faithful G

obj: C → D

h_obj: ∀ (X : C), G.obj (obj X) = F.obj X

map: {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)

h_map: ∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)


∀ (X : C), { obj := obj, map := map }.map (𝟙 X) = 𝟙 ({ obj := obj, map := map }.obj X)
C: Type u₁

inst✝³: Category C

D: Type u₂

inst✝²: Category D

E: Type u₃

inst✝¹: Category E

F✝, F': C ⥤ D

G✝: D ⥤ E

F: C ⥤ E

G: D ⥤ E

inst✝: Faithful G

obj: C → D

h_obj: ∀ (X : C), G.obj (obj X) = F.obj X

map: {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)

h_map: ∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)

X: C