LeanPool.FactorizationSystems.Characterization

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

Imported FactorizationSystems declaration.

Equations

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

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

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

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

Imported FactorizationSystems declaration.

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

  The midpoint object of the weak factorization.

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

  The left morphism of the weak factorization.

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

  The left morphism lies in the left class.

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

  The right morphism of the weak factorization.

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

  The right morphism lies in the right class.

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

  The two maps compose to the original morphism.

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

Imported FactorizationSystems declaration.

Equations

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

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

Imported FactorizationSystems declaration.

Equations

• CategoryTheory.orthogonalClass L R = (⦃A B X Y : C⦄ → (l : A ⟶ B) → L l → (r : X ⟶ Y) → R r → CategoryTheory.orthogonal l r)

def CategoryTheory.FactorizationSystemDiagonal {C : Type u} [Category.{v, u} C] {L R : MorphismProperty C} (F : FactorizationSystem L R) {A B X Y : C} (l : A ⟶ B) (hl : L l) (r : X ⟶ Y) (hr : R r) (S : l □ r) : diagonalFiller S

Imported FactorizationSystems declaration.

Equations

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

theorem CategoryTheory.FactorizationSystem_diagonal_canonicity {C : Type u} [Category.{v, u} C] {L R : MorphismProperty C} (F : FactorizationSystem L R) {A B X Y : C} (l : A ⟶ B) (hl : L l) (r : X ⟶ Y) (hr : R r) (S : l □ r) (d : diagonalFiller S) : d.map = (FactorizationSystemDiagonal F l hl r hr S).map

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

Imported FactorizationSystems declaration.

Equations

• CategoryTheory.FactorizationSystemOrthogonal L R F l hl r hr = { diagonal := fun (S : l □ r) => CategoryTheory.FactorizationSystemDiagonal F l hl r hr S, diagonal_unique := ⋯ }

theorem CategoryTheory.left_determinacy {C : Type u} [Category.{v, u} C] (L R : MorphismProperty C) (H₁R : isReplete R) (H₂ : WeakFactorizationSystem L R) (H₃ : orthogonalClass L R) : R = rightOrthogonalComplement L

theorem CategoryTheory.right_determinacy {C : Type u} [Category.{v, u} C] (L R : MorphismProperty C) (H₁L : isReplete L) (H₂ : WeakFactorizationSystem L R) (H₃ : orthogonalClass L R) : L = leftOrthogonalComplement R

noncomputable def CategoryTheory.FactorizationSystemCharacterization {C : Type u} [Category.{v, u} C] (L R : MorphismProperty C) (H₁L : isReplete L) (H₁R : isReplete R) (H₂ : WeakFactorizationSystem L R) (H₃ : orthogonalClass L R) : FactorizationSystem L R

Imported FactorizationSystems declaration.

Equations

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