Documentation

Mathlib.CategoryTheory.Subobject.Lattice

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].

The morphism to the top object in MonoOver X.

Equations
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.

Equations
  • One or more equations did not get rendered due to their size.

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

Equations
  • One or more equations did not get rendered due to their size.

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

Equations

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

Equations
  • One or more equations did not get rendered due to their size.

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

Equations

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

Equations
  • One or more equations did not get rendered due to their size.

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.

Equations
  • One or more equations did not get rendered due to their size.
@[simp]

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

Equations

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

Equations
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.

Equations

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.

Equations
  • One or more equations did not get rendered due to their size.

A morphism version of le_sup_left.

Equations
  • One or more equations did not get rendered due to their size.

A morphism version of le_sup_right.

Equations
  • One or more equations did not get rendered due to their size.
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.

Equations
  • One or more equations did not get rendered due to their size.
@[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

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

Equations
  • One or more equations did not get rendered due to their size.
@[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✝

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

Equations
theorem CategoryTheory.Subobject.le_inf {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] {A : C} (h f g : Subobject A) :
h fh gh (inf.obj f).obj g
@[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
@[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 : ISubobject B} (f : A B) :
(s.inf P).Factors f is, (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 : ISubobject 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.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_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.

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 : ISubobject B} {f : A B} (h : is, (P i).Factors f) :
(s.sup P).Factors f

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.)

Equations
  • One or more equations did not get rendered due to their size.

Auxiliary construction of a cone for le_inf.

Equations
  • One or more equations did not get rendered due to their size.

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

Equations
  • One or more equations did not get rendered due to their size.
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

A nonzero object has nontrivial subobject lattice.

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

Equations
  • One or more equations did not get rendered due to their size.