CategoryTheory.mono_of_mono_fac
theorem CategoryTheory.mono_of_mono_fac :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} {h : X ⟶ Z}
[inst_1 : CategoryTheory.Mono h], CategoryTheory.CategoryStruct.comp f g = h → CategoryTheory.Mono f
The theorem `CategoryTheory.mono_of_mono_fac` states that for any category `C` with objects `X`, `Y`, and `Z`, and morphisms `f : X ⟶ Y`, `g : Y ⟶ Z`, and `h : X ⟶ Z`, if the composition of `f` and `g` is equal to `h` and `h` is a monomorphism (i.e., injective), then `f` is also a monomorphism. In other words, if we have a monomorphism from `X` to `Z` that can be factored as the composition of two morphisms `f` and `g`, then `f` is a monomorphism as well.
More concisely: If `h : X ⟶ Z` is a monomorphism and `h = g ∘ f` for morphisms `f : X ⟶ Y` and `g : Y ⟶ Z` in a category `C`, then `f` is also a monomorphism.
|
CategoryTheory.cancel_epi
theorem CategoryTheory.cancel_epi :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) [inst_1 : CategoryTheory.Epi f]
{g h : Y ⟶ Z}, CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp f h ↔ g = h
This theorem, `CategoryTheory.cancel_epi`, states that for any category `C`, and any three objects `X`, `Y`, `Z` in `C`, given a morphism `f` from `X` to `Y` that is epi (an epimorphism, meaning that it is surjective or "onto"), and two morphisms `g` and `h` from `Y` to `Z`, the composition of `f` and `g` (`f ≫ g` in category theory notation) is equal to the composition of `f` and `h` (`f ≫ h`) if and only if `g` is equal to `h`.
In simpler terms, if we know that a morphism is an epimorphism, then if composing it with two other morphisms yields the same result, those two morphisms must be identical.
More concisely: In any category, if an epimorphism's composition with two morphisms is equal, then those morphisms are equal.
|
CategoryTheory.comp_dite
theorem CategoryTheory.comp_dite :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : Prop} [inst_1 : Decidable P] {X Y Z : C} (f : X ⟶ Y)
(g : P → (Y ⟶ Z)) (g' : ¬P → (Y ⟶ Z)),
CategoryTheory.CategoryStruct.comp f (if h : P then g h else g' h) =
if h : P then CategoryTheory.CategoryStruct.comp f (g h) else CategoryTheory.CategoryStruct.comp f (g' h)
This theorem is about the composition of morphisms in category theory, specifically within the context of a decision problem. The theorem, named `CategoryTheory.comp_dite`, states that for any category `C`, any proposition `P`, and any three objects `X`, `Y`, `Z` in `C`, for a morphism `f` from `X` to `Y`, and two morphisms `g` and `g'` from `Y` to `Z` that depend on whether `P` is true or false, the composition of `f` with the morphism chosen by a decision on `P` is equal to the composition of `f` with the morphism determined by the same decision on `P`. In other words, it doesn't matter if we decide `P` before or after composing the morphisms, the result will be the same.
More concisely: For any category C, proposition P, and objects X, Y, Z, morphisms f : X -> Y, g : Y -> Z if P then g, g' : Y -> Z if not P, the commutative diagram P->(g = g')->(f.comp.g)<-(f.comp.g') holds, i.e., f.comp.g = f.comp.g' (regardless of the order of choosing g or g' based on P).
|
CategoryTheory.Category.id_comp
theorem CategoryTheory.Category.id_comp :
∀ {obj : Type u} [self : CategoryTheory.Category.{v, u} obj] {X Y : obj} (f : X ⟶ Y),
CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id X) f = f
This theorem, `CategoryTheory.Category.id_comp`, states the principle that in the context of category theory, for any objects `X` and `Y` and any morphism `f` from `X` to `Y`, the composition of the identity morphism on `X` with `f` (`CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id X) f`) is equivalent to `f` itself. In other words, the identity morphism acts as a left identity for the operation of morphism composition.
More concisely: In category theory, for any object X and morphism f from X to Y, the identity morphism on X composed with f is equal to f. (id\_X ∘ f = f)
|
CategoryTheory.eq_whisker
theorem CategoryTheory.eq_whisker :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f g : X ⟶ Y},
f = g → ∀ (h : Y ⟶ Z), CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g h
The theorem `CategoryTheory.eq_whisker` states that in any category `C`, for any three objects `X`, `Y`, and `Z`, and for any two morphisms `f` and `g` from `X` to `Y`, if `f` is equal to `g`, then composing `f` (or equivalently `g` due to their equality) with any morphism `h` from `Y` to `Z` will result in the same morphism from `X` to `Z`. In other words, postcomposing an equality between morphisms with another morphism preserves the equality.
More concisely: In any category, if two morphisms between objects have the same source and target and are equal, then their composition with any morphism from the target to another object is equal.
|
CategoryTheory.Category.comp_id
theorem CategoryTheory.Category.comp_id :
∀ {obj : Type u} [self : CategoryTheory.Category.{v, u} obj] {X Y : obj} (f : X ⟶ Y),
CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.id Y) = f
This is a theorem in category theory that states that for any objects X and Y in a category, and any morphism f from X to Y, the composition of f with the identity morphism on Y is equal to f itself. In other words, identity morphisms serve as the right identities for the operation of morphism composition. This is expressed mathematically as `f ≫ id_Y = f` for all morphisms `f : X ⟶ Y`.
More concisely: For any morphism $f : X \to Y$ in a category, $f \circ id\_Y = f$.
|
CategoryTheory.epi_of_epi_fac
theorem CategoryTheory.epi_of_epi_fac :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} {h : X ⟶ Z}
[inst_1 : CategoryTheory.Epi h], CategoryTheory.CategoryStruct.comp f g = h → CategoryTheory.Epi g
This theorem, `CategoryTheory.epi_of_epi_fac`, states that for any Category `C` of type `Type u` and objects `X`, `Y`, and `Z` in `C`, suppose `f` is a morphism from `X` to `Y`, `g` is a morphism from `Y` to `Z`, and `h` is a morphism from `X` to `Z` which is an epimorphism (i.e., surjective in the category-theoretical sense). If the composition of `f` and `g` equals `h` (written as `CategoryTheory.CategoryStruct.comp f g = h`), then `g` is also an epimorphism. Essentially, this theorem is about preserving the property of being an epimorphism under composition in a category.
More concisely: If `h` is an epimorphism in a category `C` from `X` to `Z`, and `f: X → Y` and `g: Y → Z` are morphisms with `h = g ∘ f`, then `g` is an epimorphism.
|
CategoryTheory.dite_comp
theorem CategoryTheory.dite_comp :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : Prop} [inst_1 : Decidable P] {X Y Z : C}
(f : P → (X ⟶ Y)) (f' : ¬P → (X ⟶ Y)) (g : Y ⟶ Z),
CategoryTheory.CategoryStruct.comp (if h : P then f h else f' h) g =
if h : P then CategoryTheory.CategoryStruct.comp (f h) g else CategoryTheory.CategoryStruct.comp (f' h) g
The theorem `CategoryTheory.dite_comp` states that for any type `C` equipped with a category structure, and for any propositions `P` with a decidable instance, and for any objects `X`, `Y`, and `Z` in `C`, if we have two morphisms `f` and `f'` from `X` to `Y` that depend on whether `P` is true or not, and a morphism `g` from `Y` to `Z`, then the composition of the conditional morphism from `X` to `Y` with `g` is the same as the conditional composition of `f` or `f'` with `g`. That is, we can either first decide whether `P` is true or not and then compose, or first compose and then decide, and we get the same result either way.
More concisely: For any category `C`, propositions `P` with a decidable instance, and objects `X`, `Y`, `Z` in `C`, given morphisms `f`, `f' : X -> Y` and `g : Y -> Z`, if `P.decide` determines whether `P` holds and `g . (if P then f else f') = (if P then (f . g) else (f' . g))`, then `C` is a category with a decidable intersection type.
|
CategoryTheory.Epi.left_cancellation
theorem CategoryTheory.Epi.left_cancellation :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} [self : CategoryTheory.Epi f] {Z : C}
(g h : Y ⟶ Z), CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp f h → g = h
The theorem `CategoryTheory.Epi.left_cancellation` states that for any category `C` with objects `X`, `Y`, and `Z`, and a morphism `f` from `X` to `Y` that is an epimorphism, if two morphisms `g` and `h` from `Y` to `Z` yield the same result when composed with `f` (i.e., `f ≫ g = f ≫ h`), then `g` and `h` must be the same morphism. In other words, an epimorphism `f` allows for 'left cancellation' in the sense that precomposing with `f` preserves the distinctness of morphisms.
More concisely: Given any category C and epimorphism f: X → Y in C, if for morphisms g and h: Y → Z, we have f ∘ g = f ∘ h, then g = h.
|
CategoryTheory.mono_comp
theorem CategoryTheory.mono_comp :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) [inst_1 : CategoryTheory.Mono f]
(g : Y ⟶ Z) [inst_2 : CategoryTheory.Mono g], CategoryTheory.Mono (CategoryTheory.CategoryStruct.comp f g)
This theorem, `CategoryTheory.mono_comp`, states that in any category `C`, given objects `X`, `Y`, and `Z`, if `f` is a morphism from `X` to `Y` and `g` is a morphism from `Y` to `Z` such that `f` and `g` are both monomorphisms (injective homomorphisms in the category), then the composition of `f` and `g` (denoted by `CategoryTheory.CategoryStruct.comp f g`, or simply `f ≫ g` in categorical terms) is also a monomorphism. In other words, it says that the composition of two monomorphisms is also a monomorphism in the category `C`.
More concisely: In any category, the composition of two monomorphisms is a monomorphism.
|
CategoryTheory.mono_of_mono
theorem CategoryTheory.mono_of_mono :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z)
[inst_1 : CategoryTheory.Mono (CategoryTheory.CategoryStruct.comp f g)], CategoryTheory.Mono f
This theorem states that in any category `C`, if the composition of two morphisms `f` and `g` (where `f` maps `X` to `Y` and `g` maps `Y` to `Z`) is a monomorphism, then `f` itself is a monomorphism. In other words, if the composition `f ≫ g` is injective (which is the category theory equivalent of being a monomorphism), then `f` is also injective. "Injective" here means that if two different inputs produce the same output, then the inputs were actually the same to begin with. It's a property of a function (or morphism) that implies a certain kind of "non-collapsing" behavior.
More concisely: If `f ∘ g` is a monomorphism in a category `C`, then `f` is a monomorphism.
|
CategoryTheory.Category.assoc
theorem CategoryTheory.Category.assoc :
∀ {obj : Type u} [self : CategoryTheory.Category.{v, u} obj] {W X Y Z : obj} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z),
CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h =
CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h)
The theorem `CategoryTheory.Category.assoc` states that composition of morphisms in a category is associative. In more detail, for any category with objects of some type `obj`, and for any four objects `W`, `X`, `Y`, `Z` in this category, and any three morphisms `f : W ⟶ X`, `g : X ⟶ Y`, and `h : Y ⟶ Z`, the composition of `f` and `g` followed by `h` (notated as `(f ≫ g) ≫ h`) is the same as the composition of `f` with the composition of `g` and `h` (notated as `f ≫ (g ≫ h)`), where `≫` denotes the composition of morphisms. This is a fundamental property of categories in category theory.
More concisely: In any category, the composition of three morphisms is associative: `(f ≫ g) ≫ h = f ≫ (g ≫ h)` for all objects `W`, `X`, `Y`, `Z` and morphisms `f : W ⟶ X`, `g : X ⟶ Y`, and `h : Y ⟶ Z`.
|
CategoryTheory.cancel_mono
theorem CategoryTheory.cancel_mono :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) [inst_1 : CategoryTheory.Mono f]
{g h : Z ⟶ X}, CategoryTheory.CategoryStruct.comp g f = CategoryTheory.CategoryStruct.comp h f ↔ g = h
The theorem `CategoryTheory.cancel_mono` states that for any category `C` and any objects `X`, `Y`, and `Z` within `C`, if `f` is a monomorphism from `X` to `Y`, then for any morphisms `g` and `h` from `Z` to `X`, the composition of `g` with `f` is equal to the composition of `h` with `f` if and only if `g` is equal to `h`. In simpler terms, this theorem expresses the property of monomorphisms (or "mono") in category theory, which are morphisms that can be cancelled on the right.
More concisely: Given any category C and morphisms f: X → Y, g, h: Z → X in C, if f is a monomorphism and g = h, then g ∘ f = h ∘ f.
|
CategoryTheory.whisker_eq
theorem CategoryTheory.whisker_eq :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) {g h : Y ⟶ Z},
g = h → CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp f h
The theorem `CategoryTheory.whisker_eq` states that for any category `C`, and given objects `X`, `Y`, and `Z` of the category, and a morphism `f` from `X` to `Y` and two morphisms `g` and `h` from `Y` to `Z`, if `g` equals `h`, then the composition of `f` with `g` is equal to the composition of `f` with `h`. In other words, if two morphisms from `Y` to `Z` are equal, precomposing them with the same morphism from `X` to `Y` results in equal morphisms from `X` to `Z`. This theorem is about the compatibility of morphism composition with equality in a category.
More concisely: For any category C and morphisms f : X → Y, g, h : Y → Z in C, if g = h, then f ∘ g = f ∘ h.
|
CategoryTheory.epi_of_epi
theorem CategoryTheory.epi_of_epi :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z)
[inst_1 : CategoryTheory.Epi (CategoryTheory.CategoryStruct.comp f g)], CategoryTheory.Epi g
This theorem states that in any category `C`, if the composition of two morphisms `f` and `g`, where `f` goes from object `X` to object `Y`, and `g` goes from object `Y` to object `Z`, is an epimorphism, then the morphism `g` is also an epimorphism. In the language of category theory, an epimorphism is a morphism that is "right-cancellable", meaning that if the composition of that morphism with any other morphism equals the composition of that morphism with a different other morphism, then the two other morphisms must be equal.
More concisely: If a composition of morphisms `f: X → Y` and `g: Y → Z` in a category `C` is an epimorphism, then `g: Y → Z` is an epimorphism. (An epimorphism in a category is a morphism that is right-cancellable.)
|
CategoryTheory.epi_comp
theorem CategoryTheory.epi_comp :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) [inst_1 : CategoryTheory.Epi f]
(g : Y ⟶ Z) [inst_2 : CategoryTheory.Epi g], CategoryTheory.Epi (CategoryTheory.CategoryStruct.comp f g)
This theorem, `CategoryTheory.epi_comp`, states that in any category `C`, if there are two morphisms `f` from `X` to `Y` and `g` from `Y` to `Z` such that both `f` and `g` are epimorphisms (surjective mappings), then their composition `f ≫ g` (denoted as `CategoryTheory.CategoryStruct.comp f g` in Lean) is also an epimorphism. This conforms to the general category theory principle that the composition of two epimorphisms is again an epimorphism.
More concisely: In any category, the composition of two epimorphisms is an epimorphism.
|
CategoryTheory.Mono.right_cancellation
theorem CategoryTheory.Mono.right_cancellation :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} [self : CategoryTheory.Mono f]
{Z : C} (g h : Z ⟶ X), CategoryTheory.CategoryStruct.comp g f = CategoryTheory.CategoryStruct.comp h f → g = h
The theorem `CategoryTheory.Mono.right_cancellation` states that for any category `C`, with objects `X`, `Y`, and `Z`, and any morphism `f` from `X` to `Y` which is a monomorphism (captured by `CategoryTheory.Mono f`), if we have two morphisms `g` and `h` from `Z` to `X`, then if the composition of `g` and `f` equals the composition of `h` and `f`, it must be the case that `g` equals `h`. In other words, the morphism `f` is such that if `g ≫ f = h ≫ f` then `g = h`, where `≫` is the composition of morphisms. This property is referred to as right cancellation in category theory, illustrating the "cancellability" of `f` when it is composed after another morphism.
More concisely: If `f : X ⟶ Y` is a monomorphism in a category `C`, then `g = h` whenever `g ≫ f = h ≫ f`.
|