CategoryTheory.StructuredArrow.lift_projectSubobject
theorem CategoryTheory.StructuredArrow.lift_projectSubobject :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v, u₂} D] {S : D} {T : CategoryTheory.Functor C D}
[inst_2 : CategoryTheory.Limits.HasLimits C] [inst_3 : CategoryTheory.Limits.PreservesLimits T]
{A : CategoryTheory.StructuredArrow S T} (P : CategoryTheory.Subobject A)
{q :
(CategoryTheory.Functor.fromPUnit S).obj A.left ⟶
T.obj (CategoryTheory.Subobject.underlying.obj (CategoryTheory.StructuredArrow.projectSubobject P))}
(hq :
CategoryTheory.CategoryStruct.comp q (T.map (CategoryTheory.StructuredArrow.projectSubobject P).arrow) = A.hom),
CategoryTheory.StructuredArrow.liftSubobject (CategoryTheory.StructuredArrow.projectSubobject P) hq = P
This theorem states that for any categories `C` and `D`, functor `T` from `C` to `D`, an object `S` in `D`, a structured arrow `A` from `S` to `T`, and a subobject `P` of `A`, given the morphism `q` from `A.left` (under the functor `fromPUnit`) to the underlying object of the projected subobject of `P`, if the composition of `q` and the map of the arrow of the projected subobject of `P` via `T` equals to the morphism of `A` (denoted as `A.hom`), then lifting the projected subobject of `P` using this equality will recover the original subobject `P`. Here, categories `C` and `D` are assumed to have all (small) limits and functor `T` is assumed to preserve these limits. In other words, projecting and then lifting a subobject will get us back to the initial subobject as long as the conditions on the morphism `q` are satisfied.
More concisely: Given categories `C`, `D`, a functor `T` from `C` to `D`, an object `S` in `D`, a structured arrow `A : S ➔ T X` and a subobject `P` of `A`, if there exists a morphism `q : A.1 ⟶ S` such that `T q . App A.hom = q`, then the lifting of `P` via `q` is equal to `P`.
|
CategoryTheory.CostructuredArrow.unop_left_comp_underlyingIso_hom_unop
theorem CategoryTheory.CostructuredArrow.unop_left_comp_underlyingIso_hom_unop :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v, u₂} D] {S : CategoryTheory.Functor C D} {T : D}
{A : CategoryTheory.CostructuredArrow S T} {P : (CategoryTheory.CostructuredArrow S T)ᵒᵖ} (f : P ⟶ Opposite.op A)
[inst_2 : CategoryTheory.Mono f.unop.left.op],
CategoryTheory.CategoryStruct.comp f.unop.left (CategoryTheory.Subobject.underlyingIso f.unop.left.op).hom.unop =
(CategoryTheory.Subobject.mk f.unop.left.op).arrow.unop
This theorem, named `CategoryTheory.CostructuredArrow.unop_left_comp_underlyingIso_hom_unop`, states a technical lemma used for the `lift_projectQuotient` operation in category theory. The lemma is about the composition of morphisms in a category and the creation of subobjects.
Specifically, for any categories `C` and `D`, functors `S` from `C` to `D`, object `T` in `D`, costructured arrow `A` from `S` to `T`, and object `P` in the opposite category of the category of costructured arrows from `S` to `T`, given a morphism `f` from `P` to the opposite of `A` that has the property of being a monomorphism when its left part is considered as an opposite, the composition of `f.unop.left` with the morphism underlying the isomorphism that comes from treating `f.unop.left.op` as a subobject, which has `unop` applied, is equal to the morphism that is the underlying arrow of the subobject created from `f.unop.left.op` with `unop` applied.
More concisely: Given functors S from C to D, objects T in D, a costructured arrow A from S to T, an object P in the opposite category of the category of costructured arrows from S to T, and a monomorphism f from P to the opposite of A with f.unop.left being an isomorphism, the underlying morphism of the subobject created from f.unop.left.op and applying unop is equal to the composition of f.unop.left.op.unop with A.unop.
|
CategoryTheory.CostructuredArrow.unop_left_comp_ofMkLEMk_unop
theorem CategoryTheory.CostructuredArrow.unop_left_comp_ofMkLEMk_unop :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v, u₂} D] {S : CategoryTheory.Functor C D} {T : D}
{A : CategoryTheory.CostructuredArrow S T} {P Q : (CategoryTheory.CostructuredArrow S T)ᵒᵖ}
{f : P ⟶ Opposite.op A} {g : Q ⟶ Opposite.op A} [inst_2 : CategoryTheory.Mono f.unop.left.op]
[inst_3 : CategoryTheory.Mono g.unop.left.op]
(h : CategoryTheory.Subobject.mk f.unop.left.op ≤ CategoryTheory.Subobject.mk g.unop.left.op),
CategoryTheory.CategoryStruct.comp g.unop.left
(CategoryTheory.Subobject.ofMkLEMk f.unop.left.op g.unop.left.op h).unop =
f.unop.left
This theorem states that for categories `C` and `D`, a functor `S` from `C` to `D`, an object `T` in `D`, and costructured arrows `A`, `P`, and `Q` with `P` and `Q` being opposites of `A`, and if morphisms `f` and `g` from `P` and `Q` to the opposite of `A` are mono (injective), then if the subobject generated by `f.unop.left.op` is less than or equal to the subobject generated by `g.unop.left.op`, the composition of `g.unop.left` and `CategoryTheory.Subobject.ofMkLEMk f.unop.left.op g.unop.left.op h`.unop is equal to `f.unop.left`.
This is a technical lemma used in the proof of `quotientEquiv`. It involves the composition of morphisms, the creation of subobjects, and the notion of monomorphisms, all fundamental concepts in category theory.
More concisely: Given categories `C` and `D`, a functor `S` from `C` to `D`, objects `T` in `D`, and morphisms `f: P -> S.op(A)` and `g: Q -> S.op(A)` in the opposite category of `S`, where `P` and `Q` are opposites of `A`, if `f` and `g` are monomorphisms, then `g.op . CategoryTheory.Subobject.ofMkLEMk f.op g.op h.op = f.op` for any morphism `h: A -> P`.
|
CategoryTheory.CostructuredArrow.lift_projectQuotient
theorem CategoryTheory.CostructuredArrow.lift_projectQuotient :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v, u₂} D] {S : CategoryTheory.Functor C D} {T : D}
[inst_2 : CategoryTheory.Limits.HasColimits C] [inst_3 : CategoryTheory.Limits.PreservesColimits S]
{A : CategoryTheory.CostructuredArrow S T} (P : CategoryTheory.Subobject (Opposite.op A))
{q :
S.obj (CategoryTheory.Subobject.underlying.obj (CategoryTheory.CostructuredArrow.projectQuotient P)).unop ⟶
(CategoryTheory.Functor.fromPUnit T).obj A.right}
(hq :
CategoryTheory.CategoryStruct.comp (S.map (CategoryTheory.CostructuredArrow.projectQuotient P).arrow.unop) q =
A.hom),
CategoryTheory.CostructuredArrow.liftQuotient (CategoryTheory.CostructuredArrow.projectQuotient P) hq = P
The theorem `CategoryTheory.CostructuredArrow.lift_projectQuotient` states that for given categories `C` and `D`, a functor `S` from `C` to `D`, an object `T` in `D` and a costructured arrow `A` from `S` to `T`, if `C` has all (small) colimits and `S` preserves these colimits, then for a subobject `P` of the opposite of `A`, and a certain morphism `q` from `S` applied to the object underlying the projection of the quotient of `P` to the object in `D` obtained from `T` via the functor from `PUnit`, if the composition of `S` applied to the arrow of the projection of `P` and `q` equals the morphism of `A`, then lifting the projection of `P` recovers the original quotient `P`. In simpler terms, the theorem describes a particular property of colimits in the context of category theory, highlighting how certain operations on morphisms and objects (like projections and lifts) preserve the structure of the category.
More concisely: Given categories C and D, a functor S from C to D preserving colimits, an object T in D, a costructured arrow A from S to T, and a subobject P of the opposite of A with quotient q in D such that the composition of S(A) and q equals the morphism of A, then lifting P along S recovers the original quotient.
|