CategoryTheory.Quotient.sound
theorem CategoryTheory.Quotient.sound :
∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] (r : HomRel C) {a b : C} {f₁ f₂ : a ⟶ b},
r f₁ f₂ → (CategoryTheory.Quotient.functor r).map f₁ = (CategoryTheory.Quotient.functor r).map f₂
The theorem `CategoryTheory.Quotient.sound` states that for any category `C`, and any `HomRel r` on `C` (which is a relation defined on the hom-sets of the category), if for any two morphisms `f₁` and `f₂` from object `a` to object `b` in `C`, if `f₁` and `f₂` are related by `r`, then their images under the quotient functor associated to `r` are equal. In simpler terms, it asserts that the quotient functor respects the relation `r`: if two morphisms are related by `r`, they get mapped to the same morphism in the quotient category.
More concisely: Given a category `C` and a relation `r` on its hom-sets such that for any morphisms `f₁` and `f₂` from object `a` to object `b`, if `f₁ r f₂`, then the images of `f₁` and `f₂` under the quotient functor associated to `r` are equal.
|
CategoryTheory.Congruence.equivalence
theorem CategoryTheory.Congruence.equivalence :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] {r : HomRel C} [self : CategoryTheory.Congruence r]
{X Y : C}, Equivalence r
The theorem `CategoryTheory.Congruence.equivalence` states that for any category `C`, and any homomorphism relation `r` on `C`, if `r` is a congruence on `C` (satisfying certain conditions specified by `self : CategoryTheory.Congruence r`), then `r` is an equivalence relation on every hom-set in `C`, i.e., for every pair of objects `X, Y` in `C`, `r` is reflexive, symmetric, and transitive on the set of morphisms from `X` to `Y`.
More concisely: For any category `C` and homomorphism relation `r` on `C` that is a congruence (satisfying certain conditions), `r` is an equivalence relation on every hom-set in `C`.
|
CategoryTheory.Congruence.compLeft
theorem CategoryTheory.Congruence.compLeft :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] {r : HomRel C} [self : CategoryTheory.Congruence r]
{X Y Z : C} (f : X ⟶ Y) {g g' : Y ⟶ Z},
r g g' → r (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.comp f g')
The theorem `CategoryTheory.Congruence.compLeft` states that for any category `C` and a homo-morphic relation `r` on `C` that is a congruence, if two morphisms `g` and `g'` from `Y` to `Z` are related by `r`, then their compositions with any morphism `f` from `X` to `Y` are also related by `r`. In other words, pre-composing `g` and `g'` with `f` preserves the relation `r`. This is a property of congruence in category theory, ensuring that related morphisms behave the same when composed with other morphisms.
More concisely: For any category \(C\), if \(r\) is a homomorphic congruence relation on \(C\), then for all morphisms \(f: X \to Y\), \(g, g': Y \to Z\) such that \(g \mathrel{r} g'\), we have \(g \circ f \mathrel{r} g' \circ f\).
|
CategoryTheory.Quotient.functor_map_eq_iff
theorem CategoryTheory.Quotient.functor_map_eq_iff :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] (r : HomRel C) [h : CategoryTheory.Congruence r]
{X Y : C} (f f' : X ⟶ Y),
(CategoryTheory.Quotient.functor r).map f = (CategoryTheory.Quotient.functor r).map f' ↔ r f f'
The theorem `CategoryTheory.Quotient.functor_map_eq_iff` states that for any category `C`, given a homotopy relation `r` on the hom-sets of `C` and two morphisms `f` and `f'` from `X` to `Y` in `C`, the images of `f` and `f'` under the quotient functor associated with `r` are equal if and only if `f` and `f'` are related by `r`. This means that the quotient functor respects the relation `r` in the sense that it identifies any two morphisms that are related by `r`.
More concisely: For any category `C` and homotopy relation `r` on its hom-sets, the quotient functor identifies morphisms related by `r`.
|
CategoryTheory.Congruence.compRight
theorem CategoryTheory.Congruence.compRight :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] {r : HomRel C} [self : CategoryTheory.Congruence r]
{X Y Z : C} {f f' : X ⟶ Y} (g : Y ⟶ Z),
r f f' → r (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.comp f' g)
The theorem `CategoryTheory.Congruence.compRight` states that for any category `C` with a hom-set relation `r` (which is a congruence), given objects `X`, `Y`, `Z` of `C` and two morphisms `f` and `f'` from `X` to `Y`, and a morphism `g` from `Y` to `Z`, if `f` and `f'` are related under `r` then their compositions with `g` (`f` followed by `g`, and `f'` followed by `g`) are also related under `r`. This means that the hom-set relation `r` respects the composition operation on morphisms in the category, a property known as right-compatibility.
More concisely: If `r` is a congruence on the hom-sets of a category `C`, then for all objects `X`, `Y`, `Z` and morphisms `f ≈_r f'` from `X` to `Y` and `g : Y → Z`, `f ∘ g ≈_r f' ∘ g`.
|
CategoryTheory.Quotient.CompClosure.of
theorem CategoryTheory.Quotient.CompClosure.of :
∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] (r : HomRel C) {a b : C} (m₁ m₂ : a ⟶ b),
r m₁ m₂ → CategoryTheory.Quotient.CompClosure r m₁ m₂
This theorem states that for any category `C` and any relation `r` that assigns a relation to each hom-set in `C`, if `m₁` and `m₂` are two morphisms from object `a` to object `b` in `C` and `m₁` is related to `m₂` under this relation `r`, then `m₁` and `m₂` are also related under the quotient of this relation with respect to composition, which is called the `CompClosure` of `r`. In simpler words, the relation preserves the composition of morphisms in the category `C`.
More concisely: If relation `r` on hom-sets of a category `C` is such that `r(f) r(g)` whenever `f: a -> b` and `g: b -> c` are morphisms with `f` related to `g`, then `r` is a relation of composition in `C`.
|