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

Equations
  • CategoryTheory.MonoOver.instInhabited = { default := }

The morphism to the top object in MonoOver X.

Equations
Instances For
    @[simp]

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

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

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

        Equations
        Instances For

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

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

            Equations
            Instances For

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

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

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

                Equations
                • CategoryTheory.MonoOver.botCoeIsoZero = CategoryTheory.Limits.initialIsInitial.uniqueUpToIso CategoryTheory.Limits.HasZeroObject.zeroIsInitial
                Instances For

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

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

                    Equations
                    Instances For

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

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

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

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

                            A morphism version of le_sup_left.

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

                              A morphism version of le_sup_right.

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

                                A morphism version of sup_le.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  Equations
                                  Equations
                                  • CategoryTheory.Subobject.instInhabited = { default := }
                                  theorem CategoryTheory.Subobject.top_factors {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : C} {B : C} (f : A B) :
                                  .Factors f

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

                                  Equations
                                  Instances For

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

                                    Equations
                                    • CategoryTheory.Subobject.botCoeIsoZero = CategoryTheory.Subobject.botCoeIsoInitial ≪≫ CategoryTheory.Limits.initialIsInitial.uniqueUpToIso CategoryTheory.Limits.HasZeroObject.zeroIsInitial
                                    Instances For

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

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

                                        Equations
                                        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
                                          @[simp]
                                          theorem CategoryTheory.Subobject.inf_factors {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasPullbacks C] {A : C} {B : C} {X : CategoryTheory.Subobject B} {Y : CategoryTheory.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₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasPullbacks C] {I : Type u_1} {A : C} {B : C} {s : Finset I} {P : ICategoryTheory.Subobject B} (f : A B) :
                                          (s.inf P).Factors f is, (P i).Factors f
                                          theorem CategoryTheory.Subobject.finset_inf_arrow_factors {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasPullbacks C] {I : Type u_1} {B : C} (s : Finset I) (P : ICategoryTheory.Subobject B) (i : I) (m : i s) :
                                          (P i).Factors (s.inf P).arrow

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

                                          Equations
                                          Instances For
                                            Equations
                                            • CategoryTheory.Subobject.boundedOrder = let __src := CategoryTheory.Subobject.orderTop; let __src_1 := CategoryTheory.Subobject.orderBot; BoundedOrder.mk
                                            Equations
                                            • CategoryTheory.Subobject.instLattice = let __src := CategoryTheory.Subobject.semilatticeInf; let __src_1 := CategoryTheory.Subobject.semilatticeSup; Lattice.mk

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

                                              Auxiliary construction of a cone for le_inf.

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

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

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