Categorical images #
We define the categorical image of f as a factorisation f = e ≫ m through a monomorphism m,
so that m factors through the m' in any other such factorisation.
Main definitions #
-
A
MonoFactorisationis a factorisationf = e ≫ m, wheremis a monomorphism -
IsImage Fmeans that a given mono factorisationFhas the universal property of the image. -
HasImage fmeans that there is some image factorization for the morphismf : X ⟶ Y. -
HasImages Cmeans that every morphism inChas an image. -
Let
f : X ⟶ Yandg : P ⟶ Qbe morphisms inC, which we will represent as objects of the arrow categoryarrow C. Thensq : f ⟶ gis a commutative square inC. Iffandghave images, thenHasImageMap sqrepresents the fact that there is a morphismi : image f ⟶ image gmaking the diagramX ----→ image f ----→ Y | | | | | | ↓ ↓ ↓ P ----→ image g ----→ Q
commute, where the top row is the image factorisation of
f, the bottom row is the image factorisation ofg, and the outer rectangle is the commutative squaresq. -
If a category
HasImages, thenHasImageMapsmeans that every commutative square admits an image map. -
If a category
HasImages, thenHasStrongEpiImagesmeans that the morphism to the image is always a strong epimorphism.
Main statements #
- When
Chas equalizers, the morphismeappearing in an image factorisation is an epimorphism. - When
Chas strong epi images, then these images admit image maps.
Future work #
- TODO: coimages, and abelian categories.
- TODO: connect this with existing working in the group theory and ring theory libraries.
structure
CategoryTheory.Limits.MonoFactorisation
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
:
Type (max u v)
A factorisation of a morphism f = e ≫ m, with m monic.
- I : C
- m : self.I ⟶ Y
- m_mono : CategoryTheory.Mono self.m
- e : X ⟶ self.I
- fac : CategoryTheory.CategoryStruct.comp self.e self.m = f
@[simp]
theorem
CategoryTheory.Limits.MonoFactorisation.fac_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
(self : CategoryTheory.Limits.MonoFactorisation f)
{Z : C}
(h : Y ⟶ Z)
:
def
CategoryTheory.Limits.MonoFactorisation.self
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Mono f]
:
The obvious factorisation of a monomorphism through itself.
instance
CategoryTheory.Limits.MonoFactorisation.instInhabitedMonoFactorisation
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Mono f]
:
Equations
theorem
CategoryTheory.Limits.MonoFactorisation.ext
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{F : CategoryTheory.Limits.MonoFactorisation f}
{F' : CategoryTheory.Limits.MonoFactorisation f}
(hI : F.I = F'.I)
(hm : F.m = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom hI) F'.m)
:
F = F'
The morphism m in a factorisation f = e ≫ m through a monomorphism is uniquely
determined.
@[simp]
theorem
CategoryTheory.Limits.MonoFactorisation.compMono_m
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
(F : CategoryTheory.Limits.MonoFactorisation f)
{Y' : C}
(g : Y ⟶ Y')
[CategoryTheory.Mono g]
:
@[simp]
theorem
CategoryTheory.Limits.MonoFactorisation.compMono_e
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
(F : CategoryTheory.Limits.MonoFactorisation f)
{Y' : C}
(g : Y ⟶ Y')
[CategoryTheory.Mono g]
:
(CategoryTheory.Limits.MonoFactorisation.compMono F g).e = F.e
@[simp]
theorem
CategoryTheory.Limits.MonoFactorisation.compMono_I
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
(F : CategoryTheory.Limits.MonoFactorisation f)
{Y' : C}
(g : Y ⟶ Y')
[CategoryTheory.Mono g]
:
(CategoryTheory.Limits.MonoFactorisation.compMono F g).I = F.I
def
CategoryTheory.Limits.MonoFactorisation.compMono
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
(F : CategoryTheory.Limits.MonoFactorisation f)
{Y' : C}
(g : Y ⟶ Y')
[CategoryTheory.Mono g]
:
Any mono factorisation of f gives a mono factorisation of f ≫ g when g is a mono.
Equations
@[simp]
theorem
CategoryTheory.Limits.MonoFactorisation.ofCompIso_I
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{Y' : C}
{g : Y ⟶ Y'}
[CategoryTheory.IsIso g]
(F : CategoryTheory.Limits.MonoFactorisation (CategoryTheory.CategoryStruct.comp f g))
:
@[simp]
theorem
CategoryTheory.Limits.MonoFactorisation.ofCompIso_m
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{Y' : C}
{g : Y ⟶ Y'}
[CategoryTheory.IsIso g]
(F : CategoryTheory.Limits.MonoFactorisation (CategoryTheory.CategoryStruct.comp f g))
:
@[simp]
theorem
CategoryTheory.Limits.MonoFactorisation.ofCompIso_e
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{Y' : C}
{g : Y ⟶ Y'}
[CategoryTheory.IsIso g]
(F : CategoryTheory.Limits.MonoFactorisation (CategoryTheory.CategoryStruct.comp f g))
:
def
CategoryTheory.Limits.MonoFactorisation.ofCompIso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{Y' : C}
{g : Y ⟶ Y'}
[CategoryTheory.IsIso g]
(F : CategoryTheory.Limits.MonoFactorisation (CategoryTheory.CategoryStruct.comp f g))
:
A mono factorisation of f ≫ g, where g is an isomorphism,
gives a mono factorisation of f.
@[simp]
theorem
CategoryTheory.Limits.MonoFactorisation.isoComp_e
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
(F : CategoryTheory.Limits.MonoFactorisation f)
{X' : C}
(g : X' ⟶ X)
:
@[simp]
theorem
CategoryTheory.Limits.MonoFactorisation.isoComp_m
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
(F : CategoryTheory.Limits.MonoFactorisation f)
{X' : C}
(g : X' ⟶ X)
:
(CategoryTheory.Limits.MonoFactorisation.isoComp F g).m = F.m
@[simp]
theorem
CategoryTheory.Limits.MonoFactorisation.isoComp_I
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
(F : CategoryTheory.Limits.MonoFactorisation f)
{X' : C}
(g : X' ⟶ X)
:
(CategoryTheory.Limits.MonoFactorisation.isoComp F g).I = F.I
def
CategoryTheory.Limits.MonoFactorisation.isoComp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
(F : CategoryTheory.Limits.MonoFactorisation f)
{X' : C}
(g : X' ⟶ X)
:
Any mono factorisation of f gives a mono factorisation of g ≫ f.
Equations
@[simp]
theorem
CategoryTheory.Limits.MonoFactorisation.ofIsoComp_e
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{X' : C}
(g : X' ⟶ X)
[CategoryTheory.IsIso g]
(F : CategoryTheory.Limits.MonoFactorisation (CategoryTheory.CategoryStruct.comp g f))
:
@[simp]
theorem
CategoryTheory.Limits.MonoFactorisation.ofIsoComp_I
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{X' : C}
(g : X' ⟶ X)
[CategoryTheory.IsIso g]
(F : CategoryTheory.Limits.MonoFactorisation (CategoryTheory.CategoryStruct.comp g f))
:
(CategoryTheory.Limits.MonoFactorisation.ofIsoComp g F).I = F.I
@[simp]
theorem
CategoryTheory.Limits.MonoFactorisation.ofIsoComp_m
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{X' : C}
(g : X' ⟶ X)
[CategoryTheory.IsIso g]
(F : CategoryTheory.Limits.MonoFactorisation (CategoryTheory.CategoryStruct.comp g f))
:
(CategoryTheory.Limits.MonoFactorisation.ofIsoComp g F).m = F.m
def
CategoryTheory.Limits.MonoFactorisation.ofIsoComp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{X' : C}
(g : X' ⟶ X)
[CategoryTheory.IsIso g]
(F : CategoryTheory.Limits.MonoFactorisation (CategoryTheory.CategoryStruct.comp g f))
:
A mono factorisation of g ≫ f, where g is an isomorphism,
gives a mono factorisation of f.
Equations
@[simp]
theorem
CategoryTheory.Limits.MonoFactorisation.ofArrowIso_I
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f : CategoryTheory.Arrow C}
{g : CategoryTheory.Arrow C}
(F : CategoryTheory.Limits.MonoFactorisation f.hom)
(sq : f ⟶ g)
[CategoryTheory.IsIso sq]
:
(CategoryTheory.Limits.MonoFactorisation.ofArrowIso F sq).I = F.I
@[simp]
theorem
CategoryTheory.Limits.MonoFactorisation.ofArrowIso_e
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f : CategoryTheory.Arrow C}
{g : CategoryTheory.Arrow C}
(F : CategoryTheory.Limits.MonoFactorisation f.hom)
(sq : f ⟶ g)
[CategoryTheory.IsIso sq]
:
(CategoryTheory.Limits.MonoFactorisation.ofArrowIso F sq).e = CategoryTheory.CategoryStruct.comp (CategoryTheory.inv sq.left) F.e
@[simp]
theorem
CategoryTheory.Limits.MonoFactorisation.ofArrowIso_m
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f : CategoryTheory.Arrow C}
{g : CategoryTheory.Arrow C}
(F : CategoryTheory.Limits.MonoFactorisation f.hom)
(sq : f ⟶ g)
[CategoryTheory.IsIso sq]
:
(CategoryTheory.Limits.MonoFactorisation.ofArrowIso F sq).m = CategoryTheory.CategoryStruct.comp F.m sq.right
def
CategoryTheory.Limits.MonoFactorisation.ofArrowIso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f : CategoryTheory.Arrow C}
{g : CategoryTheory.Arrow C}
(F : CategoryTheory.Limits.MonoFactorisation f.hom)
(sq : f ⟶ g)
[CategoryTheory.IsIso sq]
:
If f and g are isomorphic arrows, then a mono factorisation of f
gives a mono factorisation of g
Equations
- One or more equations did not get rendered due to their size.
structure
CategoryTheory.Limits.IsImage
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
(F : CategoryTheory.Limits.MonoFactorisation f)
:
Type (max u v)
Data exhibiting that a given factorisation through a mono is initial.
- lift : (F' : CategoryTheory.Limits.MonoFactorisation f) → F.I ⟶ F'.I
Data exhibiting that a given factorisation through a mono is initial.
- lift_fac : ∀ (F' : CategoryTheory.Limits.MonoFactorisation f), CategoryTheory.CategoryStruct.comp (self.lift F') F'.m = F.m
Data exhibiting that a given factorisation through a mono is initial.
@[simp]
theorem
CategoryTheory.Limits.IsImage.lift_fac_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{F : CategoryTheory.Limits.MonoFactorisation f}
(self : CategoryTheory.Limits.IsImage F)
(F' : CategoryTheory.Limits.MonoFactorisation f)
{Z : C}
(h : Y ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (self.lift F') (CategoryTheory.CategoryStruct.comp F'.m h) = CategoryTheory.CategoryStruct.comp F.m h
@[simp]
theorem
CategoryTheory.Limits.IsImage.fac_lift_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{F : CategoryTheory.Limits.MonoFactorisation f}
(hF : CategoryTheory.Limits.IsImage F)
(F' : CategoryTheory.Limits.MonoFactorisation f)
{Z : C}
(h : F'.I ⟶ Z)
:
CategoryTheory.CategoryStruct.comp F.e (CategoryTheory.CategoryStruct.comp (hF.lift F') h) = CategoryTheory.CategoryStruct.comp F'.e h
@[simp]
theorem
CategoryTheory.Limits.IsImage.fac_lift
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{F : CategoryTheory.Limits.MonoFactorisation f}
(hF : CategoryTheory.Limits.IsImage F)
(F' : CategoryTheory.Limits.MonoFactorisation f)
:
CategoryTheory.CategoryStruct.comp F.e (hF.lift F') = F'.e
@[simp]
theorem
CategoryTheory.Limits.IsImage.self_lift
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Mono f]
(F' : CategoryTheory.Limits.MonoFactorisation f)
:
(CategoryTheory.Limits.IsImage.self f).lift F' = F'.e
def
CategoryTheory.Limits.IsImage.self
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Mono f]
:
The trivial factorisation of a monomorphism satisfies the universal property.
Equations
- CategoryTheory.Limits.IsImage.self f = { lift := fun (F' : CategoryTheory.Limits.MonoFactorisation f) => F'.e, lift_fac := ⋯ }
instance
CategoryTheory.Limits.IsImage.instInhabitedIsImageSelf
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Mono f]
:
Equations
@[simp]
theorem
CategoryTheory.Limits.IsImage.isoExt_hom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{F : CategoryTheory.Limits.MonoFactorisation f}
{F' : CategoryTheory.Limits.MonoFactorisation f}
(hF : CategoryTheory.Limits.IsImage F)
(hF' : CategoryTheory.Limits.IsImage F')
:
(CategoryTheory.Limits.IsImage.isoExt hF hF').hom = hF.lift F'
@[simp]
theorem
CategoryTheory.Limits.IsImage.isoExt_inv
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{F : CategoryTheory.Limits.MonoFactorisation f}
{F' : CategoryTheory.Limits.MonoFactorisation f}
(hF : CategoryTheory.Limits.IsImage F)
(hF' : CategoryTheory.Limits.IsImage F')
:
(CategoryTheory.Limits.IsImage.isoExt hF hF').inv = hF'.lift F
def
CategoryTheory.Limits.IsImage.isoExt
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{F : CategoryTheory.Limits.MonoFactorisation f}
{F' : CategoryTheory.Limits.MonoFactorisation f}
(hF : CategoryTheory.Limits.IsImage F)
(hF' : CategoryTheory.Limits.IsImage F')
:
F.I ≅ F'.I
Two factorisations through monomorphisms satisfying the universal property must factor through isomorphic objects.
Equations
- CategoryTheory.Limits.IsImage.isoExt hF hF' = { hom := hF.lift F', inv := hF'.lift F, hom_inv_id := ⋯, inv_hom_id := ⋯ }
theorem
CategoryTheory.Limits.IsImage.isoExt_hom_m
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{F : CategoryTheory.Limits.MonoFactorisation f}
{F' : CategoryTheory.Limits.MonoFactorisation f}
(hF : CategoryTheory.Limits.IsImage F)
(hF' : CategoryTheory.Limits.IsImage F')
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.IsImage.isoExt hF hF').hom F'.m = F.m
theorem
CategoryTheory.Limits.IsImage.isoExt_inv_m
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{F : CategoryTheory.Limits.MonoFactorisation f}
{F' : CategoryTheory.Limits.MonoFactorisation f}
(hF : CategoryTheory.Limits.IsImage F)
(hF' : CategoryTheory.Limits.IsImage F')
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.IsImage.isoExt hF hF').inv F.m = F'.m
theorem
CategoryTheory.Limits.IsImage.e_isoExt_hom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{F : CategoryTheory.Limits.MonoFactorisation f}
{F' : CategoryTheory.Limits.MonoFactorisation f}
(hF : CategoryTheory.Limits.IsImage F)
(hF' : CategoryTheory.Limits.IsImage F')
:
CategoryTheory.CategoryStruct.comp F.e (CategoryTheory.Limits.IsImage.isoExt hF hF').hom = F'.e
theorem
CategoryTheory.Limits.IsImage.e_isoExt_inv
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{F : CategoryTheory.Limits.MonoFactorisation f}
{F' : CategoryTheory.Limits.MonoFactorisation f}
(hF : CategoryTheory.Limits.IsImage F)
(hF' : CategoryTheory.Limits.IsImage F')
:
CategoryTheory.CategoryStruct.comp F'.e (CategoryTheory.Limits.IsImage.isoExt hF hF').inv = F.e
@[simp]
theorem
CategoryTheory.Limits.IsImage.ofArrowIso_lift
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f : CategoryTheory.Arrow C}
{g : CategoryTheory.Arrow C}
{F : CategoryTheory.Limits.MonoFactorisation f.hom}
(hF : CategoryTheory.Limits.IsImage F)
(sq : f ⟶ g)
[CategoryTheory.IsIso sq]
(F' : CategoryTheory.Limits.MonoFactorisation g.hom)
:
(CategoryTheory.Limits.IsImage.ofArrowIso hF sq).lift F' = hF.lift (CategoryTheory.Limits.MonoFactorisation.ofArrowIso F' (CategoryTheory.inv sq))
def
CategoryTheory.Limits.IsImage.ofArrowIso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f : CategoryTheory.Arrow C}
{g : CategoryTheory.Arrow C}
{F : CategoryTheory.Limits.MonoFactorisation f.hom}
(hF : CategoryTheory.Limits.IsImage F)
(sq : f ⟶ g)
[CategoryTheory.IsIso sq]
:
If f and g are isomorphic arrows, then a mono factorisation of f that is an image
gives a mono factorisation of g that is an image
Equations
- One or more equations did not get rendered due to their size.
structure
CategoryTheory.Limits.ImageFactorisation
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
:
Type (max u v)
Data exhibiting that a morphism f has an image.
Data exhibiting that a morphism
fhas an image.- isImage : CategoryTheory.Limits.IsImage self.F
Data exhibiting that a morphism
fhas an image.
instance
CategoryTheory.Limits.ImageFactorisation.instInhabitedImageFactorisation
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Mono f]
:
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Limits.ImageFactorisation.ofArrowIso_F
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f : CategoryTheory.Arrow C}
{g : CategoryTheory.Arrow C}
(F : CategoryTheory.Limits.ImageFactorisation f.hom)
(sq : f ⟶ g)
[CategoryTheory.IsIso sq]
:
@[simp]
theorem
CategoryTheory.Limits.ImageFactorisation.ofArrowIso_isImage
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f : CategoryTheory.Arrow C}
{g : CategoryTheory.Arrow C}
(F : CategoryTheory.Limits.ImageFactorisation f.hom)
(sq : f ⟶ g)
[CategoryTheory.IsIso sq]
:
(CategoryTheory.Limits.ImageFactorisation.ofArrowIso F sq).isImage = CategoryTheory.Limits.IsImage.ofArrowIso F.isImage sq
def
CategoryTheory.Limits.ImageFactorisation.ofArrowIso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f : CategoryTheory.Arrow C}
{g : CategoryTheory.Arrow C}
(F : CategoryTheory.Limits.ImageFactorisation f.hom)
(sq : f ⟶ g)
[CategoryTheory.IsIso sq]
:
If f and g are isomorphic arrows, then an image factorisation of f
gives an image factorisation of g
Equations
- CategoryTheory.Limits.ImageFactorisation.ofArrowIso F sq = { F := CategoryTheory.Limits.MonoFactorisation.ofArrowIso F.F sq, isImage := CategoryTheory.Limits.IsImage.ofArrowIso F.isImage sq }
class
CategoryTheory.Limits.HasImage
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
:
has_image f means that there exists an image factorisation of f.
- mk' :: (
- exists_image : Nonempty (CategoryTheory.Limits.ImageFactorisation f)
has_image fmeans that there exists an image factorisation off. - )
Instances
- CategoryTheory.Limits.Types.instHasImageTypeTypes
- CategoryTheory.Limits.hasImage_comp_iso
- CategoryTheory.Limits.hasImage_iso_comp
- CategoryTheory.Limits.hasImage_zero
- CategoryTheory.Limits.instHasImageCompToCategoryStruct
- CategoryTheory.Limits.instHasImageObjToQuiverToCategoryStructToPrefunctorIdLeftMkRightHom
- CategoryTheory.Limits.mono_hasImage
theorem
CategoryTheory.Limits.HasImage.mk
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
(F : CategoryTheory.Limits.ImageFactorisation f)
:
theorem
CategoryTheory.Limits.HasImage.of_arrow_iso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f : CategoryTheory.Arrow C}
{g : CategoryTheory.Arrow C}
[h : CategoryTheory.Limits.HasImage f.hom]
(sq : f ⟶ g)
[CategoryTheory.IsIso sq]
:
instance
CategoryTheory.Limits.mono_hasImage
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Mono f]
:
Equations
- ⋯ = ⋯
def
CategoryTheory.Limits.Image.monoFactorisation
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasImage f]
:
Some factorisation of f through a monomorphism (selected with choice).
Equations
def
CategoryTheory.Limits.Image.isImage
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasImage f]
:
The witness of the universal property for the chosen factorisation of f through
a monomorphism.
Equations
- CategoryTheory.Limits.Image.isImage f = (Classical.choice ⋯).isImage
def
CategoryTheory.Limits.image
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasImage f]
:
C
The categorical image of a morphism.
Equations
def
CategoryTheory.Limits.image.ι
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasImage f]
:
The inclusion of the image of a morphism into the target.
Equations
Instances For
@[simp]
theorem
CategoryTheory.Limits.image.as_ι
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasImage f]
:
instance
CategoryTheory.Limits.instMonoImageι
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasImage f]
:
Equations
- ⋯ = ⋯
def
CategoryTheory.Limits.factorThruImage
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasImage f]
:
The map from the source to the image of a morphism.
Equations
Instances For
@[simp]
theorem
CategoryTheory.Limits.as_factorThruImage
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasImage f]
:
Rewrite in terms of the factorThruImage interface.
@[simp]
theorem
CategoryTheory.Limits.image.fac_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasImage f]
{Z : C}
(h : Y ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.image.fac
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasImage f]
:
def
CategoryTheory.Limits.image.lift
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
[CategoryTheory.Limits.HasImage f]
(F' : CategoryTheory.Limits.MonoFactorisation f)
:
CategoryTheory.Limits.image f ⟶ F'.I
Any other factorisation of the morphism f through a monomorphism receives a map from the
image.
Equations
- CategoryTheory.Limits.image.lift F' = (CategoryTheory.Limits.Image.isImage f).lift F'
Instances For
@[simp]
theorem
CategoryTheory.Limits.image.lift_fac_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
[CategoryTheory.Limits.HasImage f]
(F' : CategoryTheory.Limits.MonoFactorisation f)
{Z : C}
(h : Y ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.image.lift_fac
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
[CategoryTheory.Limits.HasImage f]
(F' : CategoryTheory.Limits.MonoFactorisation f)
:
@[simp]
theorem
CategoryTheory.Limits.image.fac_lift_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
[CategoryTheory.Limits.HasImage f]
(F' : CategoryTheory.Limits.MonoFactorisation f)
{Z : C}
(h : F'.I ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.image.fac_lift
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
[CategoryTheory.Limits.HasImage f]
(F' : CategoryTheory.Limits.MonoFactorisation f)
:
@[simp]
theorem
CategoryTheory.Limits.image.isImage_lift
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
[CategoryTheory.Limits.HasImage f]
(F : CategoryTheory.Limits.MonoFactorisation f)
:
@[simp]
theorem
CategoryTheory.Limits.IsImage.lift_ι_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
[CategoryTheory.Limits.HasImage f]
{F : CategoryTheory.Limits.MonoFactorisation f}
(hF : CategoryTheory.Limits.IsImage F)
{Z : C}
(h : Y ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.IsImage.lift_ι
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
[CategoryTheory.Limits.HasImage f]
{F : CategoryTheory.Limits.MonoFactorisation f}
(hF : CategoryTheory.Limits.IsImage F)
:
instance
CategoryTheory.Limits.image.lift_mono
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
[CategoryTheory.Limits.HasImage f]
(F' : CategoryTheory.Limits.MonoFactorisation f)
:
Equations
- ⋯ = ⋯
theorem
CategoryTheory.Limits.HasImage.uniq
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
[CategoryTheory.Limits.HasImage f]
(F' : CategoryTheory.Limits.MonoFactorisation f)
(l : CategoryTheory.Limits.image f ⟶ F'.I)
(w : CategoryTheory.CategoryStruct.comp l F'.m = CategoryTheory.Limits.image.ι f)
:
instance
CategoryTheory.Limits.instHasImageCompToCategoryStruct
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
[CategoryTheory.IsIso f]
(g : Y ⟶ Z)
[CategoryTheory.Limits.HasImage g]
:
If has_image g, then has_image (f ≫ g) when f is an isomorphism.
Equations
- ⋯ = ⋯
HasImages asserts that every morphism has an image.
- has_image : ∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.Limits.HasImage f
HasImagesasserts that every morphism has an image.
def
CategoryTheory.Limits.imageMonoIsoSource
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Mono f]
:
The image of a monomorphism is isomorphic to the source.
@[simp]
theorem
CategoryTheory.Limits.imageMonoIsoSource_inv_ι_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Mono f]
{Z : C}
(h : Y ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.imageMonoIsoSource_inv_ι
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Mono f]
:
@[simp]
theorem
CategoryTheory.Limits.imageMonoIsoSource_hom_self_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Mono f]
{Z : C}
(h : Y ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.imageMonoIsoSource_hom_self
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Mono f]
:
theorem
CategoryTheory.Limits.image.ext
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasImage f]
{W : C}
{g : CategoryTheory.Limits.image f ⟶ W}
{h : CategoryTheory.Limits.image f ⟶ W}
[CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.parallelPair g h)]
(w : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.factorThruImage f) g = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.factorThruImage f) h)
:
g = h
instance
CategoryTheory.Limits.instEpiImageFactorThruImage
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasImage f]
[∀ {Z : C} (g h : CategoryTheory.Limits.image f ⟶ Z),
CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.parallelPair g h)]
:
Equations
- ⋯ = ⋯
theorem
CategoryTheory.Limits.epi_image_of_epi
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasImage f]
[E : CategoryTheory.Epi f]
:
theorem
CategoryTheory.Limits.epi_of_epi_image
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasImage f]
[CategoryTheory.Epi (CategoryTheory.Limits.image.ι f)]
[CategoryTheory.Epi (CategoryTheory.Limits.factorThruImage f)]
:
def
CategoryTheory.Limits.image.eqToHom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{f' : X ⟶ Y}
[CategoryTheory.Limits.HasImage f]
[CategoryTheory.Limits.HasImage f']
(h : f = f')
:
An equation between morphisms gives a comparison map between the images (which momentarily we prove is an iso).
Equations
- One or more equations did not get rendered due to their size.
Instances For
instance
CategoryTheory.Limits.instIsIsoImageEqToHom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{f' : X ⟶ Y}
[CategoryTheory.Limits.HasImage f]
[CategoryTheory.Limits.HasImage f']
(h : f = f')
:
Equations
- ⋯ = ⋯
def
CategoryTheory.Limits.image.eqToIso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{f' : X ⟶ Y}
[CategoryTheory.Limits.HasImage f]
[CategoryTheory.Limits.HasImage f']
(h : f = f')
:
An equation between morphisms gives an isomorphism between the images.
theorem
CategoryTheory.Limits.image.eq_fac
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{f' : X ⟶ Y}
[CategoryTheory.Limits.HasImage f]
[CategoryTheory.Limits.HasImage f']
[CategoryTheory.Limits.HasEqualizers C]
(h : f = f')
:
As long as the category has equalizers,
the image inclusion maps commute with image.eqToIso.
def
CategoryTheory.Limits.image.preComp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
{Z : C}
(g : Y ⟶ Z)
[CategoryTheory.Limits.HasImage g]
[CategoryTheory.Limits.HasImage (CategoryTheory.CategoryStruct.comp f g)]
:
The comparison map image (f ≫ g) ⟶ image g.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Limits.image.preComp_ι_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
{Z : C}
(g : Y ⟶ Z✝)
[CategoryTheory.Limits.HasImage g]
[CategoryTheory.Limits.HasImage (CategoryTheory.CategoryStruct.comp f g)]
{Z : C}
(h : Z✝ ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.image.preComp_ι
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
{Z : C}
(g : Y ⟶ Z)
[CategoryTheory.Limits.HasImage g]
[CategoryTheory.Limits.HasImage (CategoryTheory.CategoryStruct.comp f g)]
:
@[simp]
theorem
CategoryTheory.Limits.image.factorThruImage_preComp_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
{Z : C}
(g : Y ⟶ Z✝)
[CategoryTheory.Limits.HasImage g]
[CategoryTheory.Limits.HasImage (CategoryTheory.CategoryStruct.comp f g)]
{Z : C}
(h : CategoryTheory.Limits.image g ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.factorThruImage (CategoryTheory.CategoryStruct.comp f g))
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.preComp f g) h) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.factorThruImage g) h)
@[simp]
theorem
CategoryTheory.Limits.image.factorThruImage_preComp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
{Z : C}
(g : Y ⟶ Z)
[CategoryTheory.Limits.HasImage g]
[CategoryTheory.Limits.HasImage (CategoryTheory.CategoryStruct.comp f g)]
:
instance
CategoryTheory.Limits.image.preComp_mono
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
{Z : C}
(g : Y ⟶ Z)
[CategoryTheory.Limits.HasImage g]
[CategoryTheory.Limits.HasImage (CategoryTheory.CategoryStruct.comp f g)]
:
image.preComp f g is a monomorphism.
Equations
- ⋯ = ⋯
theorem
CategoryTheory.Limits.image.preComp_comp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
{Z : C}
(g : Y ⟶ Z)
{W : C}
(h : Z ⟶ W)
[CategoryTheory.Limits.HasImage (CategoryTheory.CategoryStruct.comp g h)]
[CategoryTheory.Limits.HasImage (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h))]
[CategoryTheory.Limits.HasImage h]
[CategoryTheory.Limits.HasImage (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h)]
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.preComp f (CategoryTheory.CategoryStruct.comp g h))
(CategoryTheory.Limits.image.preComp g h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.eqToHom ⋯)
(CategoryTheory.Limits.image.preComp (CategoryTheory.CategoryStruct.comp f g) h)
The two step comparison map
image (f ≫ (g ≫ h)) ⟶ image (g ≫ h) ⟶ image h
agrees with the one step comparison map
image (f ≫ (g ≫ h)) ≅ image ((f ≫ g) ≫ h) ⟶ image h.
instance
CategoryTheory.Limits.image.preComp_epi_of_epi
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
{Z : C}
(g : Y ⟶ Z)
[CategoryTheory.Limits.HasEqualizers C]
[CategoryTheory.Limits.HasImage g]
[CategoryTheory.Limits.HasImage (CategoryTheory.CategoryStruct.comp f g)]
[CategoryTheory.Epi f]
:
image.preComp f g is an epimorphism when f is an epimorphism
(we need C to have equalizers to prove this).
Equations
- ⋯ = ⋯
instance
CategoryTheory.Limits.hasImage_iso_comp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
{Z : C}
(g : Y ⟶ Z)
[CategoryTheory.IsIso f]
[CategoryTheory.Limits.HasImage g]
:
Equations
- ⋯ = ⋯
instance
CategoryTheory.Limits.image.isIso_precomp_iso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(g : Y ⟶ Z)
[CategoryTheory.Limits.HasEqualizers C]
(f : X ⟶ Y)
[CategoryTheory.IsIso f]
[CategoryTheory.Limits.HasImage g]
:
image.preComp f g is an isomorphism when f is an isomorphism
(we need C to have equalizers to prove this).
Equations
- ⋯ = ⋯
instance
CategoryTheory.Limits.hasImage_comp_iso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
{Z : C}
(g : Y ⟶ Z)
[CategoryTheory.Limits.HasImage f]
[CategoryTheory.IsIso g]
:
Equations
- ⋯ = ⋯
def
CategoryTheory.Limits.image.compIso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
{Z : C}
(g : Y ⟶ Z)
[CategoryTheory.Limits.HasEqualizers C]
[CategoryTheory.Limits.HasImage f]
[CategoryTheory.IsIso g]
:
Postcomposing by an isomorphism induces an isomorphism on the image.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Limits.image.compIso_hom_comp_image_ι_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
{Z : C}
(g : Y ⟶ Z✝)
[CategoryTheory.Limits.HasEqualizers C]
[CategoryTheory.Limits.HasImage f]
[CategoryTheory.IsIso g]
{Z : C}
(h : Z✝ ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.compIso f g).hom
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι (CategoryTheory.CategoryStruct.comp f g)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι f) (CategoryTheory.CategoryStruct.comp g h)
@[simp]
theorem
CategoryTheory.Limits.image.compIso_hom_comp_image_ι
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
{Z : C}
(g : Y ⟶ Z)
[CategoryTheory.Limits.HasEqualizers C]
[CategoryTheory.Limits.HasImage f]
[CategoryTheory.IsIso g]
:
@[simp]
theorem
CategoryTheory.Limits.image.compIso_inv_comp_image_ι_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
{Z : C}
(g : Y ⟶ Z✝)
[CategoryTheory.Limits.HasEqualizers C]
[CategoryTheory.Limits.HasImage f]
[CategoryTheory.IsIso g]
{Z : C}
(h : Y ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.compIso f g).inv
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι f) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι (CategoryTheory.CategoryStruct.comp f g))
(CategoryTheory.CategoryStruct.comp (CategoryTheory.inv g) h)
@[simp]
theorem
CategoryTheory.Limits.image.compIso_inv_comp_image_ι
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
{Z : C}
(g : Y ⟶ Z)
[CategoryTheory.Limits.HasEqualizers C]
[CategoryTheory.Limits.HasImage f]
[CategoryTheory.IsIso g]
:
instance
CategoryTheory.Limits.instHasImageObjToQuiverToCategoryStructToPrefunctorIdLeftMkRightHom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasImage f]
:
Equations
- ⋯ = ⋯
structure
CategoryTheory.Limits.ImageMap
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f : CategoryTheory.Arrow C}
{g : CategoryTheory.Arrow C}
[CategoryTheory.Limits.HasImage f.hom]
[CategoryTheory.Limits.HasImage g.hom]
(sq : f ⟶ g)
:
Type v
An image map is a morphism image f → image g fitting into a commutative square and satisfying
the obvious commutativity conditions.
- map : CategoryTheory.Limits.image f.hom ⟶ CategoryTheory.Limits.image g.hom
- map_ι : CategoryTheory.CategoryStruct.comp self.map (CategoryTheory.Limits.image.ι g.hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι f.hom) sq.right
instance
CategoryTheory.Limits.inhabitedImageMap
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f : CategoryTheory.Arrow C}
[CategoryTheory.Limits.HasImage f.hom]
:
Equations
- CategoryTheory.Limits.inhabitedImageMap = { default := { map := CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.image f.hom), map_ι := ⋯ } }
@[simp]
theorem
CategoryTheory.Limits.ImageMap.map_ι_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f : CategoryTheory.Arrow C}
{g : CategoryTheory.Arrow C}
[CategoryTheory.Limits.HasImage f.hom]
[CategoryTheory.Limits.HasImage g.hom]
{sq : f ⟶ g}
(self : CategoryTheory.Limits.ImageMap sq)
{Z : C}
(h : g.right ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.ImageMap.factor_map_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f : CategoryTheory.Arrow C}
{g : CategoryTheory.Arrow C}
[CategoryTheory.Limits.HasImage f.hom]
[CategoryTheory.Limits.HasImage g.hom]
(sq : f ⟶ g)
(m : CategoryTheory.Limits.ImageMap sq)
{Z : C}
(h : CategoryTheory.Limits.image g.hom ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.ImageMap.factor_map
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f : CategoryTheory.Arrow C}
{g : CategoryTheory.Arrow C}
[CategoryTheory.Limits.HasImage f.hom]
[CategoryTheory.Limits.HasImage g.hom]
(sq : f ⟶ g)
(m : CategoryTheory.Limits.ImageMap sq)
:
def
CategoryTheory.Limits.ImageMap.transport
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f : CategoryTheory.Arrow C}
{g : CategoryTheory.Arrow C}
[CategoryTheory.Limits.HasImage f.hom]
[CategoryTheory.Limits.HasImage g.hom]
(sq : f ⟶ g)
(F : CategoryTheory.Limits.MonoFactorisation f.hom)
{F' : CategoryTheory.Limits.MonoFactorisation g.hom}
(hF' : CategoryTheory.Limits.IsImage F')
{map : F.I ⟶ F'.I}
(map_ι : CategoryTheory.CategoryStruct.comp map F'.m = CategoryTheory.CategoryStruct.comp F.m sq.right)
:
To give an image map for a commutative square with f at the top and g at the bottom, it
suffices to give a map between any mono factorisation of f and any image factorisation of
g.
Equations
- One or more equations did not get rendered due to their size.
class
CategoryTheory.Limits.HasImageMap
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f : CategoryTheory.Arrow C}
{g : CategoryTheory.Arrow C}
[CategoryTheory.Limits.HasImage f.hom]
[CategoryTheory.Limits.HasImage g.hom]
(sq : f ⟶ g)
:
HasImageMap sq means that there is an ImageMap for the square sq.
- mk' :: (
- has_image_map : Nonempty (CategoryTheory.Limits.ImageMap sq)
HasImageMap sqmeans that there is anImageMapfor the squaresq. - )
theorem
CategoryTheory.Limits.HasImageMap.mk
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f : CategoryTheory.Arrow C}
{g : CategoryTheory.Arrow C}
[CategoryTheory.Limits.HasImage f.hom]
[CategoryTheory.Limits.HasImage g.hom]
{sq : f ⟶ g}
(m : CategoryTheory.Limits.ImageMap sq)
:
theorem
CategoryTheory.Limits.HasImageMap.transport
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f : CategoryTheory.Arrow C}
{g : CategoryTheory.Arrow C}
[CategoryTheory.Limits.HasImage f.hom]
[CategoryTheory.Limits.HasImage g.hom]
(sq : f ⟶ g)
(F : CategoryTheory.Limits.MonoFactorisation f.hom)
{F' : CategoryTheory.Limits.MonoFactorisation g.hom}
(hF' : CategoryTheory.Limits.IsImage F')
(map : F.I ⟶ F'.I)
(map_ι : CategoryTheory.CategoryStruct.comp map F'.m = CategoryTheory.CategoryStruct.comp F.m sq.right)
:
def
CategoryTheory.Limits.HasImageMap.imageMap
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f : CategoryTheory.Arrow C}
{g : CategoryTheory.Arrow C}
[CategoryTheory.Limits.HasImage f.hom]
[CategoryTheory.Limits.HasImage g.hom]
(sq : f ⟶ g)
[CategoryTheory.Limits.HasImageMap sq]
:
Obtain an ImageMap from a HasImageMap instance.
Equations
instance
CategoryTheory.Limits.hasImageMapOfIsIso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f : CategoryTheory.Arrow C}
{g : CategoryTheory.Arrow C}
[CategoryTheory.Limits.HasImage f.hom]
[CategoryTheory.Limits.HasImage g.hom]
(sq : f ⟶ g)
[CategoryTheory.IsIso sq]
:
Equations
- ⋯ = ⋯
instance
CategoryTheory.Limits.HasImageMap.comp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f : CategoryTheory.Arrow C}
{g : CategoryTheory.Arrow C}
{h : CategoryTheory.Arrow C}
[CategoryTheory.Limits.HasImage f.hom]
[CategoryTheory.Limits.HasImage g.hom]
[CategoryTheory.Limits.HasImage h.hom]
(sq1 : f ⟶ g)
(sq2 : g ⟶ h)
[CategoryTheory.Limits.HasImageMap sq1]
[CategoryTheory.Limits.HasImageMap sq2]
:
Equations
- ⋯ = ⋯
theorem
CategoryTheory.Limits.ImageMap.ext
{C : Type u}
:
∀ {inst : CategoryTheory.Category.{v, u} C} {f g : CategoryTheory.Arrow C}
{inst_1 : CategoryTheory.Limits.HasImage f.hom} {inst_2 : CategoryTheory.Limits.HasImage g.hom} {sq : f ⟶ g}
(x y : CategoryTheory.Limits.ImageMap sq), x.map = y.map → x = y
theorem
CategoryTheory.Limits.ImageMap.ext_iff
{C : Type u}
:
∀ {inst : CategoryTheory.Category.{v, u} C} {f g : CategoryTheory.Arrow C}
{inst_1 : CategoryTheory.Limits.HasImage f.hom} {inst_2 : CategoryTheory.Limits.HasImage g.hom} {sq : f ⟶ g}
(x y : CategoryTheory.Limits.ImageMap sq), x = y ↔ x.map = y.map
theorem
CategoryTheory.Limits.ImageMap.map_uniq_aux
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f : CategoryTheory.Arrow C}
{g : CategoryTheory.Arrow C}
[CategoryTheory.Limits.HasImage f.hom]
[CategoryTheory.Limits.HasImage g.hom]
{sq : f ⟶ g}
(map : CategoryTheory.Limits.image f.hom ⟶ CategoryTheory.Limits.image g.hom)
(map_ι : autoParam
(CategoryTheory.CategoryStruct.comp map (CategoryTheory.Limits.image.ι g.hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι f.hom) sq.right)
_auto✝)
(map' : CategoryTheory.Limits.image f.hom ⟶ CategoryTheory.Limits.image g.hom)
(map_ι' : CategoryTheory.CategoryStruct.comp map' (CategoryTheory.Limits.image.ι g.hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι f.hom) sq.right)
:
map = map'
theorem
CategoryTheory.Limits.ImageMap.map_uniq
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f : CategoryTheory.Arrow C}
{g : CategoryTheory.Arrow C}
[CategoryTheory.Limits.HasImage f.hom]
[CategoryTheory.Limits.HasImage g.hom]
{sq : f ⟶ g}
(F : CategoryTheory.Limits.ImageMap sq)
(G : CategoryTheory.Limits.ImageMap sq)
:
F.map = G.map
@[simp]
theorem
CategoryTheory.Limits.ImageMap.mk.injEq'
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f : CategoryTheory.Arrow C}
{g : CategoryTheory.Arrow C}
[CategoryTheory.Limits.HasImage f.hom]
[CategoryTheory.Limits.HasImage g.hom]
{sq : f ⟶ g}
(map : CategoryTheory.Limits.image f.hom ⟶ CategoryTheory.Limits.image g.hom)
(map_ι : autoParam
(CategoryTheory.CategoryStruct.comp map (CategoryTheory.Limits.image.ι g.hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι f.hom) sq.right)
_auto✝)
(map' : CategoryTheory.Limits.image f.hom ⟶ CategoryTheory.Limits.image g.hom)
(map_ι' : CategoryTheory.CategoryStruct.comp map' (CategoryTheory.Limits.image.ι g.hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι f.hom) sq.right)
:
instance
CategoryTheory.Limits.instSubsingletonImageMap
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f : CategoryTheory.Arrow C}
{g : CategoryTheory.Arrow C}
[CategoryTheory.Limits.HasImage f.hom]
[CategoryTheory.Limits.HasImage g.hom]
(sq : f ⟶ g)
:
Equations
- ⋯ = ⋯
@[inline, reducible]
abbrev
CategoryTheory.Limits.image.map
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f : CategoryTheory.Arrow C}
{g : CategoryTheory.Arrow C}
[CategoryTheory.Limits.HasImage f.hom]
[CategoryTheory.Limits.HasImage g.hom]
(sq : f ⟶ g)
[CategoryTheory.Limits.HasImageMap sq]
:
CategoryTheory.Limits.image f.hom ⟶ CategoryTheory.Limits.image g.hom
The map on images induced by a commutative square.
Equations
theorem
CategoryTheory.Limits.image.factor_map
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f : CategoryTheory.Arrow C}
{g : CategoryTheory.Arrow C}
[CategoryTheory.Limits.HasImage f.hom]
[CategoryTheory.Limits.HasImage g.hom]
(sq : f ⟶ g)
[CategoryTheory.Limits.HasImageMap sq]
:
theorem
CategoryTheory.Limits.image.map_ι
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f : CategoryTheory.Arrow C}
{g : CategoryTheory.Arrow C}
[CategoryTheory.Limits.HasImage f.hom]
[CategoryTheory.Limits.HasImage g.hom]
(sq : f ⟶ g)
[CategoryTheory.Limits.HasImageMap sq]
:
theorem
CategoryTheory.Limits.image.map_homMk'_ι
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{P : C}
{Q : C}
{k : X ⟶ Y}
[CategoryTheory.Limits.HasImage k]
{l : P ⟶ Q}
[CategoryTheory.Limits.HasImage l]
{m : X ⟶ P}
{n : Y ⟶ Q}
(w : CategoryTheory.CategoryStruct.comp m l = CategoryTheory.CategoryStruct.comp k n)
[CategoryTheory.Limits.HasImageMap (CategoryTheory.Arrow.homMk' w)]
:
def
CategoryTheory.Limits.imageMapComp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f : CategoryTheory.Arrow C}
{g : CategoryTheory.Arrow C}
[CategoryTheory.Limits.HasImage f.hom]
[CategoryTheory.Limits.HasImage g.hom]
(sq : f ⟶ g)
[CategoryTheory.Limits.HasImageMap sq]
{h : CategoryTheory.Arrow C}
[CategoryTheory.Limits.HasImage h.hom]
(sq' : g ⟶ h)
[CategoryTheory.Limits.HasImageMap sq']
:
Image maps for composable commutative squares induce an image map in the composite square.
Equations
- CategoryTheory.Limits.imageMapComp sq sq' = { map := CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.map sq) (CategoryTheory.Limits.image.map sq'), map_ι := ⋯ }
@[simp]
theorem
CategoryTheory.Limits.image.map_comp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{f : CategoryTheory.Arrow C}
{g : CategoryTheory.Arrow C}
[CategoryTheory.Limits.HasImage f.hom]
[CategoryTheory.Limits.HasImage g.hom]
(sq : f ⟶ g)
[CategoryTheory.Limits.HasImageMap sq]
{h : CategoryTheory.Arrow C}
[CategoryTheory.Limits.HasImage h.hom]
(sq' : g ⟶ h)
[CategoryTheory.Limits.HasImageMap sq']
[CategoryTheory.Limits.HasImageMap (CategoryTheory.CategoryStruct.comp sq sq')]
:
def
CategoryTheory.Limits.imageMapId
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(f : CategoryTheory.Arrow C)
[CategoryTheory.Limits.HasImage f.hom]
:
The identity image f ⟶ image f fits into the commutative square represented by the identity
morphism 𝟙 f in the arrow category.
Equations
- CategoryTheory.Limits.imageMapId f = { map := CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.image f.hom), map_ι := ⋯ }
@[simp]
theorem
CategoryTheory.Limits.image.map_id
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(f : CategoryTheory.Arrow C)
[CategoryTheory.Limits.HasImage f.hom]
[CategoryTheory.Limits.HasImageMap (CategoryTheory.CategoryStruct.id f)]
:
class
CategoryTheory.Limits.HasImageMaps
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasImages C]
:
If a category has_image_maps, then all commutative squares induce morphisms on images.
- has_image_map : ∀ {f g : CategoryTheory.Arrow C} (st : f ⟶ g), CategoryTheory.Limits.HasImageMap st
@[simp]
theorem
CategoryTheory.Limits.im_obj
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasImages C]
[CategoryTheory.Limits.HasImageMaps C]
(f : CategoryTheory.Arrow C)
:
CategoryTheory.Limits.im.obj f = CategoryTheory.Limits.image f.hom
@[simp]
theorem
CategoryTheory.Limits.im_map
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasImages C]
[CategoryTheory.Limits.HasImageMaps C]
:
∀ {X Y : CategoryTheory.Arrow C} (st : X ⟶ Y), CategoryTheory.Limits.im.map st = CategoryTheory.Limits.image.map st
def
CategoryTheory.Limits.im
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasImages C]
[CategoryTheory.Limits.HasImageMaps C]
:
The functor from the arrow category of C to C itself that maps a morphism to its image
and a commutative square to the induced morphism on images.
Equations
- One or more equations did not get rendered due to their size.
structure
CategoryTheory.Limits.StrongEpiMonoFactorisation
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
extends
CategoryTheory.Limits.MonoFactorisation
:
Type (max u v)
A strong epi-mono factorisation is a decomposition f = e ≫ m with e a strong epimorphism
and m a monomorphism.
- I : C
- m : self.I ⟶ Y
- m_mono : CategoryTheory.Mono self.m
- e : X ⟶ self.I
- fac : CategoryTheory.CategoryStruct.comp self.e self.m = f
- e_strong_epi : CategoryTheory.StrongEpi self.e
instance
CategoryTheory.Limits.strongEpiMonoFactorisationInhabited
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.StrongEpi f]
:
Satisfying the inhabited linter
Equations
- One or more equations did not get rendered due to their size.
def
CategoryTheory.Limits.StrongEpiMonoFactorisation.toMonoIsImage
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
(F : CategoryTheory.Limits.StrongEpiMonoFactorisation f)
:
CategoryTheory.Limits.IsImage F.toMonoFactorisation
A mono factorisation coming from a strong epi-mono factorisation always has the universal property of the image.
Equations
- CategoryTheory.Limits.StrongEpiMonoFactorisation.toMonoIsImage F = { lift := fun (G : CategoryTheory.Limits.MonoFactorisation f) => CategoryTheory.CommSq.lift ⋯, lift_fac := ⋯ }
class
CategoryTheory.Limits.HasStrongEpiMonoFactorisations
(C : Type u)
[CategoryTheory.Category.{v, u} C]
:
A category has strong epi-mono factorisations if every morphism admits a strong epi-mono factorisation.
- mk' :: (
- has_fac : ∀ {X Y : C} (f : X ⟶ Y), Nonempty (CategoryTheory.Limits.StrongEpiMonoFactorisation f)
A category has strong epi-mono factorisations if every morphism admits a strong epi-mono factorisation.
- )
Instances
theorem
CategoryTheory.Limits.HasStrongEpiMonoFactorisations.mk
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(d : {X Y : C} → (f : X ⟶ Y) → CategoryTheory.Limits.StrongEpiMonoFactorisation f)
:
class
CategoryTheory.Limits.HasStrongEpiImages
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasImages C]
:
A category has strong epi images if it has all images and factorThruImage f is a strong
epimorphism for all f.
- strong_factorThruImage : ∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.StrongEpi (CategoryTheory.Limits.factorThruImage f)
theorem
CategoryTheory.Limits.strongEpi_of_strongEpiMonoFactorisation
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
(F : CategoryTheory.Limits.StrongEpiMonoFactorisation f)
{F' : CategoryTheory.Limits.MonoFactorisation f}
(hF' : CategoryTheory.Limits.IsImage F')
:
If there is a single strong epi-mono factorisation of f, then every image factorisation is a
strong epi-mono factorisation.
theorem
CategoryTheory.Limits.strongEpi_factorThruImage_of_strongEpiMonoFactorisation
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
[CategoryTheory.Limits.HasImage f]
(F : CategoryTheory.Limits.StrongEpiMonoFactorisation f)
:
instance
CategoryTheory.Limits.hasStrongEpiImages_of_hasStrongEpiMonoFactorisations
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasStrongEpiMonoFactorisations C]
:
If we constructed our images from strong epi-mono factorisations, then these images are strong epi images.
Equations
- ⋯ = ⋯
instance
CategoryTheory.Limits.hasImageMapsOfHasStrongEpiImages
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasImages C]
[CategoryTheory.Limits.HasStrongEpiImages C]
:
A category with strong epi images has image maps.
Equations
- ⋯ = ⋯
instance
CategoryTheory.Limits.hasStrongEpiImages_of_hasPullbacks_of_hasEqualizers
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasImages C]
[CategoryTheory.Limits.HasPullbacks C]
[CategoryTheory.Limits.HasEqualizers C]
:
If a category has images, equalizers and pullbacks, then images are automatically strong epi images.
Equations
- ⋯ = ⋯
def
CategoryTheory.Limits.image.isoStrongEpiMono
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasStrongEpiMonoFactorisations C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{I' : C}
(e : X ⟶ I')
(m : I' ⟶ Y)
(comm : CategoryTheory.CategoryStruct.comp e m = f)
[CategoryTheory.StrongEpi e]
[CategoryTheory.Mono m]
:
If C has strong epi mono factorisations, then the image is unique up to isomorphism, in that if
f factors as a strong epi followed by a mono, this factorisation is essentially the image
factorisation.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Limits.image.isoStrongEpiMono_hom_comp_ι
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasStrongEpiMonoFactorisations C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{I' : C}
(e : X ⟶ I')
(m : I' ⟶ Y)
(comm : CategoryTheory.CategoryStruct.comp e m = f)
[CategoryTheory.StrongEpi e]
[CategoryTheory.Mono m]
:
@[simp]
theorem
CategoryTheory.Limits.image.isoStrongEpiMono_inv_comp_mono
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasStrongEpiMonoFactorisations C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{I' : C}
(e : X ⟶ I')
(m : I' ⟶ Y)
(comm : CategoryTheory.CategoryStruct.comp e m = f)
[CategoryTheory.StrongEpi e]
[CategoryTheory.Mono m]
:
theorem
CategoryTheory.Functor.hasStrongEpiMonoFactorisations_imp_of_isEquivalence
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
(F : CategoryTheory.Functor C D)
[CategoryTheory.IsEquivalence F]
[h : CategoryTheory.Limits.HasStrongEpiMonoFactorisations C]
: