LeanPool.FactorizationSystems.Basic

def CategoryTheory.containsIsos {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) : Prop

The predicate that a class of morphism contains the isomorphisms

Equations

• CategoryTheory.containsIsos W = ∀ ⦃X Y : C⦄ (f : X ≅ Y), W f.hom

class CategoryTheory.is_closed_comp {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) extends W.Respects W : Prop

The predicate of a class of morphisms being closed under compositin

• precomp {X Y Z : C} (i : X ⟶ Y) (hi : W i) (f : Y ⟶ Z) (hf : W f) : W (CategoryStruct.comp i f)
• postcomp {X Y Z : C} (i : Y ⟶ Z) (hi : W i) (f : X ⟶ Y) (hf : W f) : W (CategoryStruct.comp f i)

structure CategoryTheory.FactorizationSystem {C : Type u} [Category.{v, u} C] (L R : MorphismProperty C) : Type (max u v)

The structure of a factorization system on a category C with specified classes of morphisms

• contains_isos_left_class : containsIsos L

  The left class contains isomorphism

• contains_isos_right_class : containsIsos R

  The right class contains isomorphism

• is_closed_comp_left_class : is_closed_comp L

  The left class is closed under composition

• is_closed_comp_right_class : is_closed_comp R

  The right class is closed under composition

• image {X Y : C} (f : X ⟶ Y) : C

  The midpoint/image of the factorization

• leftMap {X Y : C} (f : X ⟶ Y) : X ⟶ self.image f

  The left map of the factorization

• left_map_in_left_class {X Y : C} (f : X ⟶ Y) : L (self.leftMap f)

  The left map of the factorization is contained in the left class

• rightMap {X Y : C} (f : X ⟶ Y) : self.image f ⟶ Y

  The right map of the factorization

• right_map_in_right_class {X Y : C} (f : X ⟶ Y) : R (self.rightMap f)

  The left map of the factorization is contained in the left class

• factorization {X Y : C} (f : X ⟶ Y) : CategoryStruct.comp (self.leftMap f) (self.rightMap f) = f

  The factorization

• factorizationIso {X Y : C} (f : X ⟶ Y) (im : C) (left : X ⟶ im) : L left → (right : im ⟶ Y) → R right → (fact : CategoryStruct.comp left right = f) → (i : self.image f ≅ im) ×' CategoryStruct.comp (self.leftMap f) i.hom = left ∧ CategoryStruct.comp i.hom right = self.rightMap f

  The factorization is unique up to isomorphism

• factorization_iso_is_unique {X Y : C} (f : X ⟶ Y) (im : C) (left : X ⟶ im) (p : L left) (right : im ⟶ Y) (q : R right) (fact : CategoryStruct.comp left right = f) (i : self.image f ≅ im) (comm₁ : CategoryStruct.comp (self.leftMap f) i.hom = left) (comm₂ : CategoryStruct.comp i.hom right = self.rightMap f) : i = (self.factorizationIso f im left p right q fact).fst

  The factorization is unique up toa unique isomorphism

theorem CategoryTheory.factorization_iso_is_unique' {C : Type u} [Category.{v, u} C] {L R : MorphismProperty C} (F : FactorizationSystem L R) {X Y : C} (f : X ⟶ Y) (E E' : C) (s : X ⟶ E) (hs : L s) (p : E ⟶ Y) (hp : R p) (fact : CategoryStruct.comp s p = f) (s' : X ⟶ E') (hs' : L s') (p' : E' ⟶ Y) (hp' : R p') (fact' : CategoryStruct.comp s' p' = f) (i i' : E ≅ E') (comm₁ : CategoryStruct.comp s i.hom = s') (comm₂ : CategoryStruct.comp i.hom p' = p) (comm₁' : CategoryStruct.comp s i'.hom = s') (comm₂' : CategoryStruct.comp i'.hom p' = p) : i = i'

A useful characterization of the uniqueness of the factorization iso

def CategoryTheory.MorphismPropertySlice {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) (X : C) : MorphismProperty (Over X)

A class of morphisms in C defines a class of morphism in the slice C/X for every X ∈ C

Equations

• CategoryTheory.MorphismPropertySlice W X f = W ((CategoryTheory.Over.forget X).map f)

theorem CategoryTheory.contains_isos_slice {C : Type u} [Category.{v, u} C] {W : MorphismProperty C} {X : C} : containsIsos W → containsIsos (MorphismPropertySlice W X)

If a class of morphisms contains isomorphisms, then so does the class of morphisms in the slice

theorem CategoryTheory.is_closed_comp_slice {C : Type u} [Category.{v, u} C] {W : MorphismProperty C} {X : C} (h : is_closed_comp W) : is_closed_comp (MorphismPropertySlice W X)

If a class of morphisms is closed under composition, then so does the class of morphisms in the slice

theorem CategoryTheory.Over.forget_map_comp {C : Type u} [Category.{v, u} C] {X : C} {p q r : Over X} (F : p ⟶ q) (G : q ⟶ r) (H : p ⟶ r) (hyp : CategoryStruct.comp F G = H) : CategoryStruct.comp (Hom.left F) (Hom.left G) = Hom.left H

If a triangle commutes in the slice C/X, then it commutes in C

def CategoryTheory.Over.forgetPreservesIsos {C : Type u} [Category.{v, u} C] {X : C} {f g : Over X} (i : f ≅ g) : f.left ≅ g.left

The forgetful functor C/X ⟶ X preserves isomorphisms

Equations

• CategoryTheory.Over.forgetPreservesIsos i = { hom := CategoryTheory.Over.Hom.left i.hom, inv := CategoryTheory.Over.Hom.left i.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ }

def CategoryTheory.imageSlice {C : Type u} [Category.{v, u} C] {X : C} {L R : MorphismProperty C} (F : FactorizationSystem L R) {f g : Over X} (φ : f ⟶ g) : Over X

Imported FactorizationSystems declaration.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.leftMapSlice {C : Type u} [Category.{v, u} C] {X : C} {L R : MorphismProperty C} (F : FactorizationSystem L R) {f g : Over X} (φ : f ⟶ g) : f ⟶ imageSlice F φ

Imported FactorizationSystems declaration.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.left_map_in_left_class_slice {C : Type u} [Category.{v, u} C] {X : C} {L R : MorphismProperty C} (F : FactorizationSystem L R) {f g : Over X} (φ : f ⟶ g) : MorphismPropertySlice L X (leftMapSlice F φ)

def CategoryTheory.rightMapSlice {C : Type u} [Category.{v, u} C] {X : C} {L R : MorphismProperty C} (F : FactorizationSystem L R) {f g : Over X} (φ : f ⟶ g) : imageSlice F φ ⟶ g

Imported FactorizationSystems declaration.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.right_map_in_right_class_slice {C : Type u} [Category.{v, u} C] {X : C} {L R : MorphismProperty C} (F : FactorizationSystem L R) {f g : Over X} (φ : f ⟶ g) : MorphismPropertySlice R X (rightMapSlice F φ)

theorem CategoryTheory.factorization_slice {C : Type u} [Category.{v, u} C] {X : C} {L R : MorphismProperty C} (F : FactorizationSystem L R) {f g : Over X} (φ : f ⟶ g) : CategoryStruct.comp (leftMapSlice F φ) (rightMapSlice F φ) = φ

def CategoryTheory.factorizationIsoSlice {C : Type u} [Category.{v, u} C] {X : C} {L R : MorphismProperty C} (F : FactorizationSystem L R) {f g : Over X} (φ : f ⟶ g) (im : Over X) (left : f ⟶ im) (p : MorphismPropertySlice L X left) (right : im ⟶ g) (q : MorphismPropertySlice R X right) (fact : CategoryStruct.comp left right = φ) : (i : imageSlice F φ ≅ im) ×' CategoryStruct.comp (leftMapSlice F φ) i.hom = left ∧ CategoryStruct.comp i.hom right = rightMapSlice F φ

Imported FactorizationSystems declaration.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.factorization_iso_is_unique_slice {C : Type u} [Category.{v, u} C] {X : C} {L R : MorphismProperty C} (F : FactorizationSystem L R) {f g : Over X} (φ : f ⟶ g) (im : Over X) (left : f ⟶ im) (p : MorphismPropertySlice L X left) (right : im ⟶ g) (q : MorphismPropertySlice R X right) (fact : CategoryStruct.comp left right = φ) (i : imageSlice F φ ≅ im) (comm₁ : CategoryStruct.comp (leftMapSlice F φ) i.hom = left) (comm₂ : CategoryStruct.comp i.hom right = rightMapSlice F φ) : i = (factorizationIsoSlice F φ im left p right q fact).fst

def CategoryTheory.FactorizationSystemSlice {C : Type u} [Category.{v, u} C] {X : C} {L R : MorphismProperty C} (F : FactorizationSystem L R) : FactorizationSystem (MorphismPropertySlice L X) (MorphismPropertySlice R X)

A factorization system in C descends to a factorization system in the slice

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.factFactIso {C : Type u} [Category.{v, u} C] {L R : MorphismProperty C} (F : FactorizationSystem L R) {X Y : C} (f : X ⟶ Y) (E : C) (l : X ⟶ E) (p : L l) (r : E ⟶ Y) (q : R r) (fact : CategoryStruct.comp l r = f) (E' : C) (l' : X ⟶ E') (p' : L l') (r' : E' ⟶ Y) (q' : R r') (fact' : CategoryStruct.comp l' r' = f) : E ≅ E'

Imported FactorizationSystems declaration.

Equations

• CategoryTheory.factFactIso F f E l p r q fact E' l' p' r' q' fact' = (F.factorizationIso f E l p r q fact).fst.symm ≪≫ (F.factorizationIso f E' l' p' r' q' fact').fst

theorem CategoryTheory.fact_fact_iso_comm_left {C : Type u} [Category.{v, u} C] {L R : MorphismProperty C} (F : FactorizationSystem L R) {X Y : C} (f : X ⟶ Y) (E : C) (l : X ⟶ E) (p : L l) (r : E ⟶ Y) (q : R r) (fact : CategoryStruct.comp l r = f) (E' : C) (l' : X ⟶ E') (p' : L l') (r' : E' ⟶ Y) (q' : R r') (fact' : CategoryStruct.comp l' r' = f) : CategoryStruct.comp l (factFactIso F f E l p r q fact E' l' p' r' q' fact').hom = l'

theorem CategoryTheory.fact_fact_iso_comm_right {C : Type u} [Category.{v, u} C] {L R : MorphismProperty C} (F : FactorizationSystem L R) {X Y : C} (f : X ⟶ Y) (E : C) (l : X ⟶ E) (p : L l) (r : E ⟶ Y) (q : R r) (fact : CategoryStruct.comp l r = f) (E' : C) (l' : X ⟶ E') (p' : L l') (r' : E' ⟶ Y) (q' : R r') (fact' : CategoryStruct.comp l' r' = f) : CategoryStruct.comp (factFactIso F f E l p r q fact E' l' p' r' q' fact').hom r' = r

@[implicit_reducible]

instance CategoryTheory.MorphismProperty.Inter {C : Type u} [Category.{v, u} C] : _root_.Inter (MorphismProperty C)

Imported FactorizationSystems declaration.

Equations

• CategoryTheory.MorphismProperty.Inter = { inter := fun (L R : CategoryTheory.MorphismProperty C) ⦃X Y : C⦄ (f : X ⟶ Y) => L f ∧ R f }

theorem CategoryTheory.left_right_intersection_iso {C : Type u} [Category.{v, u} C] {L R : MorphismProperty C} : ∀ (a : FactorizationSystem L R), L ∩ R = MorphismProperty.isomorphisms C

def CategoryTheory.MorphismProperty.leftCancellation {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) : Prop

Imported FactorizationSystems declaration.

Equations

• W.leftCancellation = ∀ ⦃X Y Z : C⦄ (u : X ⟶ Y) (v : Y ⟶ Z), W (CategoryTheory.CategoryStruct.comp u v) → W v → W u

def CategoryTheory.MorphismProperty.rightCancellation {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) : Prop

Imported FactorizationSystems declaration.

Equations

• W.rightCancellation = ∀ ⦃X Y Z : C⦄ (u : X ⟶ Y) (v : Y ⟶ Z), W (CategoryTheory.CategoryStruct.comp u v) → W u → W v

theorem CategoryTheory.right_cancellation_left_class {C : Type u} [Category.{v, u} C] {L R : MorphismProperty C} (F : FactorizationSystem L R) : L.rightCancellation

theorem CategoryTheory.left_cancellation_right_class {C : Type u} [Category.{v, u} C] {L R : MorphismProperty C} (F : FactorizationSystem L R) : R.leftCancellation