LeftFraction₂Rel

Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions

URI: https://scilib.ai/kg/mathlib#CategoryTheory.MorphismProperty.LeftFraction₂Rel

Lean4

/-- The equivalence relation on tuples of left fractions with the same denominator
for a morphism property `W`. The fact it is an equivalence relation is not
formalized, but it would follow easily from `LeftFraction₂.map_eq_iff`. -/
def LeftFraction₂Rel {X Y : C} (z₁ z₂ : W.LeftFraction₂ X Y) : Prop :=
  ∃ (Z : C) (t₁ : z₁.Y' ⟶ Z) (t₂ : z₂.Y' ⟶ Z) (_ : z₁.s ≫ t₁ = z₂.s ≫ t₂) (_ : z₁.f ≫ t₁ = z₂.f ≫ t₂) (_ :
    z₁.f' ≫ t₁ = z₂.f' ≫ t₂), W (z₁.s ≫ t₁)

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru