CategoryTheory.Subobject.inf_le_left
theorem CategoryTheory.Subobject.inf_le_left :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {A : C}
(f g : CategoryTheory.Subobject A), (CategoryTheory.Subobject.inf.obj f).obj g ≤ f
This theorem states that for any category `C` that has pullbacks and any object `A` in `C`, if we have two subobjects `f` and `g` of `A`, then the infimum of `f` and `g` (denoted by `(CategoryTheory.Subobject.inf.obj f).obj g`) is less than or equal to `f`. The infimum here refers to the greatest lower bound or "meet" of these two subobjects. In other words, any common lower bound of `f` and `g` in the partial order of subobjects of `A` must be less than or equal to the infimum of `f` and `g`.
More concisely: For any category with pullbacks and any object `A` in it, the infimum of subobjects `f` and `g` of `A` satisfies `f ⊆ (CategoryTheory.Subobject.inf.obj f).obj g`.
|
CategoryTheory.Subobject.inf_le_right
theorem CategoryTheory.Subobject.inf_le_right :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {A : C}
(f g : CategoryTheory.Subobject A), (CategoryTheory.Subobject.inf.obj f).obj g ≤ g
The theorem `CategoryTheory.Subobject.inf_le_right` states that for any category `C` with pullbacks and any object `A` in `C`, for any two subobjects `f` and `g` of `A`, the infimum of `f` and `g` (where the infimum is computed using the "inf" functor from `Subobject A` to `Subobject A`) is less than or equal to `g`. This is a formalization of the universal property of the pullback in the category of subobjects of a given object in a category. In other words, when you compute the "greatest lower bound" or infimum of `f` and `g`, the result is a subobject that is "below" `g` in the partial order of subobjects of `A`.
More concisely: For any category with pullbacks, the infimum of two subobjects of an object is less than or equal to the second subobject.
|
CategoryTheory.Subobject.nontrivial_of_not_isZero
theorem CategoryTheory.Subobject.nontrivial_of_not_isZero :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
[inst_2 : CategoryTheory.Limits.HasZeroObject C] {X : C},
¬CategoryTheory.Limits.IsZero X → Nontrivial (CategoryTheory.Subobject X)
This theorem states that in any category `C` with zero morphisms and a zero object, if `X` is a nonzero object in `C`, then the lattice of subobjects of `X` (denoted as `CategoryTheory.Subobject X`) is nontrivial. Here, a subobject of `X` is defined as an isomorphism class of monomorphisms into `X`. The `Nontrivial` predicate involves there being at least two distinct elements. So the theorem is stating that there are at least two distinct subobjects if `X` is not a zero object.
More concisely: In any category with zero morphisms and a zero object, a nonzero object has at least two distinct subobjects.
|
CategoryTheory.Subobject.inf_map
theorem CategoryTheory.Subobject.inf_map :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
{X Y : C} (g : Y ⟶ X) [inst_2 : CategoryTheory.Mono g] (f₁ f₂ : CategoryTheory.Subobject Y),
(CategoryTheory.Subobject.map g).obj (f₁ ⊓ f₂) =
(CategoryTheory.Subobject.map g).obj f₁ ⊓ (CategoryTheory.Subobject.map g).obj f₂
The theorem `CategoryTheory.Subobject.inf_map` states that for any category `C` that has pullbacks, and for any objects `X` and `Y` in `C` with a monomorphism `g` from `Y` to `X`, the operation of taking the infimum (`⊓`) of two subobjects `f₁` and `f₂` of `Y` and then mapping to `X` using `g` is the same as first mapping the individual subobjects to `X` and then taking their infimum. In other words, the operation of taking the infimum of subobjects commutes with the operation of mapping subobjects along a monomorphism.
More concisely: For any category with pullbacks and a monomorphism `g : Y ➝ X`, the infimum of `f₁ ⊓ f₂` of subobjects of `Y` is equal to `g ∘ f₁ ⊓ g ∘ f₂` of their images under `g`.
|
CategoryTheory.Subobject.isIso_iff_mk_eq_top
theorem CategoryTheory.Subobject.isIso_iff_mk_eq_top :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [inst_1 : CategoryTheory.Mono f],
CategoryTheory.IsIso f ↔ CategoryTheory.Subobject.mk f = ⊤
The theorem `CategoryTheory.Subobject.isIso_iff_mk_eq_top` in Lean 4 states that for any category `C`, and any objects `X` and `Y` in `C`, a morphism `f` from `X` to `Y` is an isomorphism if and only if the subobject generated by `f` is equal to the top element in the lattice of subobjects of `Y`. Here, the mono condition on `f` ensures that `f` really defines a subobject of `Y`.
More concisely: In category `C`, a morphism `f` from object `X` to object `Y` is an isomorphism if and only if the subobject `f''(X)` generated by `f` equals the top element in the lattice of subobjects of `Y`.
|
CategoryTheory.Subobject.isIso_arrow_iff_eq_top
theorem CategoryTheory.Subobject.isIso_arrow_iff_eq_top :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Y : C} (P : CategoryTheory.Subobject Y),
CategoryTheory.IsIso P.arrow ↔ P = ⊤
This theorem states that for any category `C` and object `Y` in `C`, a subobject `P` of `Y` in the category theory context has an isomorphism from the underlying object to the ambient object (the `arrow` of the subobject `P`), if and only if the subobject `P` is the top element (i.e., the largest subobject). In other words, the `arrow` morphism of a subobject is an isomorphism if and only if that subobject is the greatest possible subobject of the given object.
More concisely: For any object Y and subobject P in a category C, the subobject P has an isomorphism to Y if and only if P is the top element in the subobject lattice of Y.
|
CategoryTheory.Subobject.inf_pullback
theorem CategoryTheory.Subobject.inf_pullback :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
{X Y : C} (g : X ⟶ Y) (f₁ f₂ : CategoryTheory.Subobject Y),
(CategoryTheory.Subobject.pullback g).obj (f₁ ⊓ f₂) =
(CategoryTheory.Subobject.pullback g).obj f₁ ⊓ (CategoryTheory.Subobject.pullback g).obj f₂
This theorem states that the operation of "infimum" (denoted by `⊓`), commutes with the operation of "pullback" in the category theory. More specifically, given a category `C` that has pullbacks, and given objects `X` and `Y` in `C`, for any morphism `g` from `X` to `Y` and any two subobjects `f₁` and `f₂` of `Y`, the pullback of the infimum of `f₁` and `f₂` is equal to the infimum of the pullbacks of `f₁` and `f₂`. In formal mathematical terms, if we denote the pullback operation via `g` as `P_g`, this means that `P_g(f₁ ⊓ f₂) = P_g(f₁) ⊓ P_g(f₂)`.
More concisely: Given a category with pullbacks, the infimum of two subobjects commutes with the pullback of any morphism, that is, the pullback of the infimum is equal to the infimum of the pullbacks.
|