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.

Instances For
    @[simp]

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

    Instances For

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

      Instances For

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

        Instances For

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

          Instances For

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

            Instances For

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

              Instances For

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

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

                  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.

                  Instances For

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

                    Instances For

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

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

                        A morphism version of the le_inf axiom.

                        Instances For

                          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.

                          Instances For

                            A morphism version of sup_le.

                            Instances For

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

                              Instances For

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

                                Instances For

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

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

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

                                    Instances For

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

                                      Instances For

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

                                        Instances For

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

                                          Instances For

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

                                            Instances For
                                              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

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

                                              Instances For