The lattice of subobjects #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
We provide the semilattice_inf with order_top (subobject X) instance when [has_pullback C],
and the semilattice_sup (subobject X) instance when [has_images C] [has_binary_coproducts C].
@[protected, instance]
Equations
@[protected, instance]
Equations
def
category_theory.mono_over.le_top
{C : Type u₁}
[category_theory.category C]
{X : C}
(f : category_theory.mono_over X) :
The morphism to the top object in mono_over X.
Equations
@[simp]
@[simp]
def
category_theory.mono_over.map_top
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.mono f] :
map f sends ⊤ : mono_over X to ⟨X, f⟩ : mono_over Y.
noncomputable
def
category_theory.mono_over.pullback_top
{C : Type u₁}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_pullbacks C]
(f : X ⟶ Y) :
The pullback of the top object in mono_over Y
is (isomorphic to) the top object in mono_over X.
noncomputable
def
category_theory.mono_over.top_le_pullback_self
{C : Type u₁}
[category_theory.category C]
[category_theory.limits.has_pullbacks C]
{A B : C}
(f : A ⟶ B)
[category_theory.mono f] :
There is a morphism from ⊤ : mono_over A to the pullback of a monomorphism along itself;
as the category is thin this is an isomorphism.
noncomputable
def
category_theory.mono_over.pullback_self
{C : Type u₁}
[category_theory.category C]
[category_theory.limits.has_pullbacks C]
{A B : C}
(f : A ⟶ B)
[category_theory.mono f] :
The pullback of a monomorphism along itself is isomorphic to the top object.
@[protected, instance]
noncomputable
def
category_theory.mono_over.has_bot
{C : Type u₁}
[category_theory.category C]
[category_theory.limits.has_initial C]
[category_theory.limits.initial_mono_class C]
{X : C} :
Equations
- category_theory.mono_over.has_bot = {bot := category_theory.mono_over.mk' (category_theory.limits.initial.to X) category_theory.mono_over.has_bot._proof_1}
@[simp]
theorem
category_theory.mono_over.bot_left
{C : Type u₁}
[category_theory.category C]
[category_theory.limits.has_initial C]
[category_theory.limits.initial_mono_class C]
(X : C) :
@[simp]
theorem
category_theory.mono_over.bot_arrow
{C : Type u₁}
[category_theory.category C]
[category_theory.limits.has_initial C]
[category_theory.limits.initial_mono_class C]
{X : C} :
noncomputable
def
category_theory.mono_over.bot_le
{C : Type u₁}
[category_theory.category C]
[category_theory.limits.has_initial C]
[category_theory.limits.initial_mono_class C]
{X : C}
(f : category_theory.mono_over X) :
The (unique) morphism from ⊥ : mono_over X to any other f : mono_over X.
Equations
noncomputable
def
category_theory.mono_over.map_bot
{C : Type u₁}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_initial C]
[category_theory.limits.initial_mono_class C]
(f : X ⟶ Y)
[category_theory.mono f] :
map f sends ⊥ : mono_over X to ⊥ : mono_over Y.
noncomputable
def
category_theory.mono_over.bot_coe_iso_zero
{C : Type u₁}
[category_theory.category C]
[category_theory.limits.has_zero_object C]
{B : C} :
The object underlying ⊥ : subobject B is (up to isomorphism) the zero object.
@[simp]
theorem
category_theory.mono_over.bot_arrow_eq_zero
{C : Type u₁}
[category_theory.category C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_zero_morphisms C]
{B : C} :
@[simp]
theorem
category_theory.mono_over.inf_map_app
{C : Type u₁}
[category_theory.category C]
[category_theory.limits.has_pullbacks C]
{A : C}
(f₁ f₂ : category_theory.mono_over A)
(k : f₁ ⟶ f₂)
(g : category_theory.mono_over A) :
@[simp]
theorem
category_theory.mono_over.inf_obj
{C : Type u₁}
[category_theory.category C]
[category_theory.limits.has_pullbacks C]
{A : C}
(f : category_theory.mono_over A) :
noncomputable
def
category_theory.mono_over.inf
{C : Type u₁}
[category_theory.category C]
[category_theory.limits.has_pullbacks C]
{A : C} :
When [has_pullbacks C], mono_over A has "intersections", functorial in both arguments.
As mono_over A is only a preorder, this doesn't satisfy the axioms of semilattice_inf,
but we reuse all the names from semilattice_inf because they will be used to construct
semilattice_inf (subobject A) shortly.
Equations
- category_theory.mono_over.inf = {obj := λ (f : category_theory.mono_over A), category_theory.mono_over.pullback f.arrow ⋙ category_theory.mono_over.map f.arrow, map := λ (f₁ f₂ : category_theory.mono_over A) (k : f₁ ⟶ f₂), {app := λ (g : category_theory.mono_over A), category_theory.mono_over.hom_mk (category_theory.limits.pullback.lift category_theory.limits.pullback.fst (category_theory.limits.pullback.snd ≫ k.left) _) _, naturality' := _}, map_id' := _, map_comp' := _}
noncomputable
def
category_theory.mono_over.inf_le_left
{C : Type u₁}
[category_theory.category C]
[category_theory.limits.has_pullbacks C]
{A : C}
(f g : category_theory.mono_over A) :
(category_theory.mono_over.inf.obj f).obj g ⟶ f
A morphism from the "infimum" of two objects in mono_over A to the first object.
Equations
noncomputable
def
category_theory.mono_over.inf_le_right
{C : Type u₁}
[category_theory.category C]
[category_theory.limits.has_pullbacks C]
{A : C}
(f g : category_theory.mono_over A) :
(category_theory.mono_over.inf.obj f).obj g ⟶ g
A morphism from the "infimum" of two objects in mono_over A to the second object.
noncomputable
def
category_theory.mono_over.le_inf
{C : Type u₁}
[category_theory.category C]
[category_theory.limits.has_pullbacks C]
{A : C}
(f g h : category_theory.mono_over A) :
A morphism version of the le_inf axiom.
Equations
- f.le_inf g h = λ (k₁ : h ⟶ f) (k₂ : h ⟶ g), category_theory.mono_over.hom_mk (category_theory.limits.pullback.lift k₂.left k₁.left _) _
noncomputable
def
category_theory.mono_over.sup
{C : Type u₁}
[category_theory.category C]
[category_theory.limits.has_images C]
[category_theory.limits.has_binary_coproducts C]
{A : C} :
When [has_images C] [has_binary_coproducts C], mono_over A has a sup construction,
which is functorial in both arguments,
and which on subobject A will induce a semilattice_sup.
noncomputable
def
category_theory.mono_over.le_sup_left
{C : Type u₁}
[category_theory.category C]
[category_theory.limits.has_images C]
[category_theory.limits.has_binary_coproducts C]
{A : C}
(f g : category_theory.mono_over A) :
f ⟶ (category_theory.mono_over.sup.obj f).obj g
A morphism version of le_sup_left.
Equations
noncomputable
def
category_theory.mono_over.le_sup_right
{C : Type u₁}
[category_theory.category C]
[category_theory.limits.has_images C]
[category_theory.limits.has_binary_coproducts C]
{A : C}
(f g : category_theory.mono_over A) :
g ⟶ (category_theory.mono_over.sup.obj f).obj g
A morphism version of le_sup_right.
Equations
noncomputable
def
category_theory.mono_over.sup_le
{C : Type u₁}
[category_theory.category C]
[category_theory.limits.has_images C]
[category_theory.limits.has_binary_coproducts C]
{A : C}
(f g h : category_theory.mono_over A) :
A morphism version of sup_le.
@[protected, instance]
Equations
- category_theory.subobject.order_top = {top := quotient.mk' ⊤, le_top := _}
@[protected, instance]
Equations
theorem
category_theory.subobject.underlying_iso_top_hom
{C : Type u₁}
[category_theory.category C]
{B : C} :
@[protected, instance]
@[simp]
theorem
category_theory.subobject.underlying_iso_inv_top_arrow_assoc
{C : Type u₁}
[category_theory.category C]
{B X' : C}
(f' : B ⟶ X') :
@[simp]
theorem
category_theory.subobject.underlying_iso_inv_top_arrow
{C : Type u₁}
[category_theory.category C]
{B : C} :
@[simp]
theorem
category_theory.subobject.map_top
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.mono f] :
theorem
category_theory.subobject.top_factors
{C : Type u₁}
[category_theory.category C]
{A B : C}
(f : A ⟶ B) :
theorem
category_theory.subobject.is_iso_iff_mk_eq_top
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.mono f] :
theorem
category_theory.subobject.is_iso_arrow_iff_eq_top
{C : Type u₁}
[category_theory.category C]
{Y : C}
(P : category_theory.subobject Y) :
category_theory.is_iso P.arrow ↔ P = ⊤
@[protected, instance]
theorem
category_theory.subobject.mk_eq_top_of_is_iso
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.is_iso f] :
theorem
category_theory.subobject.eq_top_of_is_iso_arrow
{C : Type u₁}
[category_theory.category C]
{Y : C}
(P : category_theory.subobject Y)
[category_theory.is_iso P.arrow] :
theorem
category_theory.subobject.pullback_top
{C : Type u₁}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_pullbacks C]
(f : X ⟶ Y) :
theorem
category_theory.subobject.pullback_self
{C : Type u₁}
[category_theory.category C]
[category_theory.limits.has_pullbacks C]
{A B : C}
(f : A ⟶ B)
[category_theory.mono f] :
@[protected, instance]
noncomputable
def
category_theory.subobject.order_bot
{C : Type u₁}
[category_theory.category C]
[category_theory.limits.has_initial C]
[category_theory.limits.initial_mono_class C]
{X : C} :
Equations
- category_theory.subobject.order_bot = {bot := quotient.mk' ⊥, bot_le := _}
noncomputable
def
category_theory.subobject.bot_coe_iso_initial
{C : Type u₁}
[category_theory.category C]
[category_theory.limits.has_initial C]
[category_theory.limits.initial_mono_class C]
{B : C} :
The object underlying ⊥ : subobject B is (up to isomorphism) the initial object.
theorem
category_theory.subobject.map_bot
{C : Type u₁}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_initial C]
[category_theory.limits.initial_mono_class C]
(f : X ⟶ Y)
[category_theory.mono f] :
noncomputable
def
category_theory.subobject.bot_coe_iso_zero
{C : Type u₁}
[category_theory.category C]
[category_theory.limits.has_zero_object C]
{B : C} :
The object underlying ⊥ : subobject B is (up to isomorphism) the zero object.
theorem
category_theory.subobject.bot_eq_zero
{C : Type u₁}
[category_theory.category C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_zero_morphisms C]
{B : C} :
@[simp]
theorem
category_theory.subobject.bot_arrow
{C : Type u₁}
[category_theory.category C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_zero_morphisms C]
{B : C} :
theorem
category_theory.subobject.bot_factors_iff_zero
{C : Type u₁}
[category_theory.category C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_zero_morphisms C]
{A B : C}
(f : A ⟶ B) :
theorem
category_theory.subobject.mk_eq_bot_iff_zero
{C : Type u₁}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_zero_morphisms C]
{f : X ⟶ Y}
[category_theory.mono f] :
category_theory.subobject.mk f = ⊥ ↔ f = 0
@[simp]
theorem
category_theory.subobject.functor_obj
(C : Type u₁)
[category_theory.category C]
[category_theory.limits.has_pullbacks C]
(X : Cᵒᵖ) :
noncomputable
def
category_theory.subobject.functor
(C : Type u₁)
[category_theory.category C]
[category_theory.limits.has_pullbacks C] :
Sending X : C to subobject X is a contravariant functor Cᵒᵖ ⥤ Type.
Equations
- category_theory.subobject.functor C = {obj := λ (X : Cᵒᵖ), category_theory.subobject (opposite.unop X), map := λ (X Y : Cᵒᵖ) (f : X ⟶ Y), (category_theory.subobject.pullback f.unop).obj, map_id' := _, map_comp' := _}
@[simp]
theorem
category_theory.subobject.functor_map
(C : Type u₁)
[category_theory.category C]
[category_theory.limits.has_pullbacks C]
(X Y : Cᵒᵖ)
(f : X ⟶ Y)
(ᾰ : category_theory.subobject (opposite.unop X)) :
noncomputable
def
category_theory.subobject.inf
{C : Type u₁}
[category_theory.category C]
[category_theory.limits.has_pullbacks C]
{A : C} :
The functorial infimum on mono_over A descends to an infimum on subobject A.
theorem
category_theory.subobject.inf_le_left
{C : Type u₁}
[category_theory.category C]
[category_theory.limits.has_pullbacks C]
{A : C}
(f g : category_theory.subobject A) :
(category_theory.subobject.inf.obj f).obj g ≤ f
theorem
category_theory.subobject.inf_le_right
{C : Type u₁}
[category_theory.category C]
[category_theory.limits.has_pullbacks C]
{A : C}
(f g : category_theory.subobject A) :
(category_theory.subobject.inf.obj f).obj g ≤ g
theorem
category_theory.subobject.le_inf
{C : Type u₁}
[category_theory.category C]
[category_theory.limits.has_pullbacks C]
{A : C}
(h f g : category_theory.subobject A) :
@[protected, instance]
noncomputable
def
category_theory.subobject.semilattice_inf
{C : Type u₁}
[category_theory.category C]
[category_theory.limits.has_pullbacks C]
{B : C} :
Equations
- category_theory.subobject.semilattice_inf = {inf := λ (m n : category_theory.subobject B), (category_theory.subobject.inf.obj m).obj n, le := partial_order.le (category_theory.subobject.partial_order B), lt := partial_order.lt (category_theory.subobject.partial_order B), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, inf_le_left := _, inf_le_right := _, le_inf := _}
theorem
category_theory.subobject.factors_left_of_inf_factors
{C : Type u₁}
[category_theory.category C]
[category_theory.limits.has_pullbacks C]
{A B : C}
{X Y : category_theory.subobject B}
{f : A ⟶ B}
(h : (X ⊓ Y).factors f) :
X.factors f
theorem
category_theory.subobject.factors_right_of_inf_factors
{C : Type u₁}
[category_theory.category C]
[category_theory.limits.has_pullbacks C]
{A B : C}
{X Y : category_theory.subobject B}
{f : A ⟶ B}
(h : (X ⊓ Y).factors f) :
Y.factors f
@[simp]
theorem
category_theory.subobject.inf_factors
{C : Type u₁}
[category_theory.category C]
[category_theory.limits.has_pullbacks C]
{A B : C}
{X Y : category_theory.subobject B}
(f : A ⟶ B) :
theorem
category_theory.subobject.inf_arrow_factors_left
{C : Type u₁}
[category_theory.category C]
[category_theory.limits.has_pullbacks C]
{B : C}
(X Y : category_theory.subobject B) :
theorem
category_theory.subobject.inf_arrow_factors_right
{C : Type u₁}
[category_theory.category C]
[category_theory.limits.has_pullbacks C]
{B : C}
(X Y : category_theory.subobject B) :
@[simp]
theorem
category_theory.subobject.finset_inf_factors
{C : Type u₁}
[category_theory.category C]
[category_theory.limits.has_pullbacks C]
{I : Type u_1}
{A B : C}
{s : finset I}
{P : I → category_theory.subobject B}
(f : A ⟶ B) :
theorem
category_theory.subobject.finset_inf_arrow_factors
{C : Type u₁}
[category_theory.category C]
[category_theory.limits.has_pullbacks C]
{I : Type u_1}
{B : C}
(s : finset I)
(P : I → category_theory.subobject B)
(i : I)
(m : i ∈ s) :
theorem
category_theory.subobject.inf_eq_map_pullback'
{C : Type u₁}
[category_theory.category C]
[category_theory.limits.has_pullbacks C]
{A : C}
(f₁ : category_theory.mono_over A)
(f₂ : category_theory.subobject A) :
(category_theory.subobject.inf.obj (quotient.mk' f₁)).obj f₂ = (category_theory.subobject.map f₁.arrow).obj ((category_theory.subobject.pullback f₁.arrow).obj f₂)
theorem
category_theory.subobject.inf_eq_map_pullback
{C : Type u₁}
[category_theory.category C]
[category_theory.limits.has_pullbacks C]
{A : C}
(f₁ : category_theory.mono_over A)
(f₂ : category_theory.subobject A) :
quotient.mk' f₁ ⊓ f₂ = (category_theory.subobject.map f₁.arrow).obj ((category_theory.subobject.pullback f₁.arrow).obj f₂)
theorem
category_theory.subobject.prod_eq_inf
{C : Type u₁}
[category_theory.category C]
[category_theory.limits.has_pullbacks C]
{A : C}
{f₁ f₂ : category_theory.subobject A}
[category_theory.limits.has_binary_product f₁ f₂] :
theorem
category_theory.subobject.inf_def
{C : Type u₁}
[category_theory.category C]
[category_theory.limits.has_pullbacks C]
{B : C}
(m m' : category_theory.subobject B) :
m ⊓ m' = (category_theory.subobject.inf.obj m).obj m'
theorem
category_theory.subobject.inf_pullback
{C : Type u₁}
[category_theory.category C]
[category_theory.limits.has_pullbacks C]
{X Y : C}
(g : X ⟶ Y)
(f₁ f₂ : category_theory.subobject Y) :
(category_theory.subobject.pullback g).obj (f₁ ⊓ f₂) = (category_theory.subobject.pullback g).obj f₁ ⊓ (category_theory.subobject.pullback g).obj f₂
⊓ commutes with pullback.
theorem
category_theory.subobject.inf_map
{C : Type u₁}
[category_theory.category C]
[category_theory.limits.has_pullbacks C]
{X Y : C}
(g : Y ⟶ X)
[category_theory.mono g]
(f₁ f₂ : category_theory.subobject Y) :
(category_theory.subobject.map g).obj (f₁ ⊓ f₂) = (category_theory.subobject.map g).obj f₁ ⊓ (category_theory.subobject.map g).obj f₂
⊓ commutes with map.
noncomputable
def
category_theory.subobject.sup
{C : Type u₁}
[category_theory.category C]
[category_theory.limits.has_images C]
[category_theory.limits.has_binary_coproducts C]
{A : C} :
The functorial supremum on mono_over A descends to an supremum on subobject A.
@[protected, instance]
noncomputable
def
category_theory.subobject.semilattice_sup
{C : Type u₁}
[category_theory.category C]
[category_theory.limits.has_images C]
[category_theory.limits.has_binary_coproducts C]
{B : C} :
Equations
- category_theory.subobject.semilattice_sup = {sup := λ (m n : category_theory.subobject B), (category_theory.subobject.sup.obj m).obj n, le := partial_order.le (category_theory.subobject.partial_order B), lt := partial_order.lt (category_theory.subobject.partial_order B), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _}
theorem
category_theory.subobject.sup_factors_of_factors_left
{C : Type u₁}
[category_theory.category C]
[category_theory.limits.has_images C]
[category_theory.limits.has_binary_coproducts C]
{A B : C}
{X Y : category_theory.subobject B}
{f : A ⟶ B}
(P : X.factors f) :
theorem
category_theory.subobject.sup_factors_of_factors_right
{C : Type u₁}
[category_theory.category C]
[category_theory.limits.has_images C]
[category_theory.limits.has_binary_coproducts C]
{A B : C}
{X Y : category_theory.subobject B}
{f : A ⟶ B}
(P : Y.factors f) :
theorem
category_theory.subobject.finset_sup_factors
{C : Type u₁}
[category_theory.category C]
[category_theory.limits.has_images C]
[category_theory.limits.has_binary_coproducts C]
[category_theory.limits.has_initial C]
[category_theory.limits.initial_mono_class C]
{I : Type u_1}
{A B : C}
{s : finset I}
{P : I → category_theory.subobject B}
{f : A ⟶ B}
(h : ∃ (i : I) (H : i ∈ s), (P i).factors f) :
@[protected, instance]
noncomputable
def
category_theory.subobject.bounded_order
{C : Type u₁}
[category_theory.category C]
[category_theory.limits.has_initial C]
[category_theory.limits.initial_mono_class C]
{B : C} :
Equations
@[protected, instance]
noncomputable
def
category_theory.subobject.lattice
{C : Type u₁}
[category_theory.category C]
[category_theory.limits.has_pullbacks C]
[category_theory.limits.has_images C]
[category_theory.limits.has_binary_coproducts C]
{B : C} :
Equations
- category_theory.subobject.lattice = {sup := semilattice_sup.sup category_theory.subobject.semilattice_sup, le := semilattice_inf.le category_theory.subobject.semilattice_inf, lt := semilattice_inf.lt category_theory.subobject.semilattice_inf, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := semilattice_inf.inf category_theory.subobject.semilattice_inf, inf_le_left := _, inf_le_right := _, le_inf := _}
noncomputable
def
category_theory.subobject.wide_cospan
{C : Type u₁}
[category_theory.category C]
[category_theory.well_powered C]
{A : C}
(s : set (category_theory.subobject A)) :
The "wide cospan" diagram, with a small indexing type, constructed from a set of subobjects.
(This is just the diagram of all the subobjects pasted together, but using well_powered C
to make the diagram small.)
Equations
- category_theory.subobject.wide_cospan s = category_theory.limits.wide_pullback_shape.wide_cospan A (λ (j : ↥(⇑(equiv_shrink (category_theory.subobject A)) '' s)), ↑(⇑((equiv_shrink (category_theory.subobject A)).symm) ↑j)) (λ (j : ↥(⇑(equiv_shrink (category_theory.subobject A)) '' s)), (⇑((equiv_shrink (category_theory.subobject A)).symm) ↑j).arrow)
@[simp]
theorem
category_theory.subobject.wide_cospan_map_term
{C : Type u₁}
[category_theory.category C]
[category_theory.well_powered C]
{A : C}
(s : set (category_theory.subobject A))
(j : ↥(⇑(equiv_shrink (category_theory.subobject A)) '' s)) :
noncomputable
def
category_theory.subobject.le_Inf_cone
{C : Type u₁}
[category_theory.category C]
[category_theory.well_powered C]
{A : C}
(s : set (category_theory.subobject A))
(f : category_theory.subobject A)
(k : ∀ (g : category_theory.subobject A), g ∈ s → f ≤ g) :
Auxiliary construction of a cone for le_Inf.
Equations
@[simp]
theorem
category_theory.subobject.le_Inf_cone_π_app_none
{C : Type u₁}
[category_theory.category C]
[category_theory.well_powered C]
{A : C}
(s : set (category_theory.subobject A))
(f : category_theory.subobject A)
(k : ∀ (g : category_theory.subobject A), g ∈ s → f ≤ g) :
(category_theory.subobject.le_Inf_cone s f k).π.app option.none = f.arrow
noncomputable
def
category_theory.subobject.wide_pullback
{C : Type u₁}
[category_theory.category C]
[category_theory.well_powered C]
[category_theory.limits.has_wide_pullbacks C]
{A : C}
(s : set (category_theory.subobject A)) :
C
The limit of wide_cospan s. (This will be the supremum of the set of subobjects.)
noncomputable
def
category_theory.subobject.wide_pullback_ι
{C : Type u₁}
[category_theory.category C]
[category_theory.well_powered C]
[category_theory.limits.has_wide_pullbacks C]
{A : C}
(s : set (category_theory.subobject A)) :
The inclusion map from wide_pullback s to A
Equations
Instances for category_theory.subobject.wide_pullback_ι
@[protected, instance]
noncomputable
def
category_theory.subobject.Inf
{C : Type u₁}
[category_theory.category C]
[category_theory.well_powered C]
[category_theory.limits.has_wide_pullbacks C]
{A : C}
(s : set (category_theory.subobject A)) :
When [well_powered C] and [has_wide_pullbacks C], subobject A has arbitrary infimums.
theorem
category_theory.subobject.Inf_le
{C : Type u₁}
[category_theory.category C]
[category_theory.well_powered C]
[category_theory.limits.has_wide_pullbacks C]
{A : C}
(s : set (category_theory.subobject A))
(f : category_theory.subobject A)
(H : f ∈ s) :
theorem
category_theory.subobject.le_Inf
{C : Type u₁}
[category_theory.category C]
[category_theory.well_powered C]
[category_theory.limits.has_wide_pullbacks C]
{A : C}
(s : set (category_theory.subobject A))
(f : category_theory.subobject A)
(k : ∀ (g : category_theory.subobject A), g ∈ s → f ≤ g) :
@[protected, instance]
noncomputable
def
category_theory.subobject.complete_semilattice_Inf
{C : Type u₁}
[category_theory.category C]
[category_theory.well_powered C]
[category_theory.limits.has_wide_pullbacks C]
{B : C} :
Equations
- category_theory.subobject.complete_semilattice_Inf = {le := partial_order.le (category_theory.subobject.partial_order B), lt := partial_order.lt (category_theory.subobject.partial_order B), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, Inf := category_theory.subobject.Inf B, Inf_le := _, le_Inf := _}
noncomputable
def
category_theory.subobject.small_coproduct_desc
{C : Type u₁}
[category_theory.category C]
[category_theory.well_powered C]
[category_theory.limits.has_coproducts C]
{A : C}
(s : set (category_theory.subobject A)) :
(∐ λ (j : ↥(⇑(equiv_shrink (category_theory.subobject A)) '' s)), ↑(⇑((equiv_shrink (category_theory.subobject A)).symm) ↑j)) ⟶ A
The univesal morphism out of the coproduct of a set of subobjects,
after using [well_powered C] to reindex by a small type.
Equations
- category_theory.subobject.small_coproduct_desc s = category_theory.limits.sigma.desc (λ (j : ↥(⇑(equiv_shrink (category_theory.subobject A)) '' s)), (⇑((equiv_shrink (category_theory.subobject A)).symm) ↑j).arrow)
noncomputable
def
category_theory.subobject.Sup
{C : Type u₁}
[category_theory.category C]
[category_theory.well_powered C]
[category_theory.limits.has_coproducts C]
[category_theory.limits.has_images C]
{A : C}
(s : set (category_theory.subobject A)) :
When [well_powered C] [has_images C] [has_coproducts C],
subobject A has arbitrary supremums.
theorem
category_theory.subobject.le_Sup
{C : Type u₁}
[category_theory.category C]
[category_theory.well_powered C]
[category_theory.limits.has_coproducts C]
[category_theory.limits.has_images C]
{A : C}
(s : set (category_theory.subobject A))
(f : category_theory.subobject A)
(H : f ∈ s) :
theorem
category_theory.subobject.Sup_le
{C : Type u₁}
[category_theory.category C]
[category_theory.well_powered C]
[category_theory.limits.has_coproducts C]
[category_theory.limits.has_images C]
{A : C}
(s : set (category_theory.subobject A))
(f : category_theory.subobject A)
(k : ∀ (g : category_theory.subobject A), g ∈ s → g ≤ f) :
@[protected, instance]
noncomputable
def
category_theory.subobject.complete_semilattice_Sup
{C : Type u₁}
[category_theory.category C]
[category_theory.well_powered C]
[category_theory.limits.has_coproducts C]
[category_theory.limits.has_images C]
{B : C} :
Equations
- category_theory.subobject.complete_semilattice_Sup = {le := partial_order.le (category_theory.subobject.partial_order B), lt := partial_order.lt (category_theory.subobject.partial_order B), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, Sup := category_theory.subobject.Sup B, le_Sup := _, Sup_le := _}
@[protected, instance]
noncomputable
def
category_theory.subobject.complete_lattice
{C : Type u₁}
[category_theory.category C]
[category_theory.well_powered C]
[category_theory.limits.has_wide_pullbacks C]
[category_theory.limits.has_images C]
[category_theory.limits.has_coproducts C]
[category_theory.limits.initial_mono_class C]
{B : C} :
Equations
- category_theory.subobject.complete_lattice = {sup := semilattice_sup.sup category_theory.subobject.semilattice_sup, le := semilattice_inf.le category_theory.subobject.semilattice_inf, lt := semilattice_inf.lt category_theory.subobject.semilattice_inf, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := semilattice_inf.inf category_theory.subobject.semilattice_inf, inf_le_left := _, inf_le_right := _, le_inf := _, Sup := complete_semilattice_Sup.Sup category_theory.subobject.complete_semilattice_Sup, le_Sup := _, Sup_le := _, Inf := complete_semilattice_Inf.Inf category_theory.subobject.complete_semilattice_Inf, Inf_le := _, le_Inf := _, top := bounded_order.top category_theory.subobject.bounded_order, bot := bounded_order.bot category_theory.subobject.bounded_order, le_top := _, bot_le := _}
theorem
category_theory.subobject.nontrivial_of_not_is_zero
{C : Type u₁}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_zero_object C]
{X : C}
(h : ¬category_theory.limits.is_zero X) :
A nonzero object has nontrivial subobject lattice.
noncomputable
def
category_theory.subobject.subobject_order_iso
{C : Type u₁}
[category_theory.category C]
{X : C}
(Y : category_theory.subobject X) :
The subobject lattice of a subobject Y is order isomorphic to the interval set.Iic Y.
Equations
- Y.subobject_order_iso = {to_equiv := {to_fun := λ (Z : category_theory.subobject ↑Y), ⟨category_theory.subobject.mk (Z.arrow ≫ Y.arrow) _, _⟩, inv_fun := λ (Z : ↥(set.Iic Y)), category_theory.subobject.mk (Z.val.of_le Y _), left_inv := _, right_inv := _}, map_rel_iff' := _}