CategoryTheory.Subobject.eq_mk_of_comm
theorem CategoryTheory.Subobject.eq_mk_of_comm :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {B A : C} {X : CategoryTheory.Subobject B} (f : A ⟶ B)
[inst_1 : CategoryTheory.Mono f] (i : CategoryTheory.Subobject.underlying.obj X ≅ A),
CategoryTheory.CategoryStruct.comp i.hom f = X.arrow → X = CategoryTheory.Subobject.mk f
This theorem establishes a condition for the equality of two subobjects in a category. Specifically, for any category `C`, any objects `A` and `B` of `C`, a subobject `X` of `B`, and a monomorphism `f: A ⟶ B`, if there exists an isomorphism `i` that commutes with the arrow of `X` and the composite of `i.hom` and `f`, then `X` is equal to the subobject of `B` created by `f`. In other words, two subobjects are equal if there is an isomorphism between their underlying objects that preserves the structure of the category.
More concisely: Given any category `C`, objects `A`, `B` of `C`, a subobject `X` of `B`, a monomorphism `f: A ⟶ B`, and an isomorphism `i: X ≅ Im(f)` commuting with `X.map f` and `i.hom ∘ f`, then `X = Im(f)`.
|
CategoryTheory.Subobject.exists_iso_map
theorem CategoryTheory.Subobject.exists_iso_map :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasImages C]
(f : X ⟶ Y) [inst_2 : CategoryTheory.Mono f],
CategoryTheory.Subobject.exists f = CategoryTheory.Subobject.map f
This theorem states that in the context of category theory, when `f` is a monomorphism from object `X` to object `Y`, the operation of "existence" applied to `f` is equivalent to the operation of "mapping" applied to `f`. More specifically, for any category `C` that has images and for any objects `X` and `Y` in `C`, if `f : X ⟶ Y` is a monomorphism (an injective morphism), then the functor `exists f` agrees with the functor `map f`. These functors map subobjects of `X` to subobjects of `Y`.
More concisely: In the context of a category with images, if `f : X ⟶ Y` is a monomorphism, then the existence functor `exists f` and the mapping functor `map f` agree on subobjects of `X`, that is, `exists f(S) = map f(S)` for any subobject `S` of `X`.
|
CategoryTheory.Subobject.ofLE_arrow
theorem CategoryTheory.Subobject.ofLE_arrow :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {B : C} {X Y : CategoryTheory.Subobject B} (h : X ≤ Y),
CategoryTheory.CategoryStruct.comp (X.ofLE Y h) Y.arrow = X.arrow
This theorem states that in any category `C`, for any object `B` in `C` and for any two subobjects `X` and `Y` of `B`, if `X` is less than or equal to `Y` (denoted by `h : X ≤ Y`), then the composition of the morphism from `X` to `Y` (obtained by `CategoryTheory.Subobject.ofLE X Y h`) and the arrow from `Y` to `B` (`CategoryTheory.Subobject.arrow Y`) is equal to the arrow from `X` to `B` (`CategoryTheory.Subobject.arrow X`).
In other words, if you have two subobjects and there exists a morphism witnessing that one is less than or equal to the other, the composed morphism from the first subobject to the ambient object (through the second subobject) is the same as the direct morphism from the first subobject to the ambient object. This is a property that maintains the structure of the category when dealing with subobjects.
More concisely: In any category C, for any object B and subobjects X and Y of B with X ≤ Y, the composition of the morphisms from X to Y and from Y to B equals the morphism from X to B.
|
CategoryTheory.Subobject.underlyingIso_arrow
theorem CategoryTheory.Subobject.underlyingIso_arrow :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [inst_1 : CategoryTheory.Mono f],
CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.underlyingIso f).inv
(CategoryTheory.Subobject.mk f).arrow =
f
This theorem, `CategoryTheory.Subobject.underlyingIso_arrow`, in the field of Category Theory, states that for any category `C`, and any two objects `X` and `Y` in `C`, given a monomorphism `f` from `X` to `Y`, the composition of the inverse of the underlying isomorphism of `f` and the arrow from the subobject created by `f` to `Y` is equal to `f` itself. In other words, the arrow from the subobject gives us back our original morphism when composed with the inverse of the isomorphism.
More concisely: For any category C, if f : X → Y is a monomorphism in C, then the composition of the inverse of the underlying isomorphism of f and the arrow from the subobject of X in Y to Y is equal to f.
|
CategoryTheory.Subobject.mk_eq_mk_of_comm
theorem CategoryTheory.Subobject.mk_eq_mk_of_comm :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {B A₁ A₂ : C} (f : A₁ ⟶ B) (g : A₂ ⟶ B)
[inst_1 : CategoryTheory.Mono f] [inst_2 : CategoryTheory.Mono g] (i : A₁ ≅ A₂),
CategoryTheory.CategoryStruct.comp i.hom g = f → CategoryTheory.Subobject.mk f = CategoryTheory.Subobject.mk g
The theorem `CategoryTheory.Subobject.mk_eq_mk_of_comm` states that in order to prove the equality of two subobjects in a category, it is sufficient to demonstrate an isomorphism that commutes with the morphisms of those subobjects. More specifically, given a category `C`, objects `B`, `A₁`, and `A₂` in `C`, and morphisms `f : A₁ ⟶ B`, `g : A₂ ⟶ B` (with `f` and `g` being monomorphisms), if there exists an isomorphism `i : A₁ ≅ A₂` such that the composition of `i.hom` and `g` equals `f`, then the subobject created by `f` is equal to the subobject created by `g`. In other words, the subobjects represented by `f` and `g` are essentially the same if there is a way to "rearrange" `A₁` into `A₂` that plays nicely with `f` and `g`.
More concisely: Given a category C, monomorphisms f : A₁ ⟶ B and g : A₂ ⟶ B, if there exists an isomorphism i : A₁ ≅ A₂ such that g ∘ i.hom = f, then the subobjects of A₁ and A₂ determined by f and g are equal.
|
CategoryTheory.Subobject.le_of_comm
theorem CategoryTheory.Subobject.le_of_comm :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {B : C} {X Y : CategoryTheory.Subobject B}
(f : CategoryTheory.Subobject.underlying.obj X ⟶ CategoryTheory.Subobject.underlying.obj Y),
CategoryTheory.CategoryStruct.comp f Y.arrow = X.arrow → X ≤ Y
This theorem states that in any category `C`, for any objects `B`, `X` and `Y` of the subobject category of `B`, if there exists a morphism `f` from the underlying object of `X` to the underlying object of `Y` such that the composition of `f` and the arrow of `Y` equals the arrow of `X`, then `X` is less than or equal to `Y`. The arrow of a subobject is the morphism from an arbitrarily chosen underlying object of the subobject to the ambient object. The underlying object is the representative object in `C` for any `Subobject` of `X`.
More concisely: In any category C, if there exists a morphism from the underlying object of a subobject X of an object B to the underlying object of another subobject Y of B such that the composition is equal to the inclusion morphism of X, then X is less than or equal to Y in the subobject lattice of B.
|
CategoryTheory.Subobject.underlyingIso_hom_comp_eq_mk
theorem CategoryTheory.Subobject.underlyingIso_hom_comp_eq_mk :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [inst_1 : CategoryTheory.Mono f],
CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.underlyingIso f).hom f =
(CategoryTheory.Subobject.mk f).arrow
This theorem states that for any category 'C', and any two objects 'X' and 'Y' in 'C', given a monomorphism 'f' from 'X' to 'Y', the composition of the underlying isomorphism of 'f' and 'f' itself is equal to `CategoryTheory.Subobject.arrow` applied to the subobject created by 'f' (denoted by `CategoryTheory.Subobject.mk f`). In simpler terms, it establishes a relationship between the composition of a morphism with its underlying isomorphism and the arrow of the subobject created by the morphism itself in the context of category theory.
More concisely: For any category 'C' and monomorphism 'f' from object 'X' to object 'Y', the composition of 'f' and its underlying isomorphism equals `CategoryTheory.Subobject.arrow` of the subobject of 'Y' generated by 'f'.
|
CategoryTheory.Subobject.eq_of_comm
theorem CategoryTheory.Subobject.eq_of_comm :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {B : C} {X Y : CategoryTheory.Subobject B}
(f : CategoryTheory.Subobject.underlying.obj X ≅ CategoryTheory.Subobject.underlying.obj Y),
CategoryTheory.CategoryStruct.comp f.hom Y.arrow = X.arrow → X = Y
This theorem, `CategoryTheory.Subobject.eq_of_comm`, states that in a category 'C', for any object 'B' and two subobjects 'X' and 'Y' of 'B', if there exists an isomorphism 'f' between the underlying objects of 'X' and 'Y' such that the composition of 'f' and the arrow of 'Y' equals the arrow of 'X', then 'X' and 'Y' are the same subobject. In other words, two subobjects are considered identical if they have the same underlying object up to isomorphism, and the arrows (representing the inclusion of the subobject in the ambient object) commute with this isomorphism.
More concisely: In a category C, two subobjects X and Y of an object B are equal if there exists an isomorphism f between their underlying objects making the diagram commute: X ⟶ B ⟵ Y ≃ f ∘ Y.
|
CategoryTheory.Subobject.mk_le_mk_of_comm
theorem CategoryTheory.Subobject.mk_le_mk_of_comm :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {B A₁ A₂ : C} {f₁ : A₁ ⟶ B} {f₂ : A₂ ⟶ B}
[inst_1 : CategoryTheory.Mono f₁] [inst_2 : CategoryTheory.Mono f₂] (g : A₁ ⟶ A₂),
CategoryTheory.CategoryStruct.comp g f₂ = f₁ → CategoryTheory.Subobject.mk f₁ ≤ CategoryTheory.Subobject.mk f₂
The theorem `CategoryTheory.Subobject.mk_le_mk_of_comm` in Lean 4 states that for any category `C`, and objects `A1`, `A2` and `B` in `C`, if you have morphisms `f1` from `A1` to `B`, `f2` from `A2` to `B`, and `g` from `A1` to `A2`, such that the composition `g` followed by `f2` equals `f1`, then the subobject of `B` generated by `f1` is less than or equal to the subobject of `B` generated by `f2`. Here, `f1` and `f2` are assumed to be monomorphisms (injective morphisms), and "less than or equal to" refers to the partial order on subobjects.
More concisely: If in a category `C`, morphisms `f1 : A1 -> B`, `f2 : A2 -> B`, and `g : A1 -> A2` satisfy `g * f2 = f1` and `f1`, `f2` are monomorphisms, then `f1⁁≤ f2⁁`, where `f¹⁁` and `f²⁁` denote the subobjects of `B` generated by `f1` and `f2`, respectively.
|
CategoryTheory.Subobject.ofLE_refl
theorem CategoryTheory.Subobject.ofLE_refl :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {B : C} (X : CategoryTheory.Subobject B),
X.ofLE X ⋯ = CategoryTheory.CategoryStruct.id (CategoryTheory.Subobject.underlying.obj X)
This theorem states that for any category `C` and any object `B` in `C`, given a subobject `X` of `B`, the morphism between `X` and itself (established by the `CategoryTheory.Subobject.ofLE` function) is equivalent to the identity morphism on the underlying object of `X` in the category. In other words, for any subobject `X`, the morphism from `X` to itself is the identity on the subobject's representative object in the category `C`. It's essentially saying that the operation of witnessing an inequality between subobjects, when done on the same subobject, results in the identity morphism.
More concisely: For any category `C` and object `B` in `C`, the subobject `X` of `B` has equivalent identity and inclusion morphisms in `C`.
|
CategoryTheory.Subobject.ofMkLEMk_refl
theorem CategoryTheory.Subobject.ofMkLEMk_refl :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {B A₁ : C} (f : A₁ ⟶ B)
[inst_1 : CategoryTheory.Mono f], CategoryTheory.Subobject.ofMkLEMk f f ⋯ = CategoryTheory.CategoryStruct.id A₁
The theorem `CategoryTheory.Subobject.ofMkLEMk_refl` states that for any category `C`, and for any two objects `A₁` and `B` in this category, given a morphism `f` from `A₁` to `B` that is monic (i.e., a left-cancellative morphism), the morphism from the subobject represented by `f` to itself equals the identity morphism on `A₁`. In other words, this theorem asserts that for any monic morphism `f`, the defined morphism from the subobject of `f` to itself is the identity on the domain of `f`.
More concisely: For any monic morphism $f : A\_1 \to B$ in a category $C$, the subobject of $f$ equals the identity subobject on $A\_1$. In other words, the morphism from the subobject of $f$ to itself is the identity on $A\_1$.
|
CategoryTheory.Subobject.lower_iso
theorem CategoryTheory.Subobject.lower_iso :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C}
(F₁ F₂ : CategoryTheory.Functor (CategoryTheory.MonoOver X) (CategoryTheory.MonoOver Y)),
(F₁ ≅ F₂) → CategoryTheory.Subobject.lower F₁ = CategoryTheory.Subobject.lower F₂
The theorem `CategoryTheory.Subobject.lower_iso` states that for any category `C`, and any objects `X` and `Y` in `C`, if we have two functors `F₁` and `F₂` from the category of monomorphisms into `X` to the category of monomorphisms into `Y` which are isomorphic, then when these functors are lowered to the `Subobject` category, they become equal. This usage of equality between functors is not typically encouraged, but in this case is permissible due to the categories being thin (each hom-set has at most one morphism) and skeletal (isomorphic objects are equal).
More concisely: For any category C and objects X, Y, if functors F₁ and F₂ from the monomorphisms into X to monomorphisms into Y are isomorphic in the category of functors, then their lower instantiations in the Subobject category of X and Y are equal.
|
CategoryTheory.Subobject.eq_of_comp_arrow_eq
theorem CategoryTheory.Subobject.eq_of_comp_arrow_eq :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {P : CategoryTheory.Subobject Y}
{f g : X ⟶ CategoryTheory.Subobject.underlying.obj P},
CategoryTheory.CategoryStruct.comp f P.arrow = CategoryTheory.CategoryStruct.comp g P.arrow → f = g
The theorem `CategoryTheory.Subobject.eq_of_comp_arrow_eq` states that in any category `C`, for any objects `X` and `Y` in `C` and for any subobject `P` of `Y`, if two morphisms `f` and `g` from `X` to the underlying object of `P` have the property that their composition with the arrow from the underlying object of `P` to `Y` (denoted `CategoryTheory.Subobject.arrow P`) are equal, then the original morphisms `f` and `g` were in fact equal. In terms of category theory, this means that morphisms into a subobject are uniquely determined by their composition with the arrow to the ambient object.
More concisely: In any category, two morphisms with the same composition with the subobject arrow define equal morphisms.
|
CategoryTheory.Subobject.mk_eq_of_comm
theorem CategoryTheory.Subobject.mk_eq_of_comm :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {B A : C} {X : CategoryTheory.Subobject B} (f : A ⟶ B)
[inst_1 : CategoryTheory.Mono f] (i : A ≅ CategoryTheory.Subobject.underlying.obj X),
CategoryTheory.CategoryStruct.comp i.hom X.arrow = f → CategoryTheory.Subobject.mk f = X
This theorem states that in a given category `C`, for any two subobjects `X` and `CategoryTheory.Subobject.mk f` of an object `B`, if there exists an isomorphism `i` between an object `A` and the representative object of `X` such that the composition of `i.hom` (the morphism from `A` to `X`'s representative) and `X.arrow` (the monomorphism from `X`'s representative to `B`) is equal to `f` (the monomorphism from `A` to `B`), then `X` and `CategoryTheory.Subobject.mk f` are equal. Here, `A ⟶ B` symbolizes a morphism from `A` to `B`. The theorem bridges the gap between morphism composition and equality of subobjects in a category.
More concisely: If in a category `C`, there exists an isomorphism from an object `A` to the representative of a subobject `X` of `B`, such that the composition of this isomorphism and the inclusion morphism from `X` to `B` equals the given morphism `f` from `A` to `B`, then `X = CategoryTheory.Subobject.mk f`.
|