LeanPool.FactorizationSystems.Orthogonality

structure CategoryTheory.square {C : Type u} [Category.{v, u} C] (A B X Y : C) : Type v

Imported FactorizationSystems declaration.

• left : A ⟶ B

  The left vertical morphism.

• right : X ⟶ Y

  The right vertical morphism.

• top : A ⟶ X

  The top horizontal morphism.

• bot : B ⟶ Y

  The bottom horizontal morphism.

• comm : CategoryStruct.comp self.left self.bot = CategoryStruct.comp self.top self.right

  The square commutes.

structure CategoryTheory.squareCompletion {C : Type u} [Category.{v, u} C] {A B X Y : C} (l : A ⟶ B) (r : X ⟶ Y) : Type v

Imported FactorizationSystems declaration.

• top : A ⟶ X

  The top horizontal morphism.

• bot : B ⟶ Y

  The bottom horizontal morphism.

• comm : CategoryStruct.comp l self.bot = CategoryStruct.comp self.top r

  The square commutes.

def CategoryTheory.«term_□_» : Lean.TrailingParserDescr

Imported FactorizationSystems declaration.

Equations

• CategoryTheory.«term_□_» = Lean.ParserDescr.trailingNode `CategoryTheory.«term_□_» 75 75 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " □ ") (Lean.ParserDescr.cat `term 76))

@[reducible]

def CategoryTheory.squareOfSquareCompletion {C : Type u} [Category.{v, u} C] {A B X Y : C} {l : A ⟶ B} {r : X ⟶ Y} (S' : l □ r) : square A B X Y

Imported FactorizationSystems declaration.

Equations

• CategoryTheory.squareOfSquareCompletion S' = { left := l, right := r, top := S'.top, bot := S'.bot, comm := ⋯ }

structure CategoryTheory.diagonalFiller {C : Type u} [Category.{v, u} C] {A B X Y : C} {f : A ⟶ B} {g : X ⟶ Y} (S : f □ g) : Type v

Imported FactorizationSystems declaration.

• map : B ⟶ X

  The diagonal morphism.

• comm_top : CategoryStruct.comp f self.map = S.top

  The top triangle commutes.

• comm_bot : CategoryStruct.comp self.map g = S.bot

  The bottom triangle commutes.

structure CategoryTheory.orthogonal {C : Type u} [Category.{v, u} C] {A B X Y : C} (f : A ⟶ B) (g : X ⟶ Y) : Type v

Imported FactorizationSystems declaration.

• diagonal (S : f □ g) : diagonalFiller S

  A chosen diagonal filler for every square.

• diagonal_unique (S : f □ g) (d d' : diagonalFiller S) : d.map = d'.map

  The chosen diagonal filler is unique.

@[reducible]

def CategoryTheory.homSquareLeft {C : Type u} [Category.{v, u} C] {A B X Y : C} (l : A ⟶ B) (r : X ⟶ Y) : (B ⟶ X) ⟶ A ⟶ X

Imported FactorizationSystems declaration.

Equations

• CategoryTheory.homSquareLeft l r = TypeCat.ofHom fun (f : B✝ ⟶ X✝) => CategoryTheory.CategoryStruct.comp l f

@[reducible]

def CategoryTheory.homSquareRight {C : Type u} [Category.{v, u} C] {A B X Y : C} (l : A ⟶ B) (r : X ⟶ Y) : (B ⟶ Y) ⟶ A ⟶ Y

Imported FactorizationSystems declaration.

Equations

• CategoryTheory.homSquareRight l r = TypeCat.ofHom fun (f : B✝ ⟶ Y✝) => CategoryTheory.CategoryStruct.comp l f

@[reducible]

def CategoryTheory.homSquareTop {C : Type u} [Category.{v, u} C] {A B X Y : C} (l : A ⟶ B) (r : X ⟶ Y) : (B ⟶ X) ⟶ B ⟶ Y

Imported FactorizationSystems declaration.

Equations

• CategoryTheory.homSquareTop l r = TypeCat.ofHom fun (f : B✝ ⟶ X✝) => CategoryTheory.CategoryStruct.comp f r

@[reducible]

def CategoryTheory.homSquareBot {C : Type u} [Category.{v, u} C] {A B X Y : C} (l : A ⟶ B) (r : X ⟶ Y) : (A ⟶ X) ⟶ A ⟶ Y

Imported FactorizationSystems declaration.

Equations

• CategoryTheory.homSquareBot l r = TypeCat.ofHom fun (f : A✝ ⟶ X✝) => CategoryTheory.CategoryStruct.comp f r

@[reducible]

def CategoryTheory.homSquare {C : Type u} [Category.{v, u} C] {A B X Y : C} (l : A ⟶ B) (r : X ⟶ Y) : square (B ⟶ X) (A ⟶ X) (B ⟶ Y) (A ⟶ Y)

Imported FactorizationSystems declaration.

Equations

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

def CategoryTheory.homCospanPullback {C : Type u} [Category.{v, u} C] {A B X Y : C} (l : A ⟶ B) (r : X ⟶ Y) : Type v

Imported FactorizationSystems declaration.

Equations

• CategoryTheory.homCospanPullback l r = CategoryTheory.Limits.pullback (CategoryTheory.homSquareRight l r) (CategoryTheory.homSquareBot l r)

noncomputable def CategoryTheory.homCospanPullbackCone {C : Type u} [Category.{v, u} C] {A B X Y : C} (l : A ⟶ B) (r : X ⟶ Y) : Limits.PullbackCone (homSquareRight l r) (homSquareBot l r)

Imported FactorizationSystems declaration.

Equations

• CategoryTheory.homCospanPullbackCone l r = CategoryTheory.Limits.pullback.cone (CategoryTheory.homSquareRight l r) (CategoryTheory.homSquareBot l r)

@[reducible]

noncomputable def CategoryTheory.homCospanPullbackFst {C : Type u} [Category.{v, u} C] {A B X Y : C} (l : A ⟶ B) (r : X ⟶ Y) : homCospanPullback l r ⟶ B ⟶ Y

Imported FactorizationSystems declaration.

Equations

• CategoryTheory.homCospanPullbackFst l r = CategoryTheory.Limits.pullback.fst (CategoryTheory.homSquareRight l r) (CategoryTheory.homSquareBot l r)

@[reducible]

noncomputable def CategoryTheory.homCospanPullbackSnd {C : Type u} [Category.{v, u} C] {A B X Y : C} (l : A ⟶ B) (r : X ⟶ Y) : homCospanPullback l r ⟶ A ⟶ X

Imported FactorizationSystems declaration.

Equations

• CategoryTheory.homCospanPullbackSnd l r = CategoryTheory.Limits.pullback.snd (CategoryTheory.homSquareRight l r) (CategoryTheory.homSquareBot l r)

@[reducible]

noncomputable def CategoryTheory.homCospanPullbackLift {C : Type u} [Category.{v, u} C] {W : Type v} {A B X Y : C} (l : A ⟶ B) (r : X ⟶ Y) (φ : W ⟶ B ⟶ Y) (ψ : W ⟶ A ⟶ X) (comm : CategoryStruct.comp φ (homSquareRight l r) = CategoryStruct.comp ψ (homSquareBot l r) := by aesop_cat) : W ⟶ homCospanPullback l r

Imported FactorizationSystems declaration.

Equations

• CategoryTheory.homCospanPullbackLift l r φ ψ comm = CategoryTheory.Limits.pullback.lift φ ψ comm

theorem CategoryTheory.hom_cospan_pullback_lift_fst {C : Type u} [Category.{v, u} C] {W : Type v} {A B X Y : C} (l : A ⟶ B) (r : X ⟶ Y) (φ : W ⟶ B ⟶ Y) (ψ : W ⟶ A ⟶ X) (comm : CategoryStruct.comp φ (homSquareRight l r) = CategoryStruct.comp ψ (homSquareBot l r) := by aesop_cat) : CategoryStruct.comp (homCospanPullbackLift l r φ ψ comm) (homCospanPullbackFst l r) = φ

theorem CategoryTheory.hom_cospan_pullback_lift_snd {C : Type u} [Category.{v, u} C] {W : Type v} {A B X Y : C} (l : A ⟶ B) (r : X ⟶ Y) (φ : W ⟶ B ⟶ Y) (ψ : W ⟶ A ⟶ X) (comm : CategoryStruct.comp φ (homSquareRight l r) = CategoryStruct.comp ψ (homSquareBot l r) := by aesop_cat) : CategoryStruct.comp (homCospanPullbackLift l r φ ψ comm) (homCospanPullbackSnd l r) = ψ

theorem CategoryTheory.hom_cospan_pullback_condition {C : Type u} [Category.{v, u} C] {A B X Y : C} (l : A ⟶ B) (r : X ⟶ Y) : CategoryStruct.comp (homCospanPullbackFst l r) (homSquareRight l r) = CategoryStruct.comp (homCospanPullbackSnd l r) (homSquareBot l r)

@[reducible]

def CategoryTheory.isCartesianSquare {C : Type u} [Category.{v, u} C] [HasPullbacks : Limits.HasPullbacks C] {A B X Y : C} (S : square A B X Y) : Prop

Imported FactorizationSystems declaration.

Equations

• CategoryTheory.isCartesianSquare S = CategoryTheory.IsIso (CategoryTheory.Limits.pullback.lift S.top S.left ⋯)

@[reducible]

def CategoryTheory.homOrthogonal {C : Type u} [Category.{v, u} C] {A B X Y : C} (l : A ⟶ B) (r : X ⟶ Y) : Prop

Imported FactorizationSystems declaration.

Equations

• CategoryTheory.homOrthogonal l r = CategoryTheory.isCartesianSquare (CategoryTheory.homSquare l r)

noncomputable def CategoryTheory.diagonalsHomCospanPullbackTop {C : Type u} [Category.{v, u} C] {A B X Y : C} (l : A ⟶ B) (r : X ⟶ Y) : (B ⟶ X) ⟶ A ⟶ X

Imported FactorizationSystems declaration.

Equations

• CategoryTheory.diagonalsHomCospanPullbackTop l r = TypeCat.ofHom fun (f : B ⟶ X) => CategoryTheory.CategoryStruct.comp l f

noncomputable def CategoryTheory.diagonalsHomCospanPullbackBot {C : Type u} [Category.{v, u} C] {A B X Y : C} (l : A ⟶ B) (r : X ⟶ Y) : (B ⟶ X) ⟶ B ⟶ Y

Imported FactorizationSystems declaration.

Equations

• CategoryTheory.diagonalsHomCospanPullbackBot l r = TypeCat.ofHom fun (f : B ⟶ X) => CategoryTheory.CategoryStruct.comp f r

theorem CategoryTheory.diagonals_hom_cospan_pullback_lift_comm {C : Type u} [Category.{v, u} C] {A B X Y : C} (l : A ⟶ B) (r : X ⟶ Y) : CategoryStruct.comp (diagonalsHomCospanPullbackBot l r) (homSquareRight l r) = CategoryStruct.comp (diagonalsHomCospanPullbackTop l r) (homSquareBot l r)

noncomputable def CategoryTheory.diagonalsHomCospanPullbackLift {C : Type u} [Category.{v, u} C] {A B X Y : C} (l : A ⟶ B) (r : X ⟶ Y) : (B ⟶ X) ⟶ homCospanPullback l r

Imported FactorizationSystems declaration.

Equations

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

theorem CategoryTheory.diagonals_hom_cospan_pullback_lift_fst {C : Type u} [Category.{v, u} C] {A B X Y : C} (l : A ⟶ B) (r : X ⟶ Y) : CategoryStruct.comp (diagonalsHomCospanPullbackLift l r) (homCospanPullbackFst l r) = diagonalsHomCospanPullbackBot l r

theorem CategoryTheory.diagonals_hom_cospan_pullback_lift_snd {C : Type u} [Category.{v, u} C] {A B X Y : C} (l : A ⟶ B) (r : X ⟶ Y) : CategoryStruct.comp (diagonalsHomCospanPullbackLift l r) (homCospanPullbackSnd l r) = diagonalsHomCospanPullbackTop l r

noncomputable def CategoryTheory.homCospanPullbackToSquareCompletion {C : Type u} [Category.{v, u} C] {A B X Y : C} (l : A ⟶ B) (r : X ⟶ Y) (x : homCospanPullback l r) : l □ r

Imported FactorizationSystems declaration.

Equations

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

noncomputable def CategoryTheory.homCospanPullbackToDiagonalFiller {C : Type u} [Category.{v, u} C] {A B X Y : C} (l : A ⟶ B) (r : X ⟶ Y) (h : orthogonal l r) (x : Limits.pullback (homSquareRight l r) (homSquareBot l r)) : diagonalFiller (homCospanPullbackToSquareCompletion l r x)

Imported FactorizationSystems declaration.

Equations

• CategoryTheory.homCospanPullbackToDiagonalFiller l r { diagonal := d, diagonal_unique := S } x = d (CategoryTheory.homCospanPullbackToSquareCompletion l r x)

noncomputable def CategoryTheory.homCospanPullbackToDiagonalFillerMap {C : Type u} [Category.{v, u} C] {A B X Y : C} (l : A ⟶ B) (r : X ⟶ Y) (h : orthogonal l r) : Limits.pullback (homSquareRight l r) (homSquareBot l r) ⟶ B ⟶ X

Imported FactorizationSystems declaration.

Equations

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

theorem CategoryTheory.hom_cospan_pullback_to_diagonal_filler_map_comm_top {C : Type u} [Category.{v, u} C] {A B X Y : C} (l : A ⟶ B) (r : X ⟶ Y) (h : orthogonal l r) (x : Limits.pullback (homSquareRight l r) (homSquareBot l r)) : CategoryStruct.comp l ((ConcreteCategory.hom (homCospanPullbackToDiagonalFillerMap l r h)) x) = (homCospanPullbackToSquareCompletion l r x).top

theorem CategoryTheory.hom_cospan_pullback_to_diagonal_filler_map_comm_bot {C : Type u} [Category.{v, u} C] {A B X Y : C} (l : A ⟶ B) (r : X ⟶ Y) (h : orthogonal l r) (x : Limits.pullback (homSquareRight l r) (homSquareBot l r)) : CategoryStruct.comp ((ConcreteCategory.hom (homCospanPullbackToDiagonalFillerMap l r h)) x) r = (homCospanPullbackToSquareCompletion l r x).bot

theorem CategoryTheory.orthogonal_implies_hom_orthogonal {C : Type u} [Category.{v, u} C] {A B X Y : C} (l : A ⟶ B) (r : X ⟶ Y) : ∀ (a : orthogonal l r), homOrthogonal l r

noncomputable def CategoryTheory.homPullbackCone {C : Type u} [Category.{v, u} C] {A B X Y : C} (l : A ⟶ B) (r : X ⟶ Y) : Limits.PullbackCone (homSquare l r).right (homSquare l r).bot

Imported FactorizationSystems declaration.

Equations

• CategoryTheory.homPullbackCone l r = CategoryTheory.Limits.pullback.cone (CategoryTheory.homSquare l r).right (CategoryTheory.homSquare l r).bot

noncomputable def CategoryTheory.homPullbackConeIsLimit {C : Type u} [Category.{v, u} C] {A B X Y : C} (l : A ⟶ B) (r : X ⟶ Y) : Limits.IsLimit (homPullbackCone l r)

Imported FactorizationSystems declaration.

Equations

• CategoryTheory.homPullbackConeIsLimit l r = CategoryTheory.Limits.pullback.isLimit (CategoryTheory.homSquare l r).right (CategoryTheory.homSquare l r).bot

def CategoryTheory.homPullbackConePoint {C : Type u} [Category.{v, u} C] {A B X Y : C} (l : A ⟶ B) (r : X ⟶ Y) : Type v

Imported FactorizationSystems declaration.

Equations

• CategoryTheory.homPullbackConePoint l r = (CategoryTheory.homPullbackCone l r).pt

noncomputable def CategoryTheory.homPullbackFst {C : Type u} [Category.{v, u} C] {A B X Y : C} (l : A ⟶ B) (r : X ⟶ Y) : homPullbackConePoint l r ⟶ B ⟶ Y

Imported FactorizationSystems declaration.

Equations

• CategoryTheory.homPullbackFst l r = CategoryTheory.Limits.pullback.fst (CategoryTheory.homSquare l r).right (CategoryTheory.homSquare l r).bot

noncomputable def CategoryTheory.homPullbackSnd {C : Type u} [Category.{v, u} C] {A B X Y : C} (l : A ⟶ B) (r : X ⟶ Y) : homPullbackConePoint l r ⟶ A ⟶ X

Imported FactorizationSystems declaration.

Equations

• CategoryTheory.homPullbackSnd l r = CategoryTheory.Limits.pullback.snd (CategoryTheory.homSquare l r).right (CategoryTheory.homSquare l r).bot

theorem CategoryTheory.diagonals_comm {C : Type u} [Category.{v, u} C] {A B X Y : C} (l : A ⟶ B) (r : X ⟶ Y) : CategoryStruct.comp (homSquare l r).top (homSquare l r).right = CategoryStruct.comp (homSquare l r).left (homSquare l r).bot

def CategoryTheory.diagonalsCone {C : Type u} [Category.{v, u} C] {A B X Y : C} (l : A ⟶ B) (r : X ⟶ Y) : Limits.PullbackCone (homSquare l r).right (homSquare l r).bot

Imported FactorizationSystems declaration.

Equations

• CategoryTheory.diagonalsCone l r = CategoryTheory.Limits.PullbackCone.mk (CategoryTheory.homSquare l r).top (CategoryTheory.homSquare l r).left ⋯

def CategoryTheory.diagonalsConePoint {C : Type u} [Category.{v, u} C] {A B X Y : C} (l : A ⟶ B) (r : X ⟶ Y) : Type v

Imported FactorizationSystems declaration.

Equations

• CategoryTheory.diagonalsConePoint l r = (CategoryTheory.diagonalsCone l r).pt

def CategoryTheory.diagonalsConeFst {C : Type u} [Category.{v, u} C] {A B X Y : C} (l : A ⟶ B) (r : X ⟶ Y) : diagonalsConePoint l r ⟶ B ⟶ Y

Imported FactorizationSystems declaration.

Equations

• CategoryTheory.diagonalsConeFst l r = (CategoryTheory.diagonalsCone l r).fst

def CategoryTheory.diagonalsConeSnd {C : Type u} [Category.{v, u} C] {A B X Y : C} (l : A ⟶ B) (r : X ⟶ Y) : diagonalsConePoint l r ⟶ A ⟶ X

Imported FactorizationSystems declaration.

Equations

• CategoryTheory.diagonalsConeSnd l r = (CategoryTheory.diagonalsCone l r).snd

noncomputable def CategoryTheory.diagonalsHomCospanLift {C : Type u} [Category.{v, u} C] {A B X Y : C} (l : A ⟶ B) (r : X ⟶ Y) : diagonalsConePoint l r ⟶ homPullbackConePoint l r

Imported FactorizationSystems declaration.

Equations

• CategoryTheory.diagonalsHomCospanLift l r = (CategoryTheory.homPullbackConeIsLimit l r).lift (CategoryTheory.diagonalsCone l r)

theorem CategoryTheory.diagonals_hom_cospan_lift_fst {C : Type u} [Category.{v, u} C] {A B X Y : C} (l : A ⟶ B) (r : X ⟶ Y) : CategoryStruct.comp (diagonalsHomCospanLift l r) (homPullbackFst l r) = (homSquare l r).top

theorem CategoryTheory.diagonals_hom_cospan_lift_snd {C : Type u} [Category.{v, u} C] {A B X Y : C} (l : A ⟶ B) (r : X ⟶ Y) : CategoryStruct.comp (diagonalsHomCospanLift l r) (homPullbackSnd l r) = (homSquare l r).left

@[reducible]

def CategoryTheory.homOrthogonalAux {C : Type u} [Category.{v, u} C] {A B X Y : C} (l : A ⟶ B) (r : X ⟶ Y) : Prop

Imported FactorizationSystems declaration.

Equations

• CategoryTheory.homOrthogonalAux l r = CategoryTheory.IsIso (CategoryTheory.diagonalsHomCospanLift l r)

theorem CategoryTheory.hom_orthogonal_implies_hom_orthogonal_aux {C : Type u} [Category.{v, u} C] {A B X Y : C} (l : A ⟶ B) (r : X ⟶ Y) (h : homOrthogonal l r) : homOrthogonal l r

theorem CategoryTheory.hom_orthogonal_aux_implies_hom_orthogonal {C : Type u} [Category.{v, u} C] {A B X Y : C} (l : A ⟶ B) (r : X ⟶ Y) (h : homOrthogonalAux l r) : homOrthogonal l r

noncomputable def CategoryTheory.homOrthogonalAuxHom {C : Type u} [Category.{v, u} C] {A B X Y : C} (l : A ⟶ B) (r : X ⟶ Y) (h : homOrthogonalAux l r) : (B ⟶ X) ⟶ homCospanPullback l r

Imported FactorizationSystems declaration.

Equations

• CategoryTheory.homOrthogonalAuxHom l r h = (CategoryTheory.asIso (CategoryTheory.diagonalsHomCospanLift l r)).hom

noncomputable def CategoryTheory.homOrthogonalAuxInv {C : Type u} [Category.{v, u} C] {A B X Y : C} (l : A ⟶ B) (r : X ⟶ Y) (h : homOrthogonalAux l r) : homCospanPullback l r ⟶ B ⟶ X

Imported FactorizationSystems declaration.

Equations

• CategoryTheory.homOrthogonalAuxInv l r h = (CategoryTheory.asIso (CategoryTheory.diagonalsHomCospanLift l r)).inv

theorem CategoryTheory.hom_orthogonal_aux_hom_inv_id {C : Type u} [Category.{v, u} C] {A B X Y : C} (l : A ⟶ B) (r : X ⟶ Y) (h : homOrthogonalAux l r) : CategoryStruct.comp (homOrthogonalAuxHom l r h) (homOrthogonalAuxInv l r h) = CategoryStruct.id (B ⟶ X)

theorem CategoryTheory.hom_orthogonal_aux_inv_hom_id {C : Type u} [Category.{v, u} C] {A B X Y : C} (l : A ⟶ B) (r : X ⟶ Y) (h : homOrthogonalAux l r) : CategoryStruct.comp (homOrthogonalAuxInv l r h) (homOrthogonalAuxHom l r h) = CategoryStruct.id (homCospanPullback l r)

@[reducible]

noncomputable def CategoryTheory.homOrthogonalAuxLift {C : Type u} [Category.{v, u} C] {A B X Y : C} (l : A ⟶ B) (r : X ⟶ Y) (h : homOrthogonalAux l r) (s : Limits.PullbackCone (homSquare l r).right (homSquare l r).bot) : s.pt ⟶ diagonalsConePoint l r

Imported FactorizationSystems declaration.

Equations

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

theorem CategoryTheory.hom_orthogonal_aux_fac_left {C : Type u} [Category.{v, u} C] {A B X Y : C} (l : A ⟶ B) (r : X ⟶ Y) (h : homOrthogonalAux l r) (s : Limits.PullbackCone (homSquare l r).right (homSquare l r).bot) : CategoryStruct.comp (homOrthogonalAuxLift l r h s) (diagonalsConeFst l r) = s.fst

theorem CategoryTheory.hom_orthogonal_aux_fac_right {C : Type u} [Category.{v, u} C] {A B X Y : C} (l : A ⟶ B) (r : X ⟶ Y) (h : homOrthogonalAux l r) (s : Limits.PullbackCone (homSquare l r).right (homSquare l r).bot) : CategoryStruct.comp (homOrthogonalAuxLift l r h s) (diagonalsConeSnd l r) = s.snd

theorem CategoryTheory.hom_orthogonal_aux_uniq {C : Type u} [Category.{v, u} C] {A B X Y : C} (l : A ⟶ B) (r : X ⟶ Y) (h : homOrthogonalAux l r) (s : Limits.PullbackCone (homSquare l r).right (homSquare l r).bot) (m : s.pt ⟶ B ⟶ X) : CategoryStruct.comp m (homSquare l r).top = s.fst → CategoryStruct.comp m (homSquare l r).left = s.snd → m = homOrthogonalAuxLift l r h s

noncomputable def CategoryTheory.homOrthogonalAuxImpliesIsPullbackDiagonals {C : Type u} [Category.{v, u} C] {A B X Y : C} (l : A ⟶ B) (r : X ⟶ Y) (h : homOrthogonalAux l r) : Limits.IsLimit (diagonalsCone l r)

Imported FactorizationSystems declaration.

Equations

• CategoryTheory.homOrthogonalAuxImpliesIsPullbackDiagonals l r h = CategoryTheory.Limits.PullbackCone.IsLimit.mk ⋯ (CategoryTheory.homOrthogonalAuxLift l r h) ⋯ ⋯ ⋯

def CategoryTheory.squareCompletionConeSnd {C : Type u} [Category.{v, u} C] {A B X Y : C} (l : A ⟶ B) (r : X ⟶ Y) (S : l □ r) : PUnit.{v + 1} ⟶ A ⟶ X

Imported FactorizationSystems declaration.

Equations

• CategoryTheory.squareCompletionConeSnd l r S = TypeCat.ofHom fun (x : PUnit.{?u.1 + 1}) => S.top

def CategoryTheory.squareCompletionConeFst {C : Type u} [Category.{v, u} C] {A B X Y : C} (l : A ⟶ B) (r : X ⟶ Y) (S : l □ r) : PUnit.{v + 1} ⟶ B ⟶ Y

Imported FactorizationSystems declaration.

Equations

• CategoryTheory.squareCompletionConeFst l r S = TypeCat.ofHom fun (x : PUnit.{?u.1 + 1}) => S.bot

theorem CategoryTheory.square_completion_cone_comm {C : Type u} [Category.{v, u} C] {A B X Y : C} (l : A ⟶ B) (r : X ⟶ Y) (S : l □ r) : CategoryStruct.comp (squareCompletionConeFst l r S) (homSquare l r).right = CategoryStruct.comp (squareCompletionConeSnd l r S) (homSquare l r).bot

def CategoryTheory.squareCompletionCone {C : Type u} [Category.{v, u} C] {A B X Y : C} (l : A ⟶ B) (r : X ⟶ Y) (S : l □ r) : Limits.PullbackCone (homSquare l r).right (homSquare l r).bot

Imported FactorizationSystems declaration.

Equations

• CategoryTheory.squareCompletionCone l r S = CategoryTheory.Limits.PullbackCone.mk (CategoryTheory.squareCompletionConeFst l r S) (CategoryTheory.squareCompletionConeSnd l r S) ⋯

def CategoryTheory.diagonalFillerToPullback {C : Type u} [Category.{v, u} C] {A B X Y : C} (l : A ⟶ B) (r : X ⟶ Y) (S : l □ r) (δ : diagonalFiller S) : PUnit.{v + 1} ⟶ diagonalsConePoint l r

Imported FactorizationSystems declaration.

Equations

• CategoryTheory.diagonalFillerToPullback l r S δ = TypeCat.ofHom fun (x : PUnit.{?u.1 + 1}) => δ.map

noncomputable def CategoryTheory.isHomOrthogonalAuxImpliesIsOrthogonal {C : Type u} [Category.{v, u} C] {A B X Y : C} (l : A ⟶ B) (r : X ⟶ Y) (h : homOrthogonalAux l r) : orthogonal l r

Imported FactorizationSystems declaration.

Equations

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

noncomputable def CategoryTheory.homOrthogonalImpliesOrthogonal {C : Type u} [Category.{v, u} C] {A B X Y : C} {l : A ⟶ B} {r : X ⟶ Y} (h : homOrthogonal l r) : orthogonal l r

Imported FactorizationSystems declaration.

Equations

• CategoryTheory.homOrthogonalImpliesOrthogonal h = CategoryTheory.isHomOrthogonalAuxImpliesIsOrthogonal l r ⋯