LeanPool.FactorizationSystems.Examples

theorem CategoryTheory.isIsoIsEpi {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) : MorphismProperty.isomorphisms C f → MorphismProperty.epimorphisms C f

theorem CategoryTheory.epimorphismsContainsIsos {C : Type u} [Category.{v, u} C] : containsIsos (MorphismProperty.epimorphisms C)

theorem CategoryTheory.epimorphismsClosedUnderComp {C : Type u} [Category.{v, u} C] : is_closed_comp (MorphismProperty.epimorphisms C)

theorem CategoryTheory.isIsoIsMono {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) : MorphismProperty.isomorphisms C f → MorphismProperty.monomorphisms C f

theorem CategoryTheory.monomorphismsContainsIsos {C : Type u} [Category.{v, u} C] : containsIsos (MorphismProperty.monomorphisms C)

theorem CategoryTheory.monomorphismsClosedUnderComp {C : Type u} [Category.{v, u} C] : is_closed_comp (MorphismProperty.monomorphisms C)

def CategoryTheory.imageSet {X Y : Type u} (f : X ⟶ Y) : Type u

Imported FactorizationSystems declaration.

Equations

• CategoryTheory.imageSet f = { y : Y // ∃ (x : X), (CategoryTheory.ConcreteCategory.hom f) x = y }

def CategoryTheory.leftMapSet {X Y : Type u} (f : X ⟶ Y) : X ⟶ imageSet f

Imported FactorizationSystems declaration.

Equations

• CategoryTheory.leftMapSet f = TypeCat.ofHom fun (x : X) => ⟨(CategoryTheory.ConcreteCategory.hom f) x, ⋯⟩

def CategoryTheory.rightMapSet {X Y : Type u} (f : X ⟶ Y) : imageSet f ⟶ Y

Imported FactorizationSystems declaration.

Equations

• CategoryTheory.rightMapSet f = TypeCat.ofHom fun (y : CategoryTheory.imageSet f) => ↑y

theorem CategoryTheory.factorization_set {X Y : Type u} (f : X ⟶ Y) : CategoryStruct.comp (leftMapSet f) (rightMapSet f) = f

theorem CategoryTheory.left_map_in_left_class_set {X Y : Type u} (f : X ⟶ Y) : MorphismProperty.epimorphisms (Type u) (leftMapSet f)

theorem CategoryTheory.right_map_in_right_class_set {X Y : Type u} (f : X ⟶ Y) : MorphismProperty.monomorphisms (Type u) (rightMapSet f)

theorem CategoryTheory.factorization_iso_set_hom' {X Y : Type u} (f : X ⟶ Y) (im : Type u) (left : X ⟶ im) : MorphismProperty.epimorphisms (Type u) left → ∀ (right : im ⟶ Y) (q : MorphismProperty.monomorphisms (Type u) right) (fact : CategoryStruct.comp left right = f) (y : imageSet f), ∃! y' : im, (ConcreteCategory.hom right) y' = (ConcreteCategory.hom (rightMapSet f)) y

noncomputable def CategoryTheory.factorizationIsoSetHom {X Y : Type u} (f : X ⟶ Y) (im : Type u) (left : X ⟶ im) : MorphismProperty.epimorphisms (Type u) left → (right : im ⟶ Y) → MorphismProperty.monomorphisms (Type u) right → (fact : CategoryStruct.comp left right = f) → imageSet f ⟶ im

Imported FactorizationSystems declaration.

Equations

• CategoryTheory.factorizationIsoSetHom f im left p right q fact = TypeCat.ofHom fun (y : CategoryTheory.imageSet f) => Exists.choose ⋯

theorem CategoryTheory.factorization_iso_set_hom_comm_right {X Y : Type u} (f : X ⟶ Y) (im : Type u) (left : X ⟶ im) (p : MorphismProperty.epimorphisms (Type u) left) (right : im ⟶ Y) (q : MorphismProperty.monomorphisms (Type u) right) (fact : CategoryStruct.comp left right = f) : CategoryStruct.comp (factorizationIsoSetHom f im left p right q fact) right = rightMapSet f

theorem CategoryTheory.factorization_iso_set_hom_comm_left {X Y : Type u} (f : X ⟶ Y) (im : Type u) (left : X ⟶ im) (p : MorphismProperty.epimorphisms (Type u) left) (right : im ⟶ Y) (q : MorphismProperty.monomorphisms (Type u) right) (fact : CategoryStruct.comp left right = f) : CategoryStruct.comp (leftMapSet f) (factorizationIsoSetHom f im left p right q fact) = left

def CategoryTheory.factorizationIsoSetInv {X Y : Type u} (f : X ⟶ Y) (im : Type u) (left : X ⟶ im) : MorphismProperty.epimorphisms (Type u) left → (right : im ⟶ Y) → (fact : CategoryStruct.comp left right = f) → im ⟶ imageSet f

Imported FactorizationSystems declaration.

Equations

• CategoryTheory.factorizationIsoSetInv f im left p right fact = TypeCat.ofHom fun (y : im) => have existence := ⋯; ⟨(CategoryTheory.ConcreteCategory.hom right) y, existence⟩

theorem CategoryTheory.factorization_iso_set_inv_comm_right {X Y : Type u} (f : X ⟶ Y) (im : Type u) (left : X ⟶ im) (p : MorphismProperty.epimorphisms (Type u) left) (right : im ⟶ Y) (fact : CategoryStruct.comp left right = f) : CategoryStruct.comp (factorizationIsoSetInv f im left p right fact) (rightMapSet f) = right

theorem CategoryTheory.factorization_iso_set_inv_comm_left {X Y : Type u} (f : X ⟶ Y) (im : Type u) (left : X ⟶ im) (p : MorphismProperty.epimorphisms (Type u) left) (right : im ⟶ Y) (fact : CategoryStruct.comp left right = f) : CategoryStruct.comp left (factorizationIsoSetInv f im left p right fact) = leftMapSet f

noncomputable def CategoryTheory.factorizationIsoSet {X Y : Type u} (f : X ⟶ Y) (im : Type u) (left : X ⟶ im) : MorphismProperty.epimorphisms (Type u) left → (right : im ⟶ Y) → MorphismProperty.monomorphisms (Type u) right → CategoryStruct.comp left right = f → (i : imageSet f ≅ im) ×' CategoryStruct.comp (leftMapSet f) i.hom = left ∧ CategoryStruct.comp i.hom right = rightMapSet f

Imported FactorizationSystems declaration.

Equations

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

theorem CategoryTheory.factorization_iso_is_unique_set {X Y : Type u} (f : X ⟶ Y) (im : Type u) (left : X ⟶ im) (p : MorphismProperty.epimorphisms (Type u) left) (right : im ⟶ Y) (q : MorphismProperty.monomorphisms (Type u) right) (fact : CategoryStruct.comp left right = f) (i : imageSet f ≅ im) : CategoryStruct.comp (leftMapSet f) i.hom = left → CategoryStruct.comp i.hom right = rightMapSet f → i = (factorizationIsoSet f im left p right q fact).fst

noncomputable def CategoryTheory.EpiMonoSet : FactorizationSystem (MorphismProperty.epimorphisms (Type u)) (MorphismProperty.monomorphisms (Type u))

Imported FactorizationSystems declaration.

Equations

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