CategoryTheory.Limits.PushoutCocone.epi_of_isColimitMkIdId
theorem CategoryTheory.Limits.PushoutCocone.epi_of_isColimitMkIdId :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y),
CategoryTheory.Limits.IsColimit
(CategoryTheory.Limits.PushoutCocone.mk (CategoryTheory.CategoryStruct.id Y)
(CategoryTheory.CategoryStruct.id Y) ⋯) →
CategoryTheory.Epi f
The theorem `CategoryTheory.Limits.PushoutCocone.epi_of_isColimitMkIdId` states that for any category `C`, any two objects `X` and `Y` in `C`, and a morphism `f` from `X` to `Y`, if the pushout cocone formed by the identity morphism on `Y` is a colimit for the pair `(f, f)`, then `f` is an epimorphism. The converse of this theorem is given in `PushoutCocone.isColimitMkIdId`. In other words, this is a condition under which a morphism in a category can be recognized as an epimorphism using pushout cocones and colimits.
More concisely: If in a category, the identity morphism on an object Y forms a colimit for the pair (f, f) from object X, then morphism f from X to Y is an epimorphism.
|
Mathlib.CategoryTheory.Limits.Shapes.Pullbacks._auxLemma.2
theorem Mathlib.CategoryTheory.Limits.Shapes.Pullbacks._auxLemma.2 :
∀ {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 f (CategoryTheory.CategoryStruct.comp g h) =
CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h
This theorem is stating an aspect of associativity for category theory. Specifically, for any objects `W`, `X`, `Y`, and `Z` in a category, and for any morphisms `f: W ⟶ X`, `g: X ⟶ Y`, and `h: Y ⟶ Z`, the composition `(f ≫ (g ≫ h))` is equal to the composition `((f ≫ g) ≫ h)`. This is akin to saying that the order in which the morphisms are composed does not matter, as long as the order of the morphisms themselves is preserved.
More concisely: For any objects `W`, `X`, `Y`, and `Z` in a category, and morphisms `f: W ⟶ X`, `g: X ⟶ Y`, and `h: Y ⟶ Z`, the compositions `f ≫ (g ≫ h)` and `((f ≫ g) ≫ h)` are equal.
|
CategoryTheory.Limits.cospan_map_inl
theorem CategoryTheory.Limits.cospan_map_inl :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z),
(CategoryTheory.Limits.cospan f g).map CategoryTheory.Limits.WalkingCospan.Hom.inl = f
The theorem `CategoryTheory.Limits.cospan_map_inl` states that for any given category `C` and objects `X`, `Y`, and `Z` within that category, along with morphisms `f` from `X` to `Z` and `g` from `Y` to `Z`, the map of the walking cospan functor for the cospan formed by `f` and `g`, when applied to the left arrow of the walking cospan, is equal to the morphism `f`. In simpler terms, it means that if we create a cospan with `f` and `g`, and then map the left arrow of the walking cospan through this cospan, we get back the morphism `f`.
More concisely: For any category C and morphisms f : X -> Z and g : Y -> Z in C, the map of the walking cospan functor to X from the cospan (Z, f, g) is equal to f.
|
CategoryTheory.Limits.pullbackSymmetry_hom_comp_snd
theorem CategoryTheory.Limits.pullbackSymmetry_hom_comp_snd :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
[inst_1 : CategoryTheory.Limits.HasPullback f g],
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry f g).hom
CategoryTheory.Limits.pullback.snd =
CategoryTheory.Limits.pullback.fst
This theorem, `CategoryTheory.Limits.pullbackSymmetry_hom_comp_snd`, states that in any category `C`, for any objects `X`, `Y`, and `Z`, and morphisms `f : X ⟶ Z` and `g : Y ⟶ Z` that have a pullback, the composition of the morphism `hom` from the pullback symmetry of `f` and `g` and the second projection of the pullback equals the first projection of the pullback. In other words, if we take the pullback of `f` and `g`, swap the roles of `X` and `Y` (i.e., apply the pullback symmetry), then project back onto `Y`, we end up at the same place as if we had just projected onto `X` from the original pullback.
More concisely: In any category with pullbacks, given morphisms `f : X ⟶ Z` and `g : Y ⟶ Z` with a pullback, the composition of the pullback symmetry morphism of `f` and `g` with the second projection of the pullback equals the first projection of the pullback.
|
CategoryTheory.Limits.hasPullbacks_of_hasLimit_cospan
theorem CategoryTheory.Limits.hasPullbacks_of_hasLimit_cospan :
∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C]
[inst_1 :
∀ {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z}, CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.cospan f g)],
CategoryTheory.Limits.HasPullbacks C
This theorem states that if a category `C` has all limits of cospan diagrams `cospan f g` for any objects `X, Y, Z` in `C` and any morphisms `f` from `X` to `Z` and `g` from `Y` to `Z`, then `C` has pullbacks. In other words, the existence of all limits for these cospan diagrams is sufficient to ensure the existence of pullbacks in the category. A pullback is a particular type of limit in category theory, which intuitively represents the "product" of two morphisms with a common codomain.
More concisely: If a category has limits of all cospans, then it has pullbacks.
|
CategoryTheory.Limits.hasPushouts_of_hasColimit_span
theorem CategoryTheory.Limits.hasPushouts_of_hasColimit_span :
∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C]
[inst_1 :
∀ {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z}, CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.span f g)],
CategoryTheory.Limits.HasPushouts C
The theorem `CategoryTheory.Limits.hasPushouts_of_hasColimit_span` asserts that if a category `C` has all colimits of a certain kind, specifically for all diagrams of the form `span f g`, then `C` also has all pushouts. In more detail, given any three objects `X`, `Y`, `Z` in `C`, and two morphisms `f : X ⟶ Y` and `g : X ⟶ Z`, if `C` has a colimit for the diagram formed by `f` and `g` (expressed as `CategoryTheory.Limits.span f g`), then `C` satisfies the property `CategoryTheory.Limits.HasPushouts C`, meaning it has a pushout for any pair of morphisms.
More concisely: If a category has all colimits of diagrams of the form `span f g`, then it has all pushouts.
|
CategoryTheory.Limits.PullbackCone.condition
theorem CategoryTheory.Limits.PullbackCone.condition :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z}
(t : CategoryTheory.Limits.PullbackCone f g),
CategoryTheory.CategoryStruct.comp t.fst f = CategoryTheory.CategoryStruct.comp t.snd g
The theorem `CategoryTheory.Limits.PullbackCone.condition` states that for any category `C` and any three objects `X`, `Y`, `Z` in `C`, and given any two morphisms `f : X ⟶ Z` and `g : Y ⟶ Z`, for any pullback cone `t` of `f` and `g`, the composition of the first projection of the pullback cone `t` with `f` is equal to the composition of the second projection of the pullback cone `t` with `g`. This condition is essentially the defining property of a pullback in category theory. The pullback is the limit of a diagram consisting of two morphisms `f : X ⟶ Z` and `g : Y ⟶ Z` with a common codomain `Z`.
More concisely: In any category, given a pullback cone over morphisms `f : X ⟶ Z` and `g : Y ⟶ Z`, the composition of the first projection with `f` equals the composition of the second projection with `g`.
|
CategoryTheory.Limits.PullbackCone.IsLimit.hom_ext
theorem CategoryTheory.Limits.PullbackCone.IsLimit.hom_ext :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z}
{t : CategoryTheory.Limits.PullbackCone f g},
CategoryTheory.Limits.IsLimit t →
∀ {W : C} {k l : W ⟶ t.pt},
CategoryTheory.CategoryStruct.comp k t.fst = CategoryTheory.CategoryStruct.comp l t.fst →
CategoryTheory.CategoryStruct.comp k t.snd = CategoryTheory.CategoryStruct.comp l t.snd → k = l
This theorem states that in the category `C`, given a pullback cone `t` on the morphisms `f : X ⟶ Z` and `g : Y ⟶ Z`, and assuming `t` is a limit, if for any object `W` in `C` and any pair of morphisms `k, l : W ⟶ t.pt` (the apex of the pullback cone `t`), the compositions `k ≫ fst t` and `l ≫ fst t` are equal, and the compositions `k ≫ snd t` and `l ≫ snd t` are also equal, then it must be the case that `k = l`. In other words, if two morphisms into the apex of the pullback cone agree on their compositions with both projection maps of the cone, then these two morphisms are equal. This is a form of uniqueness condition for morphisms into the limit object in a pullback situation.
More concisely: Given a limit pullback cone in a category `C` with morphisms `f : X ⟶ Z` and `g : Y ⟶ Z`, if for any `W` and morphisms `k, l : W ⟶ t.pt`, `k ≫ fst t = l ≫ fst t` and `k ≫ snd t = l ≫ snd t`, then `k = l`.
|
CategoryTheory.Limits.pullback.lift_snd
theorem CategoryTheory.Limits.pullback.lift_snd :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z}
[inst_1 : CategoryTheory.Limits.HasPullback f g] (h : W ⟶ X) (k : W ⟶ Y)
(w : CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp k g),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.lift h k w)
CategoryTheory.Limits.pullback.snd =
k
The theorem `CategoryTheory.Limits.pullback.lift_snd` states that in the category `C`, for any four objects `W, X, Y, Z`, morphisms `f: X -> Z` and `g: Y -> Z`, and provided that `f` and `g` has a pullback, if you have additional morphisms `h: W -> X` and `k: W -> Y` satisfying the property that the composition of `h` and `f` equals the composition of `k` and `g`, then the composition of the pullback lift of `h` and `k` with respect to `w` (where `w` is the equality between the two compositions) and the second projection of the pullback equals `k`. In simpler terms, this theorem is about the commutativity of a certain diagram in the category `C` involving the pullback of two morphisms `f` and `g`.
More concisely: Given morphisms $f: X \to Z$, $g: Y \to Z$, $h: W \to X$, $k: W \to Y$ in a category $C$ with pullbacks, if $h \circ f = g \circ k$ and there exists a pullback of $f$ and $g$ at $Z$, then the pullback lift of $h$ and $k$ and the second projection of the pullback equal $k$.
|
CategoryTheory.Limits.pullback.map.proof_1
theorem CategoryTheory.Limits.pullback.map.proof_1 :
∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {W X Y Z S T : C} (f₁ : W ⟶ S) (f₂ : X ⟶ S)
[inst_1 : CategoryTheory.Limits.HasPullback f₁ f₂] (g₁ : Y ⟶ T) (g₂ : Z ⟶ T) (i₁ : W ⟶ Y) (i₂ : X ⟶ Z)
(i₃ : S ⟶ T),
CategoryTheory.CategoryStruct.comp f₁ i₃ = CategoryTheory.CategoryStruct.comp i₁ g₁ →
CategoryTheory.CategoryStruct.comp f₂ i₃ = CategoryTheory.CategoryStruct.comp i₂ g₂ →
CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst i₁)
g₁ =
CategoryTheory.CategoryStruct.comp
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd i₂) g₂
This theorem is a statement about the behavior of pullbacks in a category under mapping. More specifically, given a category `C` and objects `W, X, Y, Z, S, T` in `C`. If `f₁: W ⟶ S`, `f₂: X ⟶ S` are morphisms with a pullback and `g₁: Y ⟶ T`, `g₂: Z ⟶ T` are other morphisms, then for any morphisms `i₁: W ⟶ Y`, `i₂: X ⟶ Z`, and `i₃: S ⟶ T` such that `f₁ ≫ i₃ = i₁ ≫ g₁` and `f₂ ≫ i₃ = i₂ ≫ g₂`, it follows that `(pullback.fst ≫ i₁) ≫ g₁ = (pullback.snd ≫ i₂) ≫ g₂`. This asserts a certain commutativity property in the category theory concept of pullbacks.
More concisely: Given morphisms `f₁: W ⟶ S`, `f₂: X ⟶ S`, `g₁: Y ⟶ T`, `g₂: Z ⟶ T`, `i₁: W ⟶ Y`, `i₂: X ⟶ Z`, and `i₃: S ⟶ T` in a category `C` with pullbacks, if `f₁ ≫ i₃ = i₁ ≫ g₁` and `f₂ ≫ i₃ = i₂ ≫ g₂`, then the pullback of `i₁` along `g₁` is the same as the pullback of `i₂` along `g₂`. In other words, `(pullback.fst ≫ i₁) ≫ g₁ = (pullback.snd ≫ i₂) ≫ g₂`.
|
CategoryTheory.Limits.pullbackSymmetry_hom_comp_fst_assoc
theorem CategoryTheory.Limits.pullbackSymmetry_hom_comp_fst_assoc :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
[inst_1 : CategoryTheory.Limits.HasPullback f g] {Z_1 : C} (h : Y ⟶ Z_1),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry f g).hom
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst h) =
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd h
This theorem, `CategoryTheory.Limits.pullbackSymmetry_hom_comp_fst_assoc`, from the field of Category Theory asserts the following:
Given a category `C`, three objects `X`, `Y`, and `Z` in `C`, and two morphisms `f: X ⟶ Z` and `g: Y ⟶ Z`, if there exists a pullback for `f` and `g`, then for any object `Z_1` in `C` and a morphism `h: Y ⟶ Z_1`, the composition of the homomorphism of the pullback symmetry of `f` and `g`, with the composition of the first projection of the pullback and `h`, is equal to the composition of the second projection of the pullback and `h`.
In simple terms, it states that under certain conditions, the two different routes of composing morphisms in the pullback of `f` and `g` result in the same morphism. The conditions require the existence of a pullback for `f` and `g` and the existence of a morphism `h` from `Y` to another object `Z_1`.
More concisely: Given a pullback diagram of morphisms `f: X ⟶ Z`, `g: Y ⟶ Z` in a category `C` and a morphism `h: Y ⟶ Z_1`, the composition of the pullback symmetry of `f` and `g` with `h`, and the composition of the first projection of the pullback with `h`, are equal.
|
CategoryTheory.Limits.PushoutCocone.coequalizer_ext
theorem CategoryTheory.Limits.PushoutCocone.coequalizer_ext :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z}
(t : CategoryTheory.Limits.PushoutCocone f g) {W : C} {k l : t.pt ⟶ W},
CategoryTheory.CategoryStruct.comp t.inl k = CategoryTheory.CategoryStruct.comp t.inl l →
CategoryTheory.CategoryStruct.comp t.inr k = CategoryTheory.CategoryStruct.comp t.inr l →
∀ (j : CategoryTheory.Limits.WalkingSpan),
CategoryTheory.CategoryStruct.comp (t.ι.app j) k = CategoryTheory.CategoryStruct.comp (t.ι.app j) l
This theorem is a statement about category theory, specifically dealing with the concept of a pushout cocone. The theorem states that to verify whether a morphism is coequalized by the maps of a pushout cocone, it is sufficient to check this condition only for the morphisms `inl t` and `inr t`. In more detail, given a category `C`, objects `X`, `Y`, and `Z` in `C`, morphisms `f : X ⟶ Y` and `g : X ⟶ Z`, a pushout cocone `t` of `f` and `g`, another object `W` in `C`, and two morphisms `k, l : t.pt ⟶ W`, if the compositions `t.inl ≫ k` and `t.inl ≫ l` are equal, and `t.inr ≫ k` and `t.inr ≫ l` are also equal, then for every object `j` of the indexing category of the pushout (which is a WalkingSpan), the compositions `(t.ι.app j) ≫ k` and `(t.ι.app j) ≫ l` are equal.
More concisely: Given a pushout cocone `t` of morphisms `f : X ⟶ Y` and `g : X ⟶ Z` in a category `C`, if `k` and `l` commute with both `inl` and `inr` of the cocone, then they commute with all components `t.ι.app j` of the cocone's universal arrow.
|
Mathlib.CategoryTheory.Limits.Shapes.Pullbacks._auxLemma.3
theorem Mathlib.CategoryTheory.Limits.Shapes.Pullbacks._auxLemma.3 :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (α : X ≅ Y) {f : X ⟶ Z} {g : Y ⟶ Z},
(CategoryTheory.CategoryStruct.comp α.inv f = g) = (f = CategoryTheory.CategoryStruct.comp α.hom g)
This theorem, from the field of Category Theory in Mathematics, states that for any category `C` and objects `X`, `Y`, and `Z` in `C`, given an isomorphism `α` from `X` to `Y`, and morphisms `f` from `X` to `Z` and `g` from `Y` to `Z`, the composition of the inverse of `α` and `f` being equal to `g` is equivalent to `f` being equal to the composition of `α` and `g`. In simpler terms, it essentially describes a property of isomorphisms in the context of composing morphisms in a category.
More concisely: For any category C, given isomorphisms α : X ↔ Y and f : X -> Z in C, if α⁻¹ * f = g : Y -> Z for some g, then f = α * g.
|
CategoryTheory.Limits.pushout.inr_desc
theorem CategoryTheory.Limits.pushout.inr_desc :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z}
[inst_1 : CategoryTheory.Limits.HasPushout f g] (h : Y ⟶ W) (k : Z ⟶ W)
(w : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k),
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr (CategoryTheory.Limits.pushout.desc h k w) =
k
The theorem `CategoryTheory.Limits.pushout.inr_desc` states that in any category `C`, given objects `W`, `X`, `Y`, `Z` and morphisms `f` from `X` to `Y`, `g` from `X` to `Z`, `h` from `Y` to `W`, and `k` from `Z` to `W`, if the pushout of f and g exists (`CategoryTheory.Limits.HasPushout f g`), and the composition of `f` and `h` equals the composition of `g` and `k` (expressed as `CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k`), then the composition of the second inclusion into the pushout of `f` and `g` and the morphism `CategoryTheory.Limits.pushout.desc h k w` described by the universal property of the pushout equals `k`. In simpler terms, this theorem encapsulates one of the defining properties of a pushout in category theory.
More concisely: In a category with pushouts, if the pushout of morphisms `f` and `g` exists and `f ∘ h = g ∘ k`, then the morphism `h` factors through the pushout via `k`.
|
CategoryTheory.Limits.fst_eq_snd_of_mono_eq
theorem CategoryTheory.Limits.fst_eq_snd_of_mono_eq :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [inst_1 : CategoryTheory.Mono f],
CategoryTheory.Limits.pullback.fst = CategoryTheory.Limits.pullback.snd
This theorem states that in any category `C`, for any objects `X` and `Y` in `C`, if there is a monomorphism `f` from `X` to `Y`, then the first projection of the pullback of `f` and `f` (i.e., `CategoryTheory.Limits.pullback.fst`) is equal to the second projection of the pullback of `f` and `f` (i.e., `CategoryTheory.Limits.pullback.snd`). In other words, in the pullback square of a monomorphism with itself, both projections are the same. A monomorphism in category theory is a morphism that is left-cancellative, meaning that if two morphisms composed with `f` give the same result, then the two morphisms must be equal.
More concisely: In any category, for any monomorphism $f : X \rightarrow Y$, the first and second projections of the pullback of $f$ with itself are equal: $CategoryTheory.Limits.pullback.fst (pullback f f) = CategoryTheory.Limits.pullback.snd (pullback f f)$.
|
CategoryTheory.Limits.PushoutCocone.condition
theorem CategoryTheory.Limits.PushoutCocone.condition :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z}
(t : CategoryTheory.Limits.PushoutCocone f g),
CategoryTheory.CategoryStruct.comp f t.inl = CategoryTheory.CategoryStruct.comp g t.inr
The theorem `CategoryTheory.Limits.PushoutCocone.condition` states that for any category `C` and given three objects `X`, `Y`, `Z` within this category, and two morphisms `f : X ⟶ Y` and `g : X ⟶ Z`, for any pushout cocone `t` of `f` and `g`, the composition of `f` with the first inclusion of `t` (denoted as `CategoryTheory.Limits.PushoutCocone.inl t`) is equal to the composition of `g` with the second inclusion of `t` (denoted as `CategoryTheory.Limits.PushoutCocone.inr t`). This is a fundamental condition for the pushout cocone in category theory, ensuring that the diagram commutes.
More concisely: For any category C and morphisms f : X ⟶ Y and g : X ⟶ Z in C, if t is a pushout cocone of f and g, then f ∘ CategoryTheory.Limits.PushoutCocone.inl t = g ∘ CategoryTheory.Limits.PushoutCocone.inr t.
|
CategoryTheory.Limits.hasPullback_symmetry
theorem CategoryTheory.Limits.hasPullback_symmetry :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
[inst_1 : CategoryTheory.Limits.HasPullback f g], CategoryTheory.Limits.HasPullback g f
The theorem `CategoryTheory.Limits.hasPullback_symmetry` states that for any category `C` and objects `X`, `Y`, `Z` in `C`, if a pullback exists for a pair of morphisms `f : X ⟶ Z` and `g : Y ⟶ Z`, then a pullback also exists for the pair `g : Y ⟶ Z` and `f : X ⟶ Z`. In other words, the existence of a pullback in a category is invariant under swapping the morphisms. This theorem is necessary for the robustness and generality of concepts in category theory, but making it a global instance would cause an infinite loop in the typeclass search, hence it is defined as a standalone theorem.
More concisely: If objects X, Y, Z in a category C and morphisms f : X ⟶ Z and g : Y ⟶ Z have a pullback, then so do g and f.
|
CategoryTheory.Limits.pullback.condition_assoc
theorem CategoryTheory.Limits.pullback.condition_assoc :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z}
[inst_1 : CategoryTheory.Limits.HasPullback f g] {Z_1 : C} (h : Z ⟶ Z_1),
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp f h) =
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd
(CategoryTheory.CategoryStruct.comp g h)
The theorem `CategoryTheory.Limits.pullback.condition_assoc` states that for any given category `C` and objects `X`, `Y`, `Z`, and `Z_1` in `C`, along with morphisms `f : X ⟶ Z`, `g : Y ⟶ Z`, and `h : Z ⟶ Z_1`, and assuming that `f` and `g` have a pullback, the composition of `pullback.fst` and `(f ≫ h)` is equal to the composition of `pullback.snd` and `(g ≫ h)`. In other words, going from the pullback to `X` via `pullback.fst` and then to `Z_1` via `f ≫ h` is the same as going from the pullback to `Y` via `pullback.snd` and then to `Z_1` via `g ≫ h`. This captures the universal property of the pullback in category theory: it's the unique object that allows us to commute around the square formed by `f`, `g`, and `h`.
More concisely: Given a category `C`, objects `X`, `Y`, `Z`, and `Z_1`, morphisms `f : X ⟶ Z`, `g : Y ⟶ Z`, and `h : Z ⟶ Z_1`, and assuming the pullback of `f` and `g` exists, then `(pullback.fst ∘ f ≫ h) = (pullback.snd ∘ g ≫ h)`.
|
CategoryTheory.Limits.pullback.lift_fst
theorem CategoryTheory.Limits.pullback.lift_fst :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z}
[inst_1 : CategoryTheory.Limits.HasPullback f g] (h : W ⟶ X) (k : W ⟶ Y)
(w : CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp k g),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.lift h k w)
CategoryTheory.Limits.pullback.fst =
h
This theorem states that in any category `C`, for any four objects `W`, `X`, `Y`, `Z` and two morphisms `f : X ⟶ Z` and `g : Y ⟶ Z` such that the pullback of `f` and `g` exists, if we have two other morphisms `h : W ⟶ X` and `k : W ⟶ Y` satisfying the property that the composition of `h` and `f` is equal to the composition of `k` and `g` (represented by `w : CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp k g`), then the composition of the pullback lift of `h`, `k` and `w` with the first projection of the pullback equals `h`. This theorem is essentially verifying one of the universal properties of the pullback in category theory: the unique map into the pullback that makes the required diagrams commute.
More concisely: In any category, given morphisms `f : X ⟶ Z`, `g : Y ⟶ Z`, `h : W ⟶ X`, `k : W �re� Y`, and a pullback `p : X ⏯ Z ⨝ Y`, if `h` and `k` satisfy `comp h f = comp k g` and `w : comp (pullback.fst p) h = h`, then `comp (pullback.lift p h) (pullback.lift p k w) (pullback.snd p) = h`.
|
CategoryTheory.Limits.hasPushout_symmetry
theorem CategoryTheory.Limits.hasPushout_symmetry :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z)
[inst_1 : CategoryTheory.Limits.HasPushout f g], CategoryTheory.Limits.HasPushout g f
The theorem `CategoryTheory.Limits.hasPushout_symmetry` states that in a category `C`, for any three objects `X`, `Y`, and `Z` and for a pair of morphisms `f : X ⟶ Y` and `g : X ⟶ Z` having a pushout (which represents a particular choice of colimiting cocone for the pair of morphisms), the morphisms `g` and `f` also have a pushout. Making this a global instance, however, would cause the typeclass search to enter an infinite loop.
More concisely: In a category with pushouts, if morphisms `f : X ⟶ Y` and `g : X ⟶ Z` have a pushout, then so do `g` and `f`.
|
CategoryTheory.Limits.pushout.inl_desc
theorem CategoryTheory.Limits.pushout.inl_desc :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z}
[inst_1 : CategoryTheory.Limits.HasPushout f g] (h : Y ⟶ W) (k : Z ⟶ W)
(w : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k),
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl (CategoryTheory.Limits.pushout.desc h k w) =
h
The theorem `CategoryTheory.Limits.pushout.inl_desc` states that for any category `C` and objects `W`, `X`, `Y`, `Z` in `C`, given two morphisms `f : X ⟶ Y` and `g : X ⟶ Z`, with a pushout existing for `f` and `g`, and two morphisms `h : Y ⟶ W` and `k : Z ⟶ W` such that the composition of `f` with `h` equals the composition of `g` with `k` (denoted as `CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k`), then the composition of `CategoryTheory.Limits.pushout.inl` with `CategoryTheory.Limits.pushout.desc h k w` is equal to `h`. In terms of category theory, this is stating a property of the pushout, a type of colimit, which characterizes it up to unique isomorphism.
More concisely: Given a pushout diagram in a category `C` with objects `X`, `Y`, `Z`, and `W`, morphisms `f : X ⟶ Y`, `g : X ⟶ Z`, and compositions `h : Y ⟶ W` and `k : Z ⟶ W` satisfying `f · h = g · k`, then `CategoryTheory.Limits.pushout.inl (h, k) · w = h`, where `w` is any object in the pushout of `f` and `g`.
|
CategoryTheory.Limits.PullbackCone.equalizer_ext
theorem CategoryTheory.Limits.PullbackCone.equalizer_ext :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z}
(t : CategoryTheory.Limits.PullbackCone f g) {W : C} {k l : W ⟶ t.pt},
CategoryTheory.CategoryStruct.comp k t.fst = CategoryTheory.CategoryStruct.comp l t.fst →
CategoryTheory.CategoryStruct.comp k t.snd = CategoryTheory.CategoryStruct.comp l t.snd →
∀ (j : CategoryTheory.Limits.WalkingCospan),
CategoryTheory.CategoryStruct.comp k (t.π.app j) = CategoryTheory.CategoryStruct.comp l (t.π.app j)
The theorem `CategoryTheory.Limits.PullbackCone.equalizer_ext` states that, given a category `C`, objects `X`, `Y`, `Z` and `W` in `C`, morphisms `f : X ⟶ Z` and `g : Y ⟶ Z`, a pullback cone `t` from `f` and `g`, and two morphisms `k, l : W ⟶ t.pt`, if `k` composed with `t.fst` equals `l` composed with `t.fst` and `k` composed with `t.snd` equals `l` composed with `t.snd`, then for any object `j` in the indexing diagram of the pullback (the "walking cospan"), `k` composed with the cone's leg from `t.pt` to `j` equals `l` composed with the same leg. This theorem essentially says that to check if two morphisms are equalized by the maps of a pullback cone, it suffices to check it for the first and the second component of the cone.
More concisely: Given a pullback cone in a category and morphisms with equal components composed with the cone's legs to objects in the indexing diagram, if the components are equalized by the first and second projections of the cone, then the morphisms are equalized by the legs of the cone.
|
CategoryTheory.Limits.pullback.lift_fst_assoc
theorem CategoryTheory.Limits.pullback.lift_fst_assoc :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z}
[inst_1 : CategoryTheory.Limits.HasPullback f g] (h : W ⟶ X) (k : W ⟶ Y)
(w : CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp k g) {Z_1 : C} (h_1 : X ⟶ Z_1),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.lift h k w)
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst h_1) =
CategoryTheory.CategoryStruct.comp h h_1
The theorem `CategoryTheory.Limits.pullback.lift_fst_assoc` states that for any category `C` with objects `W`, `X`, `Y`, `Z`, `Z_1`, morphisms `f: X ⟶ Z`, `g: Y ⟶ Z`, `h: W ⟶ X`, `k: W ⟶ Y`, and `h_1: X ⟶ Z_1`, given that a pullback exists for `f` and `g`, and `h` composed with `f` equals `k` composed with `g`, the composition of `pullback.lift h k w` with the composition of `pullback.fst` and `h_1` equals the composition of `h` and `h_1`. In other words, this theorem is about the associativity property of composition in the context of pullbacks in a category.
More concisely: Given a pullback square in a category with morphisms `h`, `k`, `f`, `g`, and `h_1` such that `h` is in the pullback of `f` and `g`, `h_1 f = g k`, then `h_1 (pullback.lift h k w) = pullback.fst h (h_1 w)`.
|
CategoryTheory.Limits.pullbackSymmetry_hom_comp_fst
theorem CategoryTheory.Limits.pullbackSymmetry_hom_comp_fst :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
[inst_1 : CategoryTheory.Limits.HasPullback f g],
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry f g).hom
CategoryTheory.Limits.pullback.fst =
CategoryTheory.Limits.pullback.snd
The theorem `CategoryTheory.Limits.pullbackSymmetry_hom_comp_fst` states that in any category `C`, for any three objects `X`, `Y`, and `Z` in `C`, and for any pair of morphisms `f : X ⟶ Z` and `g : Y ⟶ Z` that have a pullback, the composition of the symmetry homomorphism of the pullback of `f` and `g` with the first projection of the pullback is equal to the second projection of the pullback. In more mathematical terms, this theorem asserts that `(pullbackSymmetry f g).hom ≫ pullback.fst = pullback.snd` in the category theory context of pullbacks.
More concisely: In any category, for morphisms `f : X ⟶ Z` and `g : Y ⟶ Z` with a pullback, the composition of the pullback symmetry isomorphism's homomorphism with the first projection equals the second projection of the pullback. That is, `(pullbackSymmetry f g).hom ≫ pullback.fst = pullback.snd`.
|
CategoryTheory.Limits.PullbackCone.mono_of_isLimitMkIdId
theorem CategoryTheory.Limits.PullbackCone.mono_of_isLimitMkIdId :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y),
CategoryTheory.Limits.IsLimit
(CategoryTheory.Limits.PullbackCone.mk (CategoryTheory.CategoryStruct.id X)
(CategoryTheory.CategoryStruct.id X) ⋯) →
CategoryTheory.Mono f
The theorem `CategoryTheory.Limits.PullbackCone.mono_of_isLimitMkIdId` states that, for any category `C` and objects `X` and `Y` in `C`, if the pullback cone created with the identity morphism on `X` as both the pullback projections is a limit for the pair `(f, f)`, where `f` is a morphism from `X` to `Y`, then `f` is a monomorphism. The converse, that a monomorphism `f` ensures the identity-based pullback cone is a limit, is given by the theorem `PullbackCone.is_id_of_mono`.
More concisely: In a category, if the identity-pullback cone of a morphism is a limit, then the morphism is a monomorphism.
|
CategoryTheory.Limits.PushoutCocone.IsColimit.hom_ext
theorem CategoryTheory.Limits.PushoutCocone.IsColimit.hom_ext :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z}
{t : CategoryTheory.Limits.PushoutCocone f g},
CategoryTheory.Limits.IsColimit t →
∀ {W : C} {k l : t.pt ⟶ W},
CategoryTheory.CategoryStruct.comp t.inl k = CategoryTheory.CategoryStruct.comp t.inl l →
CategoryTheory.CategoryStruct.comp t.inr k = CategoryTheory.CategoryStruct.comp t.inr l → k = l
This theorem, `CategoryTheory.Limits.PushoutCocone.IsColimit.hom_ext`, states that in any category `C`, for any objects `X`, `Y`, `Z`, and morphisms `f : X ⟶ Y` and `g : X ⟶ Z`, if `t` is a pushout cocone of `f` and `g` and is a colimit, then for any object `W` and any two morphisms `k, l : t.pt ⟶ W`, if the composition of `k` and `inl t` (the first inclusion of the pushout cocone) is equal to the composition of `l` and `inl t`, and the composition of `k` and `inr t` (the second inclusion of the pushout cocone) is equal to the composition of `l` and `inr t`, then `k` and `l` are the same morphism.
In other words, it says that in a category, if two morphisms `k` and `l` from the tip of a colimiting pushout cocone both compose to the same morphism with each of the cocone's inclusions, then those two morphisms must be equal.
More concisely: In a category, if two morphisms from the tip of a colimiting pushout cocone have equal compositions with both inclusive morphisms of the cocone, then they are equal.
|
CategoryTheory.Limits.inl_eq_inr_of_epi_eq
theorem CategoryTheory.Limits.inl_eq_inr_of_epi_eq :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [inst_1 : CategoryTheory.Epi f],
CategoryTheory.Limits.pushout.inl = CategoryTheory.Limits.pushout.inr
This theorem states that in any category `C`, for any objects `X` and `Y` in `C` and for any morphism `f` from `X` to `Y` that is an epimorphism (surjective), the first inclusion into the pushout of `f` and some morphism `g` is equal to the second inclusion into the pushout of `f` and `g`. In other words, if `f` is an epimorphism, then the pushout inclusions from `Y` and `Z` into the pushout of `f` and `g` are identical. This result is significant in category theory as it provides a condition under which the two different paths into a pushout coincide.
More concisely: In any category, if a morphism is an epimorphism, then the first and second inclusions into the pushout are equal.
|
CategoryTheory.Limits.pushout.hom_ext
theorem CategoryTheory.Limits.pushout.hom_ext :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z}
[inst_1 : CategoryTheory.Limits.HasPushout f g] {W : C} {k l : CategoryTheory.Limits.pushout f g ⟶ W},
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl k =
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl l →
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr k =
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr l →
k = l
This theorem, named `CategoryTheory.Limits.pushout.hom_ext`, states that in category theory, given a category `C` and objects `X`, `Y`, `Z`, `W` in `C`, and morphisms `f : X ⟶ Y`, `g : X ⟶ Z` that have a pushout, if there are two morphisms `k, l : pushout f g ⟶ W` such that the compositions of `k` and `l` with the first and second inclusion morphisms into the pushout are equal (i.e., `pushout.inl ≫ k = pushout.inl ≫ l` and `pushout.inr ≫ k = pushout.inr ≫ l`), then `k` and `l` must be the same morphism. This theorem is a form of the universal property of pushouts: a morphism from the pushout is determined uniquely by its compositions with the pushout morphisms.
More concisely: In a category, if two morphisms from the pushout of `X` into `W` of morphisms `f : X ⟶ Y` and `g : X ⟶ Z` have equal compositions with both inclusion morphisms into the pushout, then they are equal.
|
CategoryTheory.Limits.pullback.condition
theorem CategoryTheory.Limits.pullback.condition :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z}
[inst_1 : CategoryTheory.Limits.HasPullback f g],
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst f =
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd g
The `CategoryTheory.Limits.pullback.condition` theorem states that for any category `C` and any objects `X`, `Y`, `Z` in `C` with morphisms `f : X ⟶ Z` and `g : Y ⟶ Z` for which a pullback exists, the composition of the first projection of the pullback of `f` and `g` with `f` is equal to the composition of the second projection of the pullback of `f` and `g` with `g`. This equality encapsulates the universal property that defines the pullback, namely the existence of a unique morphism from `X` to `Y` making the resulting diagram commute.
More concisely: In any category, for pullback squares of morphisms `f : X ⟶ Z` and `g : Y ⟶ Z`, the composition `p_1 ∘ f = p_2 ∘ g` holds, where `p_1` and `p_2` denote the first and second projections of the pullback respectively.
|
CategoryTheory.Limits.pushout.condition
theorem CategoryTheory.Limits.pushout.condition :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z}
[inst_1 : CategoryTheory.Limits.HasPushout f g],
CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.pushout.inl =
CategoryTheory.CategoryStruct.comp g CategoryTheory.Limits.pushout.inr
The theorem `CategoryTheory.Limits.pushout.condition` asserts that, for any category `C` and any three objects `X`, `Y`, and `Z` in `C`, and morphisms `f : X ⟶ Y` and `g : X ⟶ Z` that have a pushout, the composition of `f` with the first inclusion `CategoryTheory.Limits.pushout.inl` is equal to the composition of `g` with the second inclusion `CategoryTheory.Limits.pushout.inr`. In other words, if you first apply `f` and then include the result into the pushout, you get the same thing as if you first apply `g` and then include that result into the pushout. This captures one of the defining properties of a pushout in category theory.
More concisely: Given any category `C`, objects `X`, `Y`, `Z`, morphisms `f : X ⟶ Y`, `g : X ⟶ Z` with a pushout, the diagram commutes: `f ∘ CategoryTheory.Limits.pushout.inl = CategoryTheory.Limits.pushout.inr ∘ g`.
|
CategoryTheory.Limits.pullback.hom_ext
theorem CategoryTheory.Limits.pullback.hom_ext :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z}
[inst_1 : CategoryTheory.Limits.HasPullback f g] {W : C} {k l : W ⟶ CategoryTheory.Limits.pullback f g},
CategoryTheory.CategoryStruct.comp k CategoryTheory.Limits.pullback.fst =
CategoryTheory.CategoryStruct.comp l CategoryTheory.Limits.pullback.fst →
CategoryTheory.CategoryStruct.comp k CategoryTheory.Limits.pullback.snd =
CategoryTheory.CategoryStruct.comp l CategoryTheory.Limits.pullback.snd →
k = l
The theorem `CategoryTheory.Limits.pullback.hom_ext` states that in a category `C`, given two morphisms `f : X ⟶ Z` and `g : Y ⟶ Z` with a pullback, and two morphisms `k` and `l` from some object `W` into the pullback, if the compositions of `k` and `l` with the first and second projections of the pullback are equal, then `k` and `l` must be equal.
In other words, in the category theory context, it asserts a uniqueness property for morphisms into the pullback object: any two morphisms which are equal when composed with the pullback projections are themselves equal.
More concisely: In a category, given morphisms with a pullback and equal compositions with the pullback projections, the morphisms are equal.
|
CategoryTheory.Limits.pullbackRightPullbackFstIso.proof_2
theorem CategoryTheory.Limits.pullbackRightPullbackFstIso.proof_2 :
∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {W X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (f' : W ⟶ X)
[inst_1 : CategoryTheory.Limits.HasPullback f g]
[inst_2 : CategoryTheory.Limits.HasPullback f' CategoryTheory.Limits.pullback.fst],
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst f' =
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.fst
This theorem states that in a category `C` with objects `W`, `X`, `Y`, `Z`, and morphisms `f: X ⟶ Z`, `g: Y ⟶ Z`, `f': W ⟶ X`, if `f` and `g` have a pullback and `f'` and the first projection of the pullback of `f` and `g` have a pullback, then the composition of the first projection of the pullback of `f` and `g` with `f'` is equal to the composition of the second projection of the pullback of `f` and `g` with the first projection of the pullback of `f` and `g`. This is a property of pullbacks in category theory which asserts the commutativity of a specific square diagram involving some pullbacks.
More concisely: In a category with pullbacks, if morphisms `f: X ⟶ Z`, `g: Y ⟶ Z`, `f': W ⟶ X`, and their pullbacks exist, then the composition of the first projections of their pullbacks is equal to the composition of the second projection of `f` and `g` with the first projection of the pullback of `f` and `g`.
|
CategoryTheory.Limits.PushoutCocone.condition_zero
theorem CategoryTheory.Limits.PushoutCocone.condition_zero :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z}
(t : CategoryTheory.Limits.PushoutCocone f g),
t.ι.app CategoryTheory.Limits.WalkingSpan.zero = CategoryTheory.CategoryStruct.comp f t.inl
The theorem `CategoryTheory.Limits.PushoutCocone.condition_zero` states that for any category `C` and objects `X`, `Y`, `Z` in `C` along with morphisms `f: X ⟶ Y` and `g: X ⟶ Z`, given a pushout cocone `t` of `f` and `g`, the morphism corresponding to the central point of the walking span in `t` is equal to the composition of `f` and the first inclusion of the pushout cocone `t`. In other words, in the context of category theory, this theorem expresses a fundamental property of pushout cocones concerning their compositions and inclusions.
More concisely: In any category, the morphism from the pushout of two given morphisms to their common domain is equal to the composition of those morphisms with the respective inclusions into the pushout object.
|
Mathlib.CategoryTheory.Limits.Shapes.Pullbacks._auxLemma.4
theorem Mathlib.CategoryTheory.Limits.Shapes.Pullbacks._auxLemma.4 :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (α : X ≅ Y) {f : Z ⟶ Y} {g : Z ⟶ X},
(CategoryTheory.CategoryStruct.comp f α.inv = g) = (f = CategoryTheory.CategoryStruct.comp g α.hom)
The theorem `Mathlib.CategoryTheory.Limits.Shapes.Pullbacks._auxLemma.4` from Category Theory in the Mathlib library of Lean states that for any Category `C` and any objects `X`, `Y`, and `Z` in `C`, given an isomorphism `α` from `X` to `Y`, and morphisms `f` from `Z` to `Y` and `g` from `Z` to `X`, the condition that the composition of `f` and the inverse of `α` equals `g` exactly matches the condition that `f` equals the composition of `g` and `α`. This theorem essentially shows a relationship between the composition of morphisms and the equality of morphisms in the context of a Category.
More concisely: For any category C and objects X, Y, Z, an isomorphism α from X to Y, and morphisms f from Z to Y and g from Z to X, the conditions f ∘ α^(-1) = g and g ∘ α = f are equivalent.
|
CategoryTheory.Limits.inr_comp_pushoutSymmetry_hom
theorem CategoryTheory.Limits.inr_comp_pushoutSymmetry_hom :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z)
[inst_1 : CategoryTheory.Limits.HasPushout f g],
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr
(CategoryTheory.Limits.pushoutSymmetry f g).hom =
CategoryTheory.Limits.pushout.inl
This theorem states that in any category `C`, for any objects `X`, `Y`, and `Z` and morphisms `f : X ⟶ Y` and `g : X ⟶ Z` such that the pushout of `f` and `g` exists, the composition of the second inclusion into the pushout after the pushout symmetry homomorphism is equal to the first inclusion into the pushout. In other words, if we travel along the second inclusion into the pushout and then use the pushout symmetry homomorphism, it is the same as taking the first inclusion into the pushout directly. This is a specific property of the "pushout" construction in category theory, which is a kind of colimit.
More concisely: In any category with pushouts, the second inclusion into the pushout of two morphisms is equal to the composition of the first inclusion, pushout symmetry homomorphism.
|