The lattice of subobjects

We provide the SemilatticeInf with OrderTop (Subobject X) instance when [HasPullback C], and the SemilatticeSup (Subobject X) instance when [HasImages C] [HasBinaryCoproducts C].

@[implicit_reducible]

instance CategoryTheory.MonoOver.instTop {C : Type u₁} [Category.{v₁, u₁} C] {X : C} : Top (MonoOver X)

@[implicit_reducible]

instance CategoryTheory.MonoOver.instInhabited {C : Type u₁} [Category.{v₁, u₁} C] {X : C} : Inhabited (MonoOver X)

def CategoryTheory.MonoOver.leTop {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (f : MonoOver X) : f ⟶ ⊤

The morphism to the top object in MonoOver X.

@[simp]

theorem CategoryTheory.MonoOver.top_left {C : Type u₁} [Category.{v₁, u₁} C] (X : C) : ⊤.obj.left = X

@[simp]

theorem CategoryTheory.MonoOver.top_arrow {C : Type u₁} [Category.{v₁, u₁} C] (X : C) : ⊤.arrow = CategoryStruct.id X

def CategoryTheory.MonoOver.mapTop {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [Mono f] : (map f).obj ⊤ ≅ mk f

map f sends ⊤ : MonoOver X to ⟨X, f⟩ : MonoOver Y.

noncomputable def CategoryTheory.MonoOver.pullbackTop {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} [Limits.HasPullbacks C] (f : X ⟶ Y) : (pullback f).obj ⊤ ≅ ⊤

The pullback of the top object in MonoOver Y is (isomorphic to) the top object in MonoOver X.

noncomputable def CategoryTheory.MonoOver.topLEPullbackSelf {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] {A B : C} (f : A ⟶ B) [Mono f] : ⊤ ⟶ (pullback f).obj (mk f)

There is a morphism from ⊤ : MonoOver A to the pullback of a monomorphism along itself; as the category is thin this is an isomorphism.

noncomputable def CategoryTheory.MonoOver.pullbackSelf {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] {A B : C} (f : A ⟶ B) [Mono f] : (pullback f).obj (mk f) ≅ ⊤

The pullback of a monomorphism along itself is isomorphic to the top object.

@[implicit_reducible]

noncomputable instance CategoryTheory.MonoOver.instBot {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasInitial C] [Limits.InitialMonoClass C] {X : C} : Bot (MonoOver X)

@[simp]

theorem CategoryTheory.MonoOver.bot_left {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasInitial C] [Limits.InitialMonoClass C] (X : C) : ⊥.obj.left = ⊥_ C

@[simp]

theorem CategoryTheory.MonoOver.bot_arrow {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasInitial C] [Limits.InitialMonoClass C] {X : C} : ⊥.arrow = Limits.initial.to X

noncomputable def CategoryTheory.MonoOver.botLE {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasInitial C] [Limits.InitialMonoClass C] {X : C} (f : MonoOver X) : ⊥ ⟶ f

The (unique) morphism from ⊥ : MonoOver X to any other f : MonoOver X.

noncomputable def CategoryTheory.MonoOver.mapBot {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} [Limits.HasInitial C] [Limits.InitialMonoClass C] (f : X ⟶ Y) [Mono f] : (map f).obj ⊥ ≅ ⊥

map f sends ⊥ : MonoOver X to ⊥ : MonoOver Y.

noncomputable def CategoryTheory.MonoOver.botCoeIsoZero {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] {B : C} : ⊥.obj.left ≅ 0

The object underlying ⊥ : Subobject B is (up to isomorphism) the zero object.

theorem CategoryTheory.MonoOver.bot_arrow_eq_zero {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [Limits.HasZeroMorphisms C] {B : C} : ⊥.arrow = 0

@[simp]

theorem CategoryTheory.MonoOver.initialTo_b_eq_zero {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [Limits.HasZeroMorphisms C] {B : C} : Limits.initial.to B = 0

simp-normal form of bot_arrow_eq_zero.

noncomputable def CategoryTheory.MonoOver.inf {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] {A : C} : Functor (MonoOver A) (Functor (MonoOver A) (MonoOver A))

When [HasPullbacks C], MonoOver A has "intersections", functorial in both arguments.

As MonoOver A is only a preorder, this doesn't satisfy the axioms of SemilatticeInf, but we reuse all the names from SemilatticeInf because they will be used to construct SemilatticeInf (Subobject A) shortly.

@[simp]

theorem CategoryTheory.MonoOver.inf_map_app {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] {A : C} {X✝ Y✝ : MonoOver A} (k : X✝ ⟶ Y✝) (g : MonoOver A) : (inf.map k).app g = homMk (Limits.pullback.lift (Limits.pullback.fst ((forget A).obj g).hom X✝.arrow) (CategoryStruct.comp (Limits.pullback.snd ((forget A).obj g).hom X✝.arrow) k.hom.left) ⋯) ⋯

@[simp]

theorem CategoryTheory.MonoOver.inf_obj {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] {A : C} (f : MonoOver A) : inf.obj f = (pullback f.arrow).comp (map f.arrow)

noncomputable def CategoryTheory.MonoOver.infLELeft {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] {A : C} (f g : MonoOver A) : (inf.obj f).obj g ⟶ f

A morphism from the "infimum" of two objects in MonoOver A to the first object.

noncomputable def CategoryTheory.MonoOver.infLERight {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] {A : C} (f g : MonoOver A) : (inf.obj f).obj g ⟶ g

A morphism from the "infimum" of two objects in MonoOver A to the second object.

noncomputable def CategoryTheory.MonoOver.leInf {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] {A : C} (f g h : MonoOver A) : (h ⟶ f) → (h ⟶ g) → (h ⟶ (inf.obj f).obj g)

A morphism version of the le_inf axiom.

noncomputable def CategoryTheory.MonoOver.sup {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasImages C] [Limits.HasBinaryCoproducts C] {A : C} : Functor (MonoOver A) (Functor (MonoOver A) (MonoOver A))

When [HasImages C] [HasBinaryCoproducts C], MonoOver A has a sup construction, which is functorial in both arguments, and which on Subobject A will induce a SemilatticeSup.

noncomputable def CategoryTheory.MonoOver.leSupLeft {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasImages C] [Limits.HasBinaryCoproducts C] {A : C} (f g : MonoOver A) : f ⟶ (sup.obj f).obj g

A morphism version of le_sup_left.

noncomputable def CategoryTheory.MonoOver.leSupRight {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasImages C] [Limits.HasBinaryCoproducts C] {A : C} (f g : MonoOver A) : g ⟶ (sup.obj f).obj g

A morphism version of le_sup_right.

noncomputable def CategoryTheory.MonoOver.supLe {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasImages C] [Limits.HasBinaryCoproducts C] {A : C} (f g h : MonoOver A) : (f ⟶ h) → (g ⟶ h) → ((sup.obj f).obj g ⟶ h)

A morphism version of sup_le.

@[implicit_reducible]

instance CategoryTheory.Subobject.orderTop {C : Type u₁} [Category.{v₁, u₁} C] {X : C} : OrderTop (Subobject X)

@[implicit_reducible]

instance CategoryTheory.Subobject.instInhabited {C : Type u₁} [Category.{v₁, u₁} C] {X : C} : Inhabited (Subobject X)

theorem CategoryTheory.Subobject.top_eq_id {C : Type u₁} [Category.{v₁, u₁} C] (B : C) : ⊤ = mk (CategoryStruct.id B)

theorem CategoryTheory.Subobject.underlyingIso_top_hom {C : Type u₁} [Category.{v₁, u₁} C] {B : C} : (underlyingIso (CategoryStruct.id B)).hom = ⊤.arrow

instance CategoryTheory.Subobject.top_arrow_isIso {C : Type u₁} [Category.{v₁, u₁} C] {B : C} : IsIso ⊤.arrow

@[simp]

theorem CategoryTheory.Subobject.underlyingIso_inv_top_arrow {C : Type u₁} [Category.{v₁, u₁} C] {B : C} : CategoryStruct.comp (underlyingIso (CategoryStruct.id B)).inv ⊤.arrow = CategoryStruct.id B

@[simp]

theorem CategoryTheory.Subobject.underlyingIso_inv_top_arrow_assoc {C : Type u₁} [Category.{v₁, u₁} C] {B Z : C} (h : B ⟶ Z) : CategoryStruct.comp (underlyingIso (CategoryStruct.id B)).inv (CategoryStruct.comp ⊤.arrow h) = h

@[simp]

theorem CategoryTheory.Subobject.map_top {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [Mono f] : (map f).obj ⊤ = mk f

theorem CategoryTheory.Subobject.top_factors {C : Type u₁} [Category.{v₁, u₁} C] {A B : C} (f : A ⟶ B) : ⊤.Factors f

theorem CategoryTheory.Subobject.isIso_iff_mk_eq_top {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [Mono f] : IsIso f ↔ mk f = ⊤

theorem CategoryTheory.Subobject.isIso_arrow_iff_eq_top {C : Type u₁} [Category.{v₁, u₁} C] {Y : C} (P : Subobject Y) : IsIso P.arrow ↔ P = ⊤

instance CategoryTheory.Subobject.isIso_top_arrow {C : Type u₁} [Category.{v₁, u₁} C] {Y : C} : IsIso ⊤.arrow

theorem CategoryTheory.Subobject.mk_eq_top_of_isIso {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [IsIso f] : mk f = ⊤

theorem CategoryTheory.Subobject.eq_top_of_isIso_arrow {C : Type u₁} [Category.{v₁, u₁} C] {Y : C} (P : Subobject Y) [IsIso P.arrow] : P = ⊤

theorem CategoryTheory.Subobject.epi_iff_mk_eq_top {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} [Balanced C] (f : X ⟶ Y) [Mono f] : Epi f ↔ mk f = ⊤

theorem CategoryTheory.Subobject.pullback_top {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} [Limits.HasPullbacks C] (f : X ⟶ Y) : (pullback f).obj ⊤ = ⊤

theorem CategoryTheory.Subobject.pullback_self {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] {A B : C} (f : A ⟶ B) [Mono f] : (pullback f).obj (mk f) = ⊤

@[implicit_reducible]

noncomputable instance CategoryTheory.Subobject.orderBot {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasInitial C] [Limits.InitialMonoClass C] {X : C} : OrderBot (Subobject X)

theorem CategoryTheory.Subobject.bot_eq_initial_to {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasInitial C] [Limits.InitialMonoClass C] {B : C} : ⊥ = mk (Limits.initial.to B)

noncomputable def CategoryTheory.Subobject.botCoeIsoInitial {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasInitial C] [Limits.InitialMonoClass C] {B : C} : underlying.obj ⊥ ≅ ⊥_ C

The object underlying ⊥ : Subobject B is (up to isomorphism) the initial object.

theorem CategoryTheory.Subobject.map_bot {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} [Limits.HasInitial C] [Limits.InitialMonoClass C] (f : X ⟶ Y) [Mono f] : (map f).obj ⊥ = ⊥

noncomputable def CategoryTheory.Subobject.botCoeIsoZero {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] {B : C} : underlying.obj ⊥ ≅ 0

The object underlying ⊥ : Subobject B is (up to isomorphism) the zero object.

theorem CategoryTheory.Subobject.bot_eq_zero {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [Limits.HasZeroMorphisms C] {B : C} : ⊥ = mk 0

@[simp]

theorem CategoryTheory.Subobject.bot_arrow {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [Limits.HasZeroMorphisms C] {B : C} : ⊥.arrow = 0

theorem CategoryTheory.Subobject.bot_factors_iff_zero {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [Limits.HasZeroMorphisms C] {A B : C} (f : A ⟶ B) : ⊥.Factors f ↔ f = 0

theorem CategoryTheory.Subobject.mk_eq_bot_iff_zero {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} [Limits.HasZeroObject C] [Limits.HasZeroMorphisms C] {f : X ⟶ Y} [Mono f] : mk f = ⊥ ↔ f = 0

noncomputable def CategoryTheory.Subobject.functor (C : Type u₁) [Category.{v₁, u₁} C] [Limits.HasPullbacks C] : Functor Cᵒᵖ (Type (max u₁ v₁))

Sending X : C to Subobject X is a contravariant functor Cᵒᵖ ⥤ Type.

@[simp]

theorem CategoryTheory.Subobject.functor_obj (C : Type u₁) [Category.{v₁, u₁} C] [Limits.HasPullbacks C] (X : Cᵒᵖ) : (functor C).obj X = Subobject (Opposite.unop X)

@[simp]

theorem CategoryTheory.Subobject.functor_map (C : Type u₁) [Category.{v₁, u₁} C] [Limits.HasPullbacks C] {X✝ Y✝ : Cᵒᵖ} (f : X✝ ⟶ Y✝) (a✝ : Subobject (Opposite.unop X✝)) : (functor C).map f a✝ = (pullback f.unop).obj a✝

noncomputable def CategoryTheory.Subobject.inf {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] {A : C} : Functor (Subobject A) (Functor (Subobject A) (Subobject A))

The functorial infimum on MonoOver A descends to an infimum on Subobject A.

theorem CategoryTheory.Subobject.inf_le_left {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] {A : C} (f g : Subobject A) : (inf.obj f).obj g ≤ f

theorem CategoryTheory.Subobject.inf_le_right {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] {A : C} (f g : Subobject A) : (inf.obj f).obj g ≤ g

theorem CategoryTheory.Subobject.le_inf {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] {A : C} (h f g : Subobject A) : h ≤ f → h ≤ g → h ≤ (inf.obj f).obj g

@[implicit_reducible]

noncomputable instance CategoryTheory.Subobject.semilatticeInf {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] {B : C} : SemilatticeInf (Subobject B)

theorem CategoryTheory.Subobject.inf_comp_left {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] {A : C} (f g : Subobject A) : CategoryStruct.comp ((f ⊓ g).ofLE f ⋯) f.arrow = (f ⊓ g).arrow

theorem CategoryTheory.Subobject.inf_comp_left_assoc {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] {A : C} (f g : Subobject A) {Z : C} (h : A ⟶ Z) : CategoryStruct.comp ((f ⊓ g).ofLE f ⋯) (CategoryStruct.comp f.arrow h) = CategoryStruct.comp (f ⊓ g).arrow h

theorem CategoryTheory.Subobject.inf_comp_right {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] {A : C} (f g : Subobject A) : CategoryStruct.comp ((f ⊓ g).ofLE g ⋯) g.arrow = (f ⊓ g).arrow

theorem CategoryTheory.Subobject.inf_comp_right_assoc {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] {A : C} (f g : Subobject A) {Z : C} (h : A ⟶ Z) : CategoryStruct.comp ((f ⊓ g).ofLE g ⋯) (CategoryStruct.comp g.arrow h) = CategoryStruct.comp (f ⊓ g).arrow h

theorem CategoryTheory.Subobject.factors_left_of_inf_factors {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] {A B : C} {X Y : Subobject B} {f : A ⟶ B} (h : (X ⊓ Y).Factors f) : X.Factors f

theorem CategoryTheory.Subobject.factors_right_of_inf_factors {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] {A B : C} {X Y : Subobject B} {f : A ⟶ B} (h : (X ⊓ Y).Factors f) : Y.Factors f

@[simp]

theorem CategoryTheory.Subobject.inf_factors {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] {A B : C} {X Y : Subobject B} (f : A ⟶ B) : (X ⊓ Y).Factors f ↔ X.Factors f ∧ Y.Factors f

theorem CategoryTheory.Subobject.inf_isPullback {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] {A : C} (f g : Subobject A) : IsPullback ((f ⊓ g).ofLE f ⋯) ((f ⊓ g).ofLE g ⋯) f.arrow g.arrow

theorem CategoryTheory.Subobject.inf_arrow_factors_left {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] {B : C} (X Y : Subobject B) : X.Factors (X ⊓ Y).arrow

theorem CategoryTheory.Subobject.inf_arrow_factors_right {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] {B : C} (X Y : Subobject B) : Y.Factors (X ⊓ Y).arrow

@[simp]

theorem CategoryTheory.Subobject.finset_inf_factors {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] {I : Type u_1} {A B : C} {s : Finset I} {P : I → Subobject B} (f : A ⟶ B) : (s.inf P).Factors f ↔ ∀ i ∈ s, (P i).Factors f

theorem CategoryTheory.Subobject.finset_inf_arrow_factors {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] {I : Type u_1} {B : C} (s : Finset I) (P : I → Subobject B) (i : I) (m : i ∈ s) : (P i).Factors (s.inf P).arrow

theorem CategoryTheory.Subobject.inf_eq_map_pullback' {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] {A : C} (f₁ : MonoOver A) (f₂ : Subobject A) : (inf.obj (Quotient.mk'' f₁)).obj f₂ = (map f₁.arrow).obj ((pullback f₁.arrow).obj f₂)

theorem CategoryTheory.Subobject.inf_eq_map_pullback {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] {A : C} (f₁ f₂ : Subobject A) : f₁ ⊓ f₂ = (map f₁.arrow).obj ((pullback f₁.arrow).obj f₂)

theorem CategoryTheory.Subobject.prod_eq_inf {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] {A : C} {f₁ f₂ : Subobject A} [Limits.HasBinaryProduct f₁ f₂] : (f₁ ⨯ f₂) = f₁ ⊓ f₂

theorem CategoryTheory.Subobject.inf_def {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] {B : C} (m m' : Subobject B) : m ⊓ m' = (inf.obj m).obj m'

theorem CategoryTheory.Subobject.inf_pullback {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] {X Y : C} (g : X ⟶ Y) (f₁ f₂ : Subobject Y) : (pullback g).obj (f₁ ⊓ f₂) = (pullback g).obj f₁ ⊓ (pullback g).obj f₂

⊓ commutes with pullback.

theorem CategoryTheory.Subobject.inf_map {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] {X Y : C} (g : Y ⟶ X) [Mono g] (f₁ f₂ : Subobject Y) : (map g).obj (f₁ ⊓ f₂) = (map g).obj f₁ ⊓ (map g).obj f₂

⊓ commutes with map.

noncomputable def CategoryTheory.Subobject.sup {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasImages C] [Limits.HasBinaryCoproducts C] {A : C} : Functor (Subobject A) (Functor (Subobject A) (Subobject A))

The functorial supremum on MonoOver A descends to a supremum on Subobject A.

@[implicit_reducible]

noncomputable instance CategoryTheory.Subobject.semilatticeSup {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasImages C] [Limits.HasBinaryCoproducts C] {B : C} : SemilatticeSup (Subobject B)

theorem CategoryTheory.Subobject.sup_factors_of_factors_left {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasImages C] [Limits.HasBinaryCoproducts C] {A B : C} {X Y : Subobject B} {f : A ⟶ B} (P : X.Factors f) : (X ⊔ Y).Factors f

theorem CategoryTheory.Subobject.sup_factors_of_factors_right {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasImages C] [Limits.HasBinaryCoproducts C] {A B : C} {X Y : Subobject B} {f : A ⟶ B} (P : Y.Factors f) : (X ⊔ Y).Factors f

theorem CategoryTheory.Subobject.finset_sup_factors {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasImages C] [Limits.HasBinaryCoproducts C] [Limits.HasInitial C] [Limits.InitialMonoClass C] {I : Type u_1} {A B : C} {s : Finset I} {P : I → Subobject B} {f : A ⟶ B} (h : ∃ i ∈ s, (P i).Factors f) : (s.sup P).Factors f

@[implicit_reducible]

noncomputable instance CategoryTheory.Subobject.boundedOrder {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasInitial C] [Limits.InitialMonoClass C] {B : C} : BoundedOrder (Subobject B)

@[implicit_reducible]

noncomputable instance CategoryTheory.Subobject.instLattice {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] [Limits.HasImages C] [Limits.HasBinaryCoproducts C] {B : C} : Lattice (Subobject B)

noncomputable def CategoryTheory.Subobject.wideCospan {C : Type u₁} [Category.{v₁, u₁} C] [LocallySmall.{w, v₁, u₁} C] [WellPowered.{w, v₁, u₁} C] {A : C} (s : Set (Subobject A)) : Functor (Limits.WidePullbackShape ↑(⇑(equivShrink (Subobject A)) '' s)) C

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 WellPowered C to make the diagram small.)

@[simp]

theorem CategoryTheory.Subobject.wideCospan_map_term {C : Type u₁} [Category.{v₁, u₁} C] [LocallySmall.{w, v₁, u₁} C] [WellPowered.{w, v₁, u₁} C] {A : C} (s : Set (Subobject A)) (j : ↑(⇑(equivShrink (Subobject A)) '' s)) : (wideCospan s).map (Limits.WidePullbackShape.Hom.term j) = ((equivShrink (Subobject A)).symm ↑j).arrow

noncomputable def CategoryTheory.Subobject.leInfCone {C : Type u₁} [Category.{v₁, u₁} C] [LocallySmall.{w, v₁, u₁} C] [WellPowered.{w, v₁, u₁} C] {A : C} (s : Set (Subobject A)) (f : Subobject A) (k : ∀ g ∈ s, f ≤ g) : Limits.Cone (wideCospan s)

Auxiliary construction of a cone for le_inf.

@[simp]

theorem CategoryTheory.Subobject.leInfCone_π_app_none {C : Type u₁} [Category.{v₁, u₁} C] [LocallySmall.{w, v₁, u₁} C] [WellPowered.{w, v₁, u₁} C] {A : C} (s : Set (Subobject A)) (f : Subobject A) (k : ∀ g ∈ s, f ≤ g) : (leInfCone s f k).π.app none = f.arrow

noncomputable def CategoryTheory.Subobject.widePullback {C : Type u₁} [Category.{v₁, u₁} C] [LocallySmall.{w, v₁, u₁} C] [WellPowered.{w, v₁, u₁} C] [Limits.HasWidePullbacks C] {A : C} (s : Set (Subobject A)) : C

The limit of wideCospan s. (This will be the supremum of the set of subobjects.)

noncomputable def CategoryTheory.Subobject.widePullbackι {C : Type u₁} [Category.{v₁, u₁} C] [LocallySmall.{w, v₁, u₁} C] [WellPowered.{w, v₁, u₁} C] [Limits.HasWidePullbacks C] {A : C} (s : Set (Subobject A)) : widePullback s ⟶ A

The inclusion map from widePullback s to A

instance CategoryTheory.Subobject.widePullbackι_mono {C : Type u₁} [Category.{v₁, u₁} C] [LocallySmall.{w, v₁, u₁} C] [WellPowered.{w, v₁, u₁} C] [Limits.HasWidePullbacks C] {A : C} (s : Set (Subobject A)) : Mono (widePullbackι s)

noncomputable def CategoryTheory.Subobject.sInf {C : Type u₁} [Category.{v₁, u₁} C] [LocallySmall.{w, v₁, u₁} C] [WellPowered.{w, v₁, u₁} C] [Limits.HasWidePullbacks C] {A : C} (s : Set (Subobject A)) : Subobject A

When [WellPowered C] and [HasWidePullbacks C], Subobject A has arbitrary infimums.

theorem CategoryTheory.Subobject.sInf_le {C : Type u₁} [Category.{v₁, u₁} C] [LocallySmall.{w, v₁, u₁} C] [WellPowered.{w, v₁, u₁} C] [Limits.HasWidePullbacks C] {A : C} (s : Set (Subobject A)) (f : Subobject A) (hf : f ∈ s) : sInf s ≤ f

theorem CategoryTheory.Subobject.le_sInf {C : Type u₁} [Category.{v₁, u₁} C] [LocallySmall.{w, v₁, u₁} C] [WellPowered.{w, v₁, u₁} C] [Limits.HasWidePullbacks C] {A : C} (s : Set (Subobject A)) (f : Subobject A) (k : ∀ g ∈ s, f ≤ g) : f ≤ sInf s

@[implicit_reducible]

noncomputable instance CategoryTheory.Subobject.completeSemilatticeInf {C : Type u₁} [Category.{v₁, u₁} C] [LocallySmall.{w, v₁, u₁} C] [WellPowered.{w, v₁, u₁} C] [Limits.HasWidePullbacks C] {B : C} : CompleteSemilatticeInf (Subobject B)

noncomputable def CategoryTheory.Subobject.smallCoproductDesc {C : Type u₁} [Category.{v₁, u₁} C] [LocallySmall.{w, v₁, u₁} C] [WellPowered.{w, v₁, u₁} C] [Limits.HasCoproducts C] {A : C} (s : Set (Subobject A)) : (∐ fun (j : ↑(⇑(equivShrink (Subobject A)) '' s)) => underlying.obj ((equivShrink (Subobject A)).symm ↑j)) ⟶ A

The universal morphism out of the coproduct of a set of subobjects, after using [WellPowered C] to reindex by a small type.

noncomputable def CategoryTheory.Subobject.sSup {C : Type u₁} [Category.{v₁, u₁} C] [LocallySmall.{w, v₁, u₁} C] [WellPowered.{w, v₁, u₁} C] [Limits.HasCoproducts C] [Limits.HasImages C] {A : C} (s : Set (Subobject A)) : Subobject A

When [WellPowered C] [HasImages C] [HasCoproducts C], Subobject A has arbitrary supremums.

theorem CategoryTheory.Subobject.le_sSup {C : Type u₁} [Category.{v₁, u₁} C] [LocallySmall.{w, v₁, u₁} C] [WellPowered.{w, v₁, u₁} C] [Limits.HasCoproducts C] [Limits.HasImages C] {A : C} (s : Set (Subobject A)) (f : Subobject A) (hf : f ∈ s) : f ≤ sSup s

theorem CategoryTheory.Subobject.symm_apply_mem_iff_mem_image {α : Type u_1} {β : Type u_2} (e : α ≃ β) (s : Set α) (x : β) : e.symm x ∈ s ↔ x ∈ ⇑e '' s

theorem CategoryTheory.Subobject.sSup_le {C : Type u₁} [Category.{v₁, u₁} C] [LocallySmall.{w, v₁, u₁} C] [WellPowered.{w, v₁, u₁} C] [Limits.HasCoproducts C] [Limits.HasImages C] {A : C} (s : Set (Subobject A)) (f : Subobject A) (k : ∀ g ∈ s, g ≤ f) : sSup s ≤ f

@[implicit_reducible]

noncomputable instance CategoryTheory.Subobject.completeSemilatticeSup {C : Type u₁} [Category.{v₁, u₁} C] [LocallySmall.{w, v₁, u₁} C] [WellPowered.{w, v₁, u₁} C] [Limits.HasCoproducts C] [Limits.HasImages C] {B : C} : CompleteSemilatticeSup (Subobject B)

@[implicit_reducible]

noncomputable instance CategoryTheory.Subobject.instCompleteLattice {C : Type u₁} [Category.{v₁, u₁} C] [LocallySmall.{w, v₁, u₁} C] [WellPowered.{w, v₁, u₁} C] [Limits.HasWidePullbacks C] [Limits.HasImages C] [Limits.HasCoproducts C] [Limits.InitialMonoClass C] {B : C} : CompleteLattice (Subobject B)

theorem CategoryTheory.Subobject.subsingleton_of_isInitial {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (hX : Limits.IsInitial X) : Subsingleton (Subobject X)

theorem CategoryTheory.Subobject.subsingleton_of_isZero {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (hX : Limits.IsZero X) : Subsingleton (Subobject X)

theorem CategoryTheory.Subobject.nontrivial_of_not_isZero {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroMorphisms C] [Limits.HasZeroObject C] {X : C} (h : ¬Limits.IsZero X) : Nontrivial (Subobject X)

A nonzero object has nontrivial subobject lattice.

noncomputable def CategoryTheory.Subobject.subobjectOrderIso {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (Y : Subobject X) : Subobject (underlying.obj Y) ≃o ↑(Set.Iic Y)

The subobject lattice of a subobject Y is order isomorphic to the interval Set.Iic Y.