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) 2020 Bhavik Mehta. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Bhavik Mehta
Ported by: JoΓ«l Riou

! This file was ported from Lean 3 source module category_theory.essential_image
! leanprover-community/mathlib commit 550b58538991c8977703fdeb7c9d51a5aa27df11
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.CategoryTheory.NatIso
import Mathlib.CategoryTheory.FullSubcategory

/-!
# Essential image of a functor

The essential image `essImage` of a functor consists of the objects in the target category which
are isomorphic to an object in the image of the object function.
This, for instance, allows us to talk about objects belonging to a subcategory expressed as a
functor rather than a subtype, preserving the principle of equivalence. For example this lets us
define exponential ideals.

The essential image can also be seen as a subcategory of the target category, and witnesses that
a functor decomposes into a essentially surjective functor and a fully faithful functor.
(TODO: show that this decomposition forms an orthogonal factorisation system).
-/


universe v₁ vβ‚‚ u₁ uβ‚‚

noncomputable section

namespace CategoryTheory

variable {
C: Type u₁
C
:
Type u₁: Type (u₁+1)
Type u₁
} {
D: Type uβ‚‚
D
:
Type uβ‚‚: Type (uβ‚‚+1)
Type uβ‚‚
} [
Category: Type ?u.698 β†’ Type (max?u.698(v₁+1))
Category
.{v₁}
C: Type u₁
C
] [
Category: Type ?u.192 β†’ Type (max?u.192(vβ‚‚+1))
Category
.{vβ‚‚}
D: Type uβ‚‚
D
] {
F: C β₯€ D
F
:
C: Type u₁
C
β₯€
D: Type uβ‚‚
D
} namespace Functor /-- The essential image of a functor `F` consists of those objects in the target category which are isomorphic to an object in the image of the function `F.obj`. In other words, this is the closure under isomorphism of the function `F.obj`. This is the "non-evil" way of describing the image of a functor. -/ def
essImage: C β₯€ D β†’ Set D
essImage
(
F: C β₯€ D
F
:
C: Type u₁
C
β₯€
D: Type uβ‚‚
D
) :
Set: Type ?u.70 β†’ Type ?u.70
Set
D: Type uβ‚‚
D
:= fun
Y: ?m.75
Y
=> βˆƒ
X: C
X
:
C: Type u₁
C
,
Nonempty: Sort ?u.81 β†’ Prop
Nonempty
(
F: C β₯€ D
F
.
obj: {V : Type ?u.119} β†’ [inst : Quiver V] β†’ {W : Type ?u.118} β†’ [inst_1 : Quiver W] β†’ V β₯€q W β†’ V β†’ W
obj
X: C
X
β‰…
Y: ?m.75
Y
) #align category_theory.functor.ess_image
CategoryTheory.Functor.essImage: {C : Type u₁} β†’ {D : Type uβ‚‚} β†’ [inst : Category C] β†’ [inst_1 : Category D] β†’ C β₯€ D β†’ Set D
CategoryTheory.Functor.essImage
/-- Get the witnessing object that `Y` is in the subcategory given by `F`. -/ def
essImage.witness: {Y : D} β†’ Y ∈ essImage F β†’ C
essImage.witness
{
Y: D
Y
:
D: Type uβ‚‚
D
} (h :
Y: D
Y
∈
F: C β₯€ D
F
.
essImage: {C : Type ?u.229} β†’ {D : Type ?u.228} β†’ [inst : Category C] β†’ [inst_1 : Category D] β†’ C β₯€ D β†’ Set D
essImage
) :
C: Type u₁
C
:= h.
choose: {Ξ± : Sort ?u.270} β†’ {p : Ξ± β†’ Prop} β†’ (βˆƒ a, p a) β†’ Ξ±
choose
#align category_theory.functor.ess_image.witness
CategoryTheory.Functor.essImage.witness: {C : Type u₁} β†’ {D : Type uβ‚‚} β†’ [inst : Category C] β†’ [inst_1 : Category D] β†’ {F : C β₯€ D} β†’ {Y : D} β†’ Y ∈ essImage F β†’ C
CategoryTheory.Functor.essImage.witness
/-- Extract the isomorphism between `F.obj h.witness` and `Y` itself. -/ -- Porting note: in the next, the dot notation `h.witness` no longer works def
essImage.getIso: {Y : D} β†’ (h : Y ∈ essImage F) β†’ F.obj (witness h) β‰… Y
essImage.getIso
{
Y: D
Y
:
D: Type uβ‚‚
D
} (h :
Y: D
Y
∈
F: C β₯€ D
F
.
essImage: {C : Type ?u.433} β†’ {D : Type ?u.432} β†’ [inst : Category C] β†’ [inst_1 : Category D] β†’ C β₯€ D β†’ Set D
essImage
) :
F: C β₯€ D
F
.
obj: {V : Type ?u.500} β†’ [inst : Quiver V] β†’ {W : Type ?u.499} β†’ [inst_1 : Quiver W] β†’ V β₯€q W β†’ V β†’ W
obj
(
essImage.witness: {C : Type ?u.540} β†’ {D : Type ?u.539} β†’ [inst : Category C] β†’ [inst_1 : Category D] β†’ {F : C β₯€ D} β†’ {Y : D} β†’ Y ∈ essImage F β†’ C
essImage.witness
h) β‰…
Y: D
Y
:=
Classical.choice: {Ξ± : Sort ?u.596} β†’ Nonempty Ξ± β†’ Ξ±
Classical.choice
h.
choose_spec: βˆ€ {Ξ± : Sort ?u.598} {p : Ξ± β†’ Prop} (P : βˆƒ a, p a), p (Exists.choose P)
choose_spec
#align category_theory.functor.ess_image.get_iso
CategoryTheory.Functor.essImage.getIso: {C : Type u₁} β†’ {D : Type uβ‚‚} β†’ [inst : Category C] β†’ [inst_1 : Category D] β†’ {F : C β₯€ D} β†’ {Y : D} β†’ (h : Y ∈ essImage F) β†’ F.obj (essImage.witness h) β‰… Y
CategoryTheory.Functor.essImage.getIso
/-- Being in the essential image is a "hygienic" property: it is preserved under isomorphism. -/ theorem
essImage.ofIso: βˆ€ {Y Y' : D}, (Y β‰… Y') β†’ Y ∈ essImage F β†’ Y' ∈ essImage F
essImage.ofIso
{
Y: D
Y
Y': D
Y'
:
D: Type uβ‚‚
D
} (
h: Y β‰… Y'
h
:
Y: D
Y
β‰…
Y': D
Y'
) (hY :
Y: D
Y
∈
essImage: {C : Type ?u.764} β†’ {D : Type ?u.763} β†’ [inst : Category C] β†’ [inst_1 : Category D] β†’ C β₯€ D β†’ Set D
essImage
F: C β₯€ D
F
) :
Y': D
Y'
∈
essImage: {C : Type ?u.844} β†’ {D : Type ?u.843} β†’ [inst : Category C] β†’ [inst_1 : Category D] β†’ C β₯€ D β†’ Set D
essImage
F: C β₯€ D
F
:= hY.
imp: βˆ€ {Ξ± : Sort ?u.896} {p q : Ξ± β†’ Prop}, (βˆ€ (a : Ξ±), p a β†’ q a) β†’ (βˆƒ a, p a) β†’ βˆƒ a, q a
imp
fun
_: ?m.912
_
=>
Nonempty.map: βˆ€ {Ξ± : Sort ?u.914} {Ξ² : Sort ?u.915}, (Ξ± β†’ Ξ²) β†’ Nonempty Ξ± β†’ Nonempty Ξ²
Nonempty.map
(Β· β‰ͺ≫
h: Y β‰… Y'
h
) #align category_theory.functor.ess_image.of_iso
CategoryTheory.Functor.essImage.ofIso: βˆ€ {C : Type u₁} {D : Type uβ‚‚} [inst : Category C] [inst_1 : Category D] {F : C β₯€ D} {Y Y' : D}, (Y β‰… Y') β†’ Y ∈ essImage F β†’ Y' ∈ essImage F
CategoryTheory.Functor.essImage.ofIso
/-- If `Y` is in the essential image of `F` then it is in the essential image of `F'` as long as `F β‰… F'`. -/ theorem
essImage.ofNatIso: βˆ€ {C : Type u₁} {D : Type uβ‚‚} [inst : Category C] [inst_1 : Category D] {F F' : C β₯€ D}, (F β‰… F') β†’ βˆ€ {Y : D}, Y ∈ essImage F β†’ Y ∈ essImage F'
essImage.ofNatIso
{
F': C β₯€ D
F'
:
C: Type u₁
C
β₯€
D: Type uβ‚‚
D
} (
h: F β‰… F'
h
:
F: C β₯€ D
F
β‰…
F': C β₯€ D
F'
) {
Y: D
Y
:
D: Type uβ‚‚
D
} (hY :
Y: D
Y
∈
essImage: {C : Type ?u.1084} β†’ {D : Type ?u.1083} β†’ [inst : Category C] β†’ [inst_1 : Category D] β†’ C β₯€ D β†’ Set D
essImage
F: C β₯€ D
F
) :
Y: D
Y
∈
essImage: {C : Type ?u.1159} β†’ {D : Type ?u.1158} β†’ [inst : Category C] β†’ [inst_1 : Category D] β†’ C β₯€ D β†’ Set D
essImage
F': C β₯€ D
F'
:= hY.
imp: βˆ€ {Ξ± : Sort ?u.1211} {p q : Ξ± β†’ Prop}, (βˆ€ (a : Ξ±), p a β†’ q a) β†’ (βˆƒ a, p a) β†’ βˆƒ a, q a
imp
fun
X: ?m.1227
X
=>
Nonempty.map: βˆ€ {Ξ± : Sort ?u.1229} {Ξ² : Sort ?u.1230}, (Ξ± β†’ Ξ²) β†’ Nonempty Ξ± β†’ Nonempty Ξ²
Nonempty.map
fun
t: ?m.1240
t
=>
h: F β‰… F'
h
.
symm: {C : Type ?u.1268} β†’ [inst : Category C] β†’ {X Y : C} β†’ (X β‰… Y) β†’ (Y β‰… X)
symm
.
app: {C : Type ?u.1292} β†’ [inst : Category C] β†’ {D : Type ?u.1291} β†’ [inst_1 : Category D] β†’ {F G : C β₯€ D} β†’ (F β‰… G) β†’ (X : C) β†’ F.obj X β‰… G.obj X
app
X: ?m.1227
X
β‰ͺ≫
t: ?m.1240
t
#align category_theory.functor.ess_image.of_nat_iso
CategoryTheory.Functor.essImage.ofNatIso: βˆ€ {C : Type u₁} {D : Type uβ‚‚} [inst : Category C] [inst_1 : Category D] {F F' : C β₯€ D}, (F β‰… F') β†’ βˆ€ {Y : D}, Y ∈ essImage F β†’ Y ∈ essImage F'
CategoryTheory.Functor.essImage.ofNatIso
/-- Isomorphic functors have equal essential images. -/ theorem
essImage_eq_of_natIso: βˆ€ {C : Type u₁} {D : Type uβ‚‚} [inst : Category C] [inst_1 : Category D] {F F' : C β₯€ D}, (F β‰… F') β†’ essImage F = essImage F'
essImage_eq_of_natIso
{
F': C β₯€ D
F'
:
C: Type u₁
C
β₯€
D: Type uβ‚‚
D
} (
h: F β‰… F'
h
:
F: C β₯€ D
F
β‰…
F': C β₯€ D
F'
) :
essImage: {C : Type ?u.1431} β†’ {D : Type ?u.1430} β†’ [inst : Category C] β†’ [inst_1 : Category D] β†’ C β₯€ D β†’ Set D
essImage
F: C β₯€ D
F
=
essImage: {C : Type ?u.1450} β†’ {D : Type ?u.1449} β†’ [inst : Category C] β†’ [inst_1 : Category D] β†’ C β₯€ D β†’ Set D
essImage
F': C β₯€ D
F'
:=
funext: βˆ€ {Ξ± : Sort ?u.1470} {Ξ² : Ξ± β†’ Sort ?u.1469} {f g : (x : Ξ±) β†’ Ξ² x}, (βˆ€ (x : Ξ±), f x = g x) β†’ f = g
funext
fun
_: ?m.1482
_
=>
propext: βˆ€ {a b : Prop}, (a ↔ b) β†’ a = b
propext
⟨
essImage.ofNatIso: βˆ€ {C : Type ?u.1498} {D : Type ?u.1497} [inst : Category C] [inst_1 : Category D] {F F' : C β₯€ D}, (F β‰… F') β†’ βˆ€ {Y : D}, Y ∈ essImage F β†’ Y ∈ essImage F'
essImage.ofNatIso
h: F β‰… F'
h
,
essImage.ofNatIso: βˆ€ {C : Type ?u.1539} {D : Type ?u.1538} [inst : Category C] [inst_1 : Category D] {F F' : C β₯€ D}, (F β‰… F') β†’ βˆ€ {Y : D}, Y ∈ essImage F β†’ Y ∈ essImage F'
essImage.ofNatIso
h: F β‰… F'
h
.
symm: {C : Type ?u.1548} β†’ [inst : Category C] β†’ {X Y : C} β†’ (X β‰… Y) β†’ (Y β‰… X)
symm
⟩ #align category_theory.functor.ess_image_eq_of_nat_iso
CategoryTheory.Functor.essImage_eq_of_natIso: βˆ€ {C : Type u₁} {D : Type uβ‚‚} [inst : Category C] [inst_1 : Category D] {F F' : C β₯€ D}, (F β‰… F') β†’ essImage F = essImage F'
CategoryTheory.Functor.essImage_eq_of_natIso
/-- An object in the image is in the essential image. -/ theorem
obj_mem_essImage: βˆ€ {C : Type u₁} {D : Type uβ‚‚} [inst : Category C] [inst_1 : Category D] (F : D β₯€ C) (Y : D), F.obj Y ∈ essImage F
obj_mem_essImage
(
F: D β₯€ C
F
:
D: Type uβ‚‚
D
β₯€
C: Type u₁
C
) (
Y: D
Y
:
D: Type uβ‚‚
D
) :
F: D β₯€ C
F
.
obj: {V : Type ?u.1677} β†’ [inst : Quiver V] β†’ {W : Type ?u.1676} β†’ [inst_1 : Quiver W] β†’ V β₯€q W β†’ V β†’ W
obj
Y: D
Y
∈
essImage: {C : Type ?u.1717} β†’ {D : Type ?u.1716} β†’ [inst : Category C] β†’ [inst_1 : Category D] β†’ C β₯€ D β†’ Set D
essImage
F: D β₯€ C
F
:= ⟨
Y: D
Y
, ⟨
Iso.refl: {C : Type ?u.1792} β†’ [inst : Category C] β†’ (X : C) β†’ X β‰… X
Iso.refl
_: ?m.1794
_
⟩⟩ #align category_theory.functor.obj_mem_ess_image
CategoryTheory.Functor.obj_mem_essImage: βˆ€ {C : Type u₁} {D : Type uβ‚‚} [inst : Category C] [inst_1 : Category D] (F : D β₯€ C) (Y : D), F.obj Y ∈ essImage F
CategoryTheory.Functor.obj_mem_essImage
/-- The essential image of a functor, interpreted of a full subcategory of the target category. -/ -- Porting note: no hasNonEmptyInstance linter yet def
EssImageSubcategory: (F : C β₯€ D) β†’ ?m.1867 F
EssImageSubcategory
(
F: C β₯€ D
F
:
C: Type u₁
C
β₯€
D: Type uβ‚‚
D
) :=
FullSubcategory: {C : Type ?u.1870} β†’ (C β†’ Prop) β†’ Type ?u.1870
FullSubcategory
F: C β₯€ D
F
.
essImage: {C : Type ?u.1879} β†’ {D : Type ?u.1878} β†’ [inst : Category C] β†’ [inst_1 : Category D] β†’ C β₯€ D β†’ Set D
essImage
#align category_theory.functor.ess_image_subcategory
CategoryTheory.Functor.EssImageSubcategory: {C : Type u₁} β†’ {D : Type uβ‚‚} β†’ [inst : Category C] β†’ [inst_1 : Category D] β†’ C β₯€ D β†’ Type uβ‚‚
CategoryTheory.Functor.EssImageSubcategory
-- Porting note: `deriving Category` is not able to derive this instance
instance: {C : Type u₁} β†’ {D : Type uβ‚‚} β†’ [inst : Category C] β†’ [inst_1 : Category D] β†’ {F : C β₯€ D} β†’ Category (EssImageSubcategory F)
instance
:
Category: Type ?u.1937 β†’ Type (max?u.1937(?u.1938+1))
Category
(
EssImageSubcategory: {C : Type ?u.1940} β†’ {D : Type ?u.1939} β†’ [inst : Category C] β†’ [inst_1 : Category D] β†’ C β₯€ D β†’ Type ?u.1939
EssImageSubcategory
F: C β₯€ D
F
) := (
inferInstance: {Ξ± : Sort ?u.1997} β†’ [i : Ξ±] β†’ Ξ±
inferInstance
:
Category: Type ?u.1993 β†’ Type (max?u.1993(vβ‚‚+1))
Category
.{vβ‚‚} (
FullSubcategory: {C : Type ?u.1994} β†’ (C β†’ Prop) β†’ Type ?u.1994
FullSubcategory
_: ?m.1995 β†’ Prop
_
)) /-- The essential image as a subcategory has a fully faithful inclusion into the target category. -/ @[simps!] def
essImageInclusion: (F : C β₯€ D) β†’ EssImageSubcategory F β₯€ D
essImageInclusion
(
F: C β₯€ D
F
:
C: Type u₁
C
β₯€
D: Type uβ‚‚
D
) :
F: C β₯€ D
F
.
EssImageSubcategory: {C : Type ?u.2166} β†’ {D : Type ?u.2165} β†’ [inst : Category C] β†’ [inst_1 : Category D] β†’ C β₯€ D β†’ Type ?u.2165
EssImageSubcategory
β₯€
D: Type uβ‚‚
D
:=
fullSubcategoryInclusion: {C : Type ?u.2220} β†’ [inst : Category C] β†’ (Z : C β†’ Prop) β†’ FullSubcategory Z β₯€ C
fullSubcategoryInclusion
_: ?m.2222 β†’ Prop
_
#align category_theory.functor.ess_image_inclusion
CategoryTheory.Functor.essImageInclusion: {C : Type u₁} β†’ {D : Type uβ‚‚} β†’ [inst : Category C] β†’ [inst_1 : Category D] β†’ (F : C β₯€ D) β†’ EssImageSubcategory F β₯€ D
CategoryTheory.Functor.essImageInclusion
#align category_theory.functor.ess_image_inclusion_obj
CategoryTheory.Functor.essImageInclusion_obj: βˆ€ {C : Type u₁} {D : Type uβ‚‚} [inst : Category C] [inst_1 : Category D] (F : C β₯€ D) (self : FullSubcategory (essImage F)), (essImageInclusion F).obj self = self.obj
CategoryTheory.Functor.essImageInclusion_obj
#align category_theory.functor.ess_image_inclusion_map
CategoryTheory.Functor.essImageInclusion_map: βˆ€ {C : Type u₁} {D : Type uβ‚‚} [inst : Category C] [inst_1 : Category D] (F : C β₯€ D) {X Y : InducedCategory D FullSubcategory.obj} (f : X ⟢ Y), (essImageInclusion F).map f = f
CategoryTheory.Functor.essImageInclusion_map
-- Porting note: `deriving Full` is not able to derive this instance
instance: {C : Type u₁} β†’ {D : Type uβ‚‚} β†’ [inst : Category C] β†’ [inst_1 : Category D] β†’ {F : C β₯€ D} β†’ Full (essImageInclusion F)
instance
:
Full: {C : Type ?u.2390} β†’ [inst : Category C] β†’ {D : Type ?u.2389} β†’ [inst_1 : Category D] β†’ C β₯€ D β†’ Type (max(max?u.2390?u.2392)?u.2391)
Full
(
essImageInclusion: {C : Type ?u.2434} β†’ {D : Type ?u.2433} β†’ [inst : Category C] β†’ [inst_1 : Category D] β†’ (F : C β₯€ D) β†’ EssImageSubcategory F β₯€ D
essImageInclusion
F: C β₯€ D
F
) := (
inferInstance: {Ξ± : Sort ?u.2726} β†’ [i : Ξ±] β†’ Ξ±
inferInstance
:
Full: {C : Type ?u.2493} β†’ [inst : Category C] β†’ {D : Type ?u.2492} β†’ [inst_1 : Category D] β†’ C β₯€ D β†’ Type (max(max?u.2493?u.2495)?u.2494)
Full
(
fullSubcategoryInclusion: {C : Type ?u.2536} β†’ [inst : Category C] β†’ (Z : C β†’ Prop) β†’ FullSubcategory Z β₯€ C
fullSubcategoryInclusion
_: ?m.2538 β†’ Prop
_
)) -- Porting note: `deriving Faithful` is not able to derive this instance
instance: βˆ€ {C : Type u₁} {D : Type uβ‚‚} [inst : Category C] [inst_1 : Category D] {F : C β₯€ D}, Faithful (essImageInclusion F)
instance
:
Faithful: {C : Type ?u.2957} β†’ [inst : Category C] β†’ {D : Type ?u.2956} β†’ [inst_1 : Category D] β†’ C β₯€ D β†’ Prop
Faithful
(
essImageInclusion: {C : Type ?u.3001} β†’ {D : Type ?u.3000} β†’ [inst : Category C] β†’ [inst_1 : Category D] β†’ (F : C β₯€ D) β†’ EssImageSubcategory F β₯€ D
essImageInclusion
F: C β₯€ D
F
) := (
inferInstance: βˆ€ {Ξ± : Sort ?u.3293} [i : Ξ±], Ξ±
inferInstance
:
Faithful: {C : Type ?u.3060} β†’ [inst : Category C] β†’ {D : Type ?u.3059} β†’ [inst_1 : Category D] β†’ C β₯€ D β†’ Prop
Faithful
(
fullSubcategoryInclusion: {C : Type ?u.3103} β†’ [inst : Category C] β†’ (Z : C β†’ Prop) β†’ FullSubcategory Z β₯€ C
fullSubcategoryInclusion
_: ?m.3105 β†’ Prop
_
)) /-- Given a functor `F : C β₯€ D`, we have an (essentially surjective) functor from `C` to the essential image of `F`. -/ @[simps!] def
toEssImage: (F : C β₯€ D) β†’ C β₯€ EssImageSubcategory F
toEssImage
(
F: C β₯€ D
F
:
C: Type u₁
C
β₯€
D: Type uβ‚‚
D
) :
C: Type u₁
C
β₯€
F: C β₯€ D
F
.
EssImageSubcategory: {C : Type ?u.3503} β†’ {D : Type ?u.3502} β†’ [inst : Category C] β†’ [inst_1 : Category D] β†’ C β₯€ D β†’ Type ?u.3502
EssImageSubcategory
:=
FullSubcategory.lift: {C : Type ?u.3557} β†’ [inst : Category C] β†’ {D : Type ?u.3556} β†’ [inst_1 : Category D] β†’ (P : D β†’ Prop) β†’ (F : C β₯€ D) β†’ (βˆ€ (X : C), P (F.obj X)) β†’ C β₯€ FullSubcategory P
FullSubcategory.lift
_: ?m.3562 β†’ Prop
_
F: C β₯€ D
F
(
obj_mem_essImage: βˆ€ {C : Type ?u.3612} {D : Type ?u.3611} [inst : Category C] [inst_1 : Category D] (F : D β₯€ C) (Y : D), F.obj Y ∈ essImage F
obj_mem_essImage
_: ?m.3616 β₯€ ?m.3615
_
) #align category_theory.functor.to_ess_image
CategoryTheory.Functor.toEssImage: {C : Type u₁} β†’ {D : Type uβ‚‚} β†’ [inst : Category C] β†’ [inst_1 : Category D] β†’ (F : C β₯€ D) β†’ C β₯€ EssImageSubcategory F
CategoryTheory.Functor.toEssImage
#align category_theory.functor.to_ess_image_map
CategoryTheory.Functor.toEssImage_map: βˆ€ {C : Type u₁} {D : Type uβ‚‚} [inst : Category C] [inst_1 : Category D] (F : C β₯€ D) {X Y : C} (f : X ⟢ Y), (toEssImage F).map f = F.map f
CategoryTheory.Functor.toEssImage_map
#align category_theory.functor.to_ess_image_obj_obj
CategoryTheory.Functor.toEssImage_obj_obj: βˆ€ {C : Type u₁} {D : Type uβ‚‚} [inst : Category C] [inst_1 : Category D] (F : C β₯€ D) (X : C), ((toEssImage F).obj X).obj = F.obj X
CategoryTheory.Functor.toEssImage_obj_obj
/-- The functor `F` factorises through its essential image, where the first functor is essentially surjective and the second is fully faithful. -/ @[simps!] def
toEssImageCompEssentialImageInclusion: {C : Type u₁} β†’ {D : Type uβ‚‚} β†’ [inst : Category C] β†’ [inst_1 : Category D] β†’ (F : C β₯€ D) β†’ toEssImage F β‹™ essImageInclusion F β‰… F
toEssImageCompEssentialImageInclusion
(
F: C β₯€ D
F
:
C: Type u₁
C
β₯€
D: Type uβ‚‚
D
) :
F: C β₯€ D
F
.
toEssImage: {C : Type ?u.3974} β†’ {D : Type ?u.3973} β†’ [inst : Category C] β†’ [inst_1 : Category D] β†’ (F : C β₯€ D) β†’ C β₯€ EssImageSubcategory F
toEssImage
β‹™
F: C β₯€ D
F
.
essImageInclusion: {C : Type ?u.4003} β†’ {D : Type ?u.4002} β†’ [inst : Category C] β†’ [inst_1 : Category D] β†’ (F : C β₯€ D) β†’ EssImageSubcategory F β₯€ D
essImageInclusion
β‰…
F: C β₯€ D
F
:=
FullSubcategory.lift_comp_inclusion: {C : Type ?u.4070} β†’ [inst : Category C] β†’ {D : Type ?u.4069} β†’ [inst_1 : Category D] β†’ (P : D β†’ Prop) β†’ (F : C β₯€ D) β†’ (hF : βˆ€ (X : C), P (F.obj X)) β†’ FullSubcategory.lift P F hF β‹™ fullSubcategoryInclusion P β‰… F
FullSubcategory.lift_comp_inclusion
_: ?m.4075 β†’ Prop
_
_: ?m.4073 β₯€ ?m.4075
_
_: βˆ€ (X : ?m.4073), ?m.4077 (?m.4078.obj X)
_
#align category_theory.functor.to_ess_image_comp_essential_image_inclusion
CategoryTheory.Functor.toEssImageCompEssentialImageInclusion: {C : Type u₁} β†’ {D : Type uβ‚‚} β†’ [inst : Category C] β†’ [inst_1 : Category D] β†’ (F : C β₯€ D) β†’ toEssImage F β‹™ essImageInclusion F β‰… F
CategoryTheory.Functor.toEssImageCompEssentialImageInclusion
#align category_theory.functor.to_ess_image_comp_essential_image_inclusion_hom_app
CategoryTheory.Functor.toEssImageCompEssentialImageInclusion_hom_app: βˆ€ {C : Type u₁} {D : Type uβ‚‚} [inst : Category C] [inst_1 : Category D] (F : C β₯€ D) (X : C), (toEssImageCompEssentialImageInclusion F).hom.app X = πŸ™ (F.obj X)
CategoryTheory.Functor.toEssImageCompEssentialImageInclusion_hom_app
#align category_theory.functor.to_ess_image_comp_essential_image_inclusion_inv_app
CategoryTheory.Functor.toEssImageCompEssentialImageInclusion_inv_app: βˆ€ {C : Type u₁} {D : Type uβ‚‚} [inst : Category C] [inst_1 : Category D] (F : C β₯€ D) (X : C), (toEssImageCompEssentialImageInclusion F).inv.app X = πŸ™ (F.obj X)
CategoryTheory.Functor.toEssImageCompEssentialImageInclusion_inv_app
end Functor /-- A functor `F : C β₯€ D` is essentially surjective if every object of `D` is in the essential image of `F`. In other words, for every `Y : D`, there is some `X : C` with `F.obj X β‰… Y`. See . -/ class
EssSurj: {C : Type u₁} β†’ {D : Type uβ‚‚} β†’ [inst : Category C] β†’ [inst_1 : Category D] β†’ C β₯€ D β†’ Prop
EssSurj
(
F: C β₯€ D
F
:
C: Type u₁
C
β₯€
D: Type uβ‚‚
D
) :
Prop: Type
Prop
where /-- All the objects of the target category are in the essential image. -/
mem_essImage: βˆ€ {C : Type u₁} {D : Type uβ‚‚} [inst : Category C] [inst_1 : Category D] {F : C β₯€ D} [self : EssSurj F] (Y : D), Y ∈ Functor.essImage F
mem_essImage
(
Y: D
Y
:
D: Type uβ‚‚
D
) :
Y: D
Y
∈
F: C β₯€ D
F
.
essImage: {C : Type ?u.4873} β†’ {D : Type ?u.4872} β†’ [inst : Category C] β†’ [inst_1 : Category D] β†’ C β₯€ D β†’ Set D
essImage
#align category_theory.ess_surj
CategoryTheory.EssSurj: {C : Type u₁} β†’ {D : Type uβ‚‚} β†’ [inst : Category C] β†’ [inst_1 : Category D] β†’ C β₯€ D β†’ Prop
CategoryTheory.EssSurj
instance: βˆ€ {C : Type u₁} {D : Type uβ‚‚} [inst : Category C] [inst_1 : Category D] {F : C β₯€ D}, EssSurj (Functor.toEssImage F)
instance
:
EssSurj: {C : Type ?u.4965} β†’ {D : Type ?u.4964} β†’ [inst : Category C] β†’ [inst_1 : Category D] β†’ C β₯€ D β†’ Prop
EssSurj
F: C β₯€ D
F
.
toEssImage: {C : Type ?u.5009} β†’ {D : Type ?u.5008} β†’ [inst : Category C] β†’ [inst_1 : Category D] β†’ (F : C β₯€ D) β†’ C β₯€ Functor.EssImageSubcategory F
toEssImage
where mem_essImage := fun ⟨_,
hY: Functor.essImage F obj✝
hY
⟩ => ⟨
_: ?m.5119
_
, ⟨⟨
_: ?m.5144 ⟢ ?m.5145
_
,
_: ?m.5145 ⟢ ?m.5144
_
,
hY: Functor.essImage F obj✝
hY
.
getIso: {C : Type ?u.5172} β†’ {D : Type ?u.5171} β†’ [inst : Category C] β†’ [inst_1 : Category D] β†’ {F : C β₯€ D} β†’ {Y : D} β†’ (h : Y ∈ Functor.essImage F) β†’ F.obj (Functor.essImage.witness h) β‰… Y
getIso
.
hom_inv_id: βˆ€ {C : Type ?u.5199} [inst : Category C] {X Y : C} (self : X β‰… Y), self.hom ≫ self.inv = πŸ™ X
hom_inv_id
,
hY: Functor.essImage F obj✝
hY
.
getIso: {C : Type ?u.5234} β†’ {D : Type ?u.5233} β†’ [inst : Category C] β†’ [inst_1 : Category D] β†’ {F : C β₯€ D} β†’ {Y : D} β†’ (h : Y ∈ Functor.essImage F) β†’ F.obj (Functor.essImage.witness h) β‰… Y
getIso
.
inv_hom_id: βˆ€ {C : Type ?u.5250} [inst : Category C] {X Y : C} (self : X β‰… Y), self.inv ≫ self.hom = πŸ™ Y
inv_hom_id
⟩⟩⟩ variable (
F: ?m.5407
F
) [
EssSurj: {C : Type ?u.6180} β†’ {D : Type ?u.6179} β†’ [inst : Category C] β†’ [inst_1 : Category D] β†’ C β₯€ D β†’ Prop
EssSurj
F: ?m.5407
F
] /-- Given an essentially surjective functor, we can find a preimage for every object `Y` in the codomain. Applying the functor to this preimage will yield an object isomorphic to `Y`, see `obj_obj_preimage_iso`. -/ def
Functor.objPreimage: {C : Type u₁} β†’ {D : Type uβ‚‚} β†’ [inst : Category C] β†’ [inst_1 : Category D] β†’ (F : C β₯€ D) β†’ [inst : EssSurj F] β†’ D β†’ C
Functor.objPreimage
(
Y: D
Y
:
D: Type uβ‚‚
D
) :
C: Type u₁
C
:=
essImage.witness: {C : Type ?u.5623} β†’ {D : Type ?u.5622} β†’ [inst : Category C] β†’ [inst_1 : Category D] β†’ {F : C β₯€ D} β†’ {Y : D} β†’ Y ∈ essImage F β†’ C
essImage.witness
(@
EssSurj.mem_essImage: βˆ€ {C : Type ?u.5669} {D : Type ?u.5668} [inst : Category C] [inst_1 : Category D] {F : C β₯€ D} [self : EssSurj F] (Y : D), Y ∈ essImage F
EssSurj.mem_essImage
_: Type ?u.5669
_
_: Type ?u.5668
_
_ _
F: C β₯€ D
F
_
Y: D
Y
) #align category_theory.functor.obj_preimage
CategoryTheory.Functor.objPreimage: {C : Type u₁} β†’ {D : Type uβ‚‚} β†’ [inst : Category C] β†’ [inst_1 : Category D] β†’ (F : C β₯€ D) β†’ [inst : EssSurj F] β†’ D β†’ C
CategoryTheory.Functor.objPreimage
/-- Applying an essentially surjective functor to a preimage of `Y` yields an object that is isomorphic to `Y`. -/ def
Functor.objObjPreimageIso: (Y : D) β†’ F.obj (objPreimage F Y) β‰… Y
Functor.objObjPreimageIso
(
Y: D
Y
:
D: Type uβ‚‚
D
) :
F: C β₯€ D
F
.
obj: {V : Type ?u.5944} β†’ [inst : Quiver V] β†’ {W : Type ?u.5943} β†’ [inst_1 : Quiver W] β†’ V β₯€q W β†’ V β†’ W
obj
(
F: C β₯€ D
F
.
objPreimage: {C : Type ?u.5984} β†’ {D : Type ?u.5983} β†’ [inst : Category C] β†’ [inst_1 : Category D] β†’ (F : C β₯€ D) β†’ [inst : EssSurj F] β†’ D β†’ C
objPreimage
Y: D
Y
) β‰…
Y: D
Y
:=
Functor.essImage.getIso: {C : Type ?u.6018} β†’ {D : Type ?u.6017} β†’ [inst : Category C] β†’ [inst_1 : Category D] β†’ {F : C β₯€ D} β†’ {Y : D} β†’ (h : Y ∈ essImage F) β†’ F.obj (essImage.witness h) β‰… Y
Functor.essImage.getIso
_: ?m.6026 ∈ essImage ?m.6025
_
#align category_theory.functor.obj_obj_preimage_iso
CategoryTheory.Functor.objObjPreimageIso: {C : Type u₁} β†’ {D : Type uβ‚‚} β†’ [inst : Category C] β†’ [inst_1 : Category D] β†’ (F : C β₯€ D) β†’ [inst_2 : EssSurj F] β†’ (Y : D) β†’ F.obj (Functor.objPreimage F Y) β‰… Y
CategoryTheory.Functor.objObjPreimageIso
/-- The induced functor of a faithful functor is faithful -/ instance
Faithful.toEssImage: βˆ€ (F : C β₯€ D) [inst : Faithful F], Faithful (Functor.toEssImage F)
Faithful.toEssImage
(
F: C β₯€ D
F
:
C: Type u₁
C
β₯€
D: Type uβ‚‚
D
) [
Faithful: {C : Type ?u.6256} β†’ [inst : Category C] β†’ {D : Type ?u.6255} β†’ [inst_1 : Category D] β†’ C β₯€ D β†’ Prop
Faithful
F: C β₯€ D
F
] :
Faithful: {C : Type ?u.6316} β†’ [inst : Category C] β†’ {D : Type ?u.6315} β†’ [inst_1 : Category D] β†’ C β₯€ D β†’ Prop
Faithful
F: C β₯€ D
F
.
toEssImage: {C : Type ?u.6360} β†’ {D : Type ?u.6359} β†’ [inst : Category C] β†’ [inst_1 : Category D] β†’ (F : C β₯€ D) β†’ C β₯€ Functor.EssImageSubcategory F
toEssImage
:=
Faithful.of_comp_iso: βˆ€ {C : Type ?u.6410} [inst : Category C] {D : Type ?u.6409} [inst_1 : Category D] {E : Type ?u.6408} [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
F: C β₯€ D
F
.
toEssImageCompEssentialImageInclusion: {C : Type ?u.6515} β†’ {D : Type ?u.6514} β†’ [inst : Category C] β†’ [inst_1 : Category D] β†’ (F : C β₯€ D) β†’ Functor.toEssImage F β‹™ Functor.essImageInclusion F β‰… F
toEssImageCompEssentialImageInclusion
#align category_theory.faithful.to_ess_image
CategoryTheory.Faithful.toEssImage: βˆ€ {C : Type u₁} {D : Type uβ‚‚} [inst : Category C] [inst_1 : Category D] (F : C β₯€ D) [inst_2 : Faithful F], Faithful (Functor.toEssImage F)
CategoryTheory.Faithful.toEssImage
/-- The induced functor of a full functor is full -/ instance
Full.toEssImage: (F : C β₯€ D) β†’ [inst : Full F] β†’ Full (Functor.toEssImage F)
Full.toEssImage
(
F: C β₯€ D
F
:
C: Type u₁
C
β₯€
D: Type uβ‚‚
D
) [
Full: {C : Type ?u.6730} β†’ [inst : Category C] β†’ {D : Type ?u.6729} β†’ [inst_1 : Category D] β†’ C β₯€ D β†’ Type (max(max?u.6730?u.6732)?u.6731)
Full
F: C β₯€ D
F
] :
Full: {C : Type ?u.6790} β†’ [inst : Category C] β†’ {D : Type ?u.6789} β†’ [inst_1 : Category D] β†’ C β₯€ D β†’ Type (max(max?u.6790?u.6792)?u.6791)
Full
F: C β₯€ D
F
.
toEssImage: {C : Type ?u.6834} β†’ {D : Type ?u.6833} β†’ [inst : Category C] β†’ [inst_1 : Category D] β†’ (F : C β₯€ D) β†’ C β₯€ Functor.EssImageSubcategory F
toEssImage
:= haveI :=
Full.ofIso: {C : Type ?u.6885} β†’ [inst : Category C] β†’ {D : Type ?u.6884} β†’ [inst_1 : Category D] β†’ {F F' : C β₯€ D} β†’ [inst_2 : Full F] β†’ (F β‰… F') β†’ Full F'
Full.ofIso
F: C β₯€ D
F
.
toEssImageCompEssentialImageInclusion: {C : Type ?u.6961} β†’ {D : Type ?u.6960} β†’ [inst : Category C] β†’ [inst_1 : Category D] β†’ (F : C β₯€ D) β†’ Functor.toEssImage F β‹™ Functor.essImageInclusion F β‰… F
toEssImageCompEssentialImageInclusion
.
symm: {C : Type ?u.6972} β†’ [inst : Category C] β†’ {X Y : C} β†’ (X β‰… Y) β†’ (Y β‰… X)
symm
Full.ofCompFaithful: {C : Type ?u.7032} β†’ [inst : Category C] β†’ {D : Type ?u.7031} β†’ [inst_1 : Category D] β†’ {E : Type ?u.7030} β†’ [inst_2 : Category E] β†’ (F : C β₯€ D) β†’ (G : D β₯€ E) β†’ [inst_3 : Full (F β‹™ G)] β†’ [inst_4 : Faithful G] β†’ Full F
Full.ofCompFaithful
F: C β₯€ D
F
.
toEssImage: {C : Type ?u.7043} β†’ {D : Type ?u.7042} β†’ [inst : Category C] β†’ [inst_1 : Category D] β†’ (F : C β₯€ D) β†’ C β₯€ Functor.EssImageSubcategory F
toEssImage
F: C β₯€ D
F
.
essImageInclusion: {C : Type ?u.7096} β†’ {D : Type ?u.7095} β†’ [inst : Category C] β†’ [inst_1 : Category D] β†’ (F : C β₯€ D) β†’ Functor.EssImageSubcategory F β₯€ D
essImageInclusion
#align category_theory.full.to_ess_image
CategoryTheory.Full.toEssImage: {C : Type u₁} β†’ {D : Type uβ‚‚} β†’ [inst : Category C] β†’ [inst_1 : Category D] β†’ (F : C β₯€ D) β†’ [inst_2 : Full F] β†’ Full (Functor.toEssImage F)
CategoryTheory.Full.toEssImage
end CategoryTheory