CategoryTheory.MorphismProperty.LeftFraction.comp₀_rel
theorem CategoryTheory.MorphismProperty.LeftFraction.comp₀_rel :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty C}
[inst_1 : W.HasLeftCalculusOfFractions] {X Y Z : C} (z₁ : W.LeftFraction X Y) (z₂ : W.LeftFraction Y Z)
(z₃ z₃' : W.LeftFraction z₁.Y' z₂.Y'),
CategoryTheory.CategoryStruct.comp z₂.f z₃.s = CategoryTheory.CategoryStruct.comp z₁.s z₃.f →
CategoryTheory.CategoryStruct.comp z₂.f z₃'.s = CategoryTheory.CategoryStruct.comp z₁.s z₃'.f →
CategoryTheory.MorphismProperty.LeftFractionRel (z₁.comp₀ z₂ z₃) (z₁.comp₀ z₂ z₃')
This theorem states that, within a given category `C` with a morphism property `W` and a left calculus of fractions defined, given objects `X`, `Y`, and `Z` in `C` and left fractions `z₁` from `X` to `Y`, `z₂` from `Y` to `Z`, and `z₃` and `z₃'` from `z₁.Y'` to `z₂.Y'`, the equivalence class of the composition of `z₁` and `z₂` with `z₃` is not dependent on the choice between `z₃` and `z₃'`, as long as both `z₃` and `z₃'` satisfy the compatibility condition that composing `z₂.f` with `z₃.s` equals composing `z₁.s` with `z₃.f` and similarly for `z₃'`.
More concisely: Given objects `X`, `Y`, `Z` in a category `C` with morphism property `W` and left calculus of fractions, and left fractions `z₁: X �הכ Y`, `z₂: Y �הכ Z`, `z₃, z₃' : z₁.Y �הכ z₂.Y`, if `z₂.f ∘ z₃ = z₁.s ∘ z₃` and `z₂.f ∘ z₃' = z₁.s ∘ z₃'`, then the equivalence classes of `z₁ ∘ z₂ ∘ z₃` and `z₁ ∘ z₂ ∘ z₃'` are equal.
|
CategoryTheory.MorphismProperty.RightFraction.hs
theorem CategoryTheory.MorphismProperty.RightFraction.hs :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y : C}
(self : W.RightFraction X Y), W self.s
The theorem `CategoryTheory.MorphismProperty.RightFraction.hs` states that for any category `C`, any morphism property `W` of `C`, and any objects `X` and `Y` in `C`, if `self` is a right fraction of `X` and `Y` that satisfies the morphism property `W`, then `self.s`, the denominator of the right fraction, also satisfies the morphism property `W`. This theorem essentially asserts that the property `W`, which is a certain condition that a morphism in category `C` may satisfy, is also satisfied by the denominator of any right fraction that satisfies `W`.
More concisely: If `self` is a right fraction of objects `X` and `Y` in a category `C` satisfying morphism property `W`, then the denominator `self.s` of `self` also satisfies the morphism property `W`.
|
CategoryTheory.MorphismProperty.LeftFraction.hs
theorem CategoryTheory.MorphismProperty.LeftFraction.hs :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y : C}
(self : W.LeftFraction X Y), W self.s
This theorem states that in any category 'C' with a given morphism property 'W', for any two objects X and Y in 'C', if there is a left fraction from X to Y that belongs to the morphism property 'W', then the denominator of that left fraction satisfies the morphism property 'W'. Here, a 'left fraction' is a construct in category theory and the 'denominator' is a component of that construct.
More concisely: If in a category with morphism property 'W', there exists a left fraction from object X to Y belonging to 'W', then the denominator of that fraction is also in 'W'.
|