LeanPool.FactorizationSystems.OrthogonalComplements

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

Imported FactorizationSystems declaration.

Equations

• CategoryTheory.rightOrthogonalComplement W f = ∀ ⦃A B : C⦄ (g : A ⟶ B), W g → CategoryTheory.homOrthogonal g f

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

Imported FactorizationSystems declaration.

Equations

• CategoryTheory.leftOrthogonalComplement W f = ∀ ⦃A B : C⦄ (g : A ⟶ B), W g → CategoryTheory.homOrthogonal f g

@[reducible]

def CategoryTheory.Arrow.sourceConeArrowCone {C : Type u} [Category.{v, u} C] {J : Type u} [Category.{v, u} J] (f : Functor J (Arrow C)) (Cf : Limits.Cone f) : Limits.Cone (f.comp leftFunc)

Imported FactorizationSystems declaration.

Equations

• CategoryTheory.Arrow.sourceConeArrowCone f Cf = { pt := CategoryTheory.Arrow.leftFunc.obj Cf.pt, π := { app := fun (i : J) => CategoryTheory.Arrow.leftFunc.map (Cf.π.app i), naturality := ⋯ } }

@[reducible]

def CategoryTheory.Arrow.coneSourceTrivConeArrow {C : Type u} [Category.{v, u} C] {J : Type u} [Category.{v, u} J] (f : Functor J (Arrow C)) (s : Limits.Cone (f.comp leftFunc)) : Limits.Cone f

Imported FactorizationSystems declaration.

Equations

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

@[reducible]

def CategoryTheory.Arrow.mapTrivMapArrowSource {C : Type u} [Category.{v, u} C] (f : Arrow C) (X : C) (m : X ⟶ f.left) : mk (CategoryStruct.id X) ⟶ f

Imported FactorizationSystems declaration.

Equations

• f.mapTrivMapArrowSource X m = CategoryTheory.Arrow.homMk m (CategoryTheory.CategoryStruct.comp m f.hom) ⋯

def CategoryTheory.Arrow.sourceLimitConeArrowLimitCone {C : Type u} [Category.{v, u} C] {J : Type u} [Category.{v, u} J] (f : Functor J (Arrow C)) (Cf : Limits.LimitCone f) : Limits.LimitCone (f.comp leftFunc)

Imported FactorizationSystems declaration.

Equations

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

@[reducible]

def CategoryTheory.Arrow.targetConeArrowCone {C : Type u} [Category.{v, u} C] {J : Type u} [Category.{v, u} J] (f : Functor J (Arrow C)) (Cf : Limits.Cone f) : Limits.Cone (f.comp rightFunc)

Imported FactorizationSystems declaration.

Equations

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

@[reducible]

noncomputable def CategoryTheory.Arrow.coneTargetTrivConeArrow {C : Type u} [Category.{v, u} C] {J : Type u} [Category.{v, u} J] [Limits.HasInitial C] (f : Functor J (Arrow C)) (s : Limits.Cone (f.comp rightFunc)) : Limits.Cone f

Imported FactorizationSystems declaration.

Equations

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

@[reducible]

noncomputable def CategoryTheory.Arrow.mapTrivMapArrowTarget {C : Type u} [Category.{v, u} C] [Limits.HasInitial C] (f : Arrow C) (B : C) (m : B ⟶ f.right) : mk (Limits.initial.to B) ⟶ f

Imported FactorizationSystems declaration.

Equations

• f.mapTrivMapArrowTarget B m = CategoryTheory.Arrow.homMk (CategoryTheory.Limits.initial.to f.left) m ⋯

noncomputable def CategoryTheory.Arrow.targetLimitConeArrowLimitCone {C : Type u} [Category.{v, u} C] {J : Type u} [Category.{v, u} J] [Limits.HasInitial C] (f : Functor J (Arrow C)) (Cf : Limits.LimitCone f) : Limits.LimitCone (f.comp rightFunc)

Imported FactorizationSystems declaration.

Equations

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

@[reducible]

def CategoryTheory.Arrow.squareCompletionIsClosedUnderLimitsROrtComplement {C : Type u} [Category.{v, u} C] {A B : C} {J : Type u} [Category.{v, u} J] (f : Functor J (Arrow C)) (s : Limits.LimitCone f) (m : A ⟶ B) (sq_lim : m □ s.cone.pt.hom) (i : J) : m □ (f.obj i).hom

Imported FactorizationSystems declaration.

Equations

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

@[reducible]

noncomputable def CategoryTheory.Arrow.coneLimitIsClosedUnderLimitsROrtComplement {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) {A B : C} {J : Type u} [Category.{v, u} J] (f : Functor J (Arrow C)) (s : Limits.LimitCone f) (m : A ⟶ B) (Wm : W m) (sq_lim : m □ s.cone.pt.hom) (p : ∀ (i : J), rightOrthogonalComplement W (f.obj i).hom) : Limits.Cone (f.comp leftFunc)

Imported FactorizationSystems declaration.

Equations

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

@[reducible]

noncomputable def CategoryTheory.Arrow.diagonalMapLimitIsClosedUnderLimitsROrtComplement {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) {A B : C} {J : Type u} [Category.{v, u} J] (f : Functor J (Arrow C)) (s : Limits.LimitCone f) (m : A ⟶ B) (Wm : W m) (sq_lim : m □ s.cone.pt.hom) (p : ∀ (i : J), rightOrthogonalComplement W (f.obj i).hom) : B ⟶ s.cone.pt.left

Imported FactorizationSystems declaration.

Equations

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

theorem CategoryTheory.Arrow.diagonal_comm_top_limit_is_closed_under_limits_r_ort_complement {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) {A B : C} {J : Type u} [Category.{v, u} J] (f : Functor J (Arrow C)) (s : Limits.LimitCone f) (m : A ⟶ B) (Wm : W m) (sq_lim : m □ s.cone.pt.hom) (p : ∀ (i : J), rightOrthogonalComplement W (f.obj i).hom) : CategoryStruct.comp m (diagonalMapLimitIsClosedUnderLimitsROrtComplement W f s m Wm sq_lim p) = sq_lim.top

theorem CategoryTheory.Arrow.diagonal_comm_bot_limit_is_closed_under_limits_r_ort_complement {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) {A B : C} {J : Type u} [Category.{v, u} J] [Limits.HasInitial C] (f : Functor J (Arrow C)) (s : Limits.LimitCone f) (m : A ⟶ B) (Wm : W m) (sq_lim : m □ s.cone.pt.hom) (p : ∀ (i : J), rightOrthogonalComplement W (f.obj i).hom) : CategoryStruct.comp (diagonalMapLimitIsClosedUnderLimitsROrtComplement W f s m Wm sq_lim p) s.cone.pt.hom = sq_lim.bot

noncomputable def CategoryTheory.Arrow.diagonalFillerLimitIsClosedUnderLimitsROrtComplement {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) {A B : C} {J : Type u} [Category.{v, u} J] [Limits.HasInitial C] (f : Functor J (Arrow C)) (s : Limits.LimitCone f) (m : A ⟶ B) (Wm : W m) (sq_lim : m □ s.cone.pt.hom) (p : ∀ (i : J), rightOrthogonalComplement W (f.obj i).hom) : diagonalFiller sq_lim

Imported FactorizationSystems declaration.

Equations

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

@[reducible]

def CategoryTheory.Arrow.diagonalPostcompIsDiagonal {C : Type u} [Category.{v, u} C] {J : Type u} [Category.{v, u} J] (f : Functor J (Arrow C)) (s : Limits.LimitCone f) {A B : C} (m : A ⟶ B) (S : m □ s.cone.pt.hom) (d : diagonalFiller S) (i : J) : diagonalFiller (squareCompletionIsClosedUnderLimitsROrtComplement f s m S i)

Imported FactorizationSystems declaration.

Equations

• CategoryTheory.Arrow.diagonalPostcompIsDiagonal f s m S d i = { map := CategoryTheory.CategoryStruct.comp d.map (CategoryTheory.Arrow.Hom.left (s.cone.π.app i)), comm_top := ⋯, comm_bot := ⋯ }

theorem CategoryTheory.Arrow.diagonal_unique_limit_is_closed_under_limits_r_ort_complement {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) {A B : C} {J : Type u} [Category.{v, u} J] [Limits.HasInitial C] (f : Functor J (Arrow C)) (s : Limits.LimitCone f) (m : A ⟶ B) (Wm : W m) (p : ∀ (i : J), rightOrthogonalComplement W (f.obj i).hom) (sq_lim : m □ s.cone.pt.hom) (d d' : diagonalFiller sq_lim) : d.map = d'.map

noncomputable def CategoryTheory.Arrow.isClosedUnderLimitsROrtComplement {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) {A B : C} {J : Type u} [Category.{v, u} J] [Limits.HasInitial C] (f : Functor J (Arrow C)) (s : Limits.LimitCone f) (m : A ⟶ B) (Wm : W m) (p : ∀ (i : J), rightOrthogonalComplement W (f.obj i).hom) : orthogonal m s.cone.pt.hom

Imported FactorizationSystems declaration.

Equations

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

theorem CategoryTheory.Arrow.is_closed_under_comp_r_ort_complement {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) {X Y Z : C} (r : X ⟶ Y) (hr : rightOrthogonalComplement W r) (r' : Y ⟶ Z) (hr' : rightOrthogonalComplement W r') : rightOrthogonalComplement W (CategoryStruct.comp r r')

theorem CategoryTheory.Arrow.is_closed_under_comp_l_ort_complement {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) {D E F : C} (l : D ⟶ E) (hl : leftOrthogonalComplement W l) (l' : E ⟶ F) (hl' : leftOrthogonalComplement W l') : leftOrthogonalComplement W (CategoryStruct.comp l l')

theorem CategoryTheory.Arrow.left_cancellation_r_ort_complement {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) {X Y Z : C} (r : X ⟶ Y) (r' : Y ⟶ Z) (hr' : rightOrthogonalComplement W r') (hr'r : rightOrthogonalComplement W (CategoryStruct.comp r r')) : rightOrthogonalComplement W r

theorem CategoryTheory.Arrow.base_change_r_ort_complement {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] (W : MorphismProperty C) {Y X' Y' : C} (r' : X' ⟶ Y') (hr' : rightOrthogonalComplement W r') (f : Y ⟶ Y') : rightOrthogonalComplement W (Limits.pullback.snd r' f)

theorem CategoryTheory.Arrow.contains_isos_left_ort_complement {C : Type u} [Category.{v, u} C] (R : MorphismProperty C) : containsIsos (leftOrthogonalComplement R)

theorem CategoryTheory.Arrow.contains_isos_right_ort_complement {C : Type u} [Category.{v, u} C] (L : MorphismProperty C) : containsIsos (rightOrthogonalComplement L)