Not signed in (Sign In)

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Site Tag Cloud

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory internal-categories k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorAlec Rhea
    • CommentTimeMar 2nd 2021

    Test edit, I can’t seem to get the page to accept the larger edit I’ve made.

    diff, v26, current

    • CommentRowNumber2.
    • CommentAuthorAlec Rhea
    • CommentTimeMar 2nd 2021

    Added discussion of skeletons as an endo-2-functor on the 2-category of categories, skeletons of indexed categories and skeletons of fibrations. There is probably a more general discussion to be had at the \infty-level, but I’m not sure what \infty-skeleta look like at the moment.

    diff, v26, current

    • CommentRowNumber3.
    • CommentAuthorHurkyl
    • CommentTimeMar 2nd 2021
    • (edited Mar 2nd 2021)

    In the case of quasi-categories, I imagine Lurie’s “minimal inner fibrations” (Higher Topos Theory, 2.3.3) would be the right notion of ∞-skeleton to consider.

    I guess then the right thing for simplicial categories is to combine the evident condition on objects with requiring the hom-spaces be minimal Kan fibrations.

  1. Apologies that you had to battle the spam filter Alec, it is suspicious of large edits (but becomes less suspicious the more of an editing history one has, until it eventually allow one free reign :-)).

    • CommentRowNumber5.
    • CommentAuthorAlec Rhea
    • CommentTimeMar 3rd 2021

    Slightly changed definition section to explicitly name skeletons vs weak skeletons, and added a simple theorem about the stronger sense of skeletons without without choice.

    The changes to the definition section might be controversial, as I named the weaker version a ’weak skeleton’ and defined a skeleton to be the classical notion. If there is more standard terminology it should be put in this section.

    diff, v29, current

    • CommentRowNumber6.
    • CommentAuthorAlec Rhea
    • CommentTimeMar 7th 2021

    Added coherence isomorphisms for skeleton endo-pseudofunctor.

    diff, v30, current

    • CommentRowNumber7.
    • CommentAuthorUrs
    • CommentTimeJul 22nd 2022
    • (edited Jul 22nd 2022)

    have added an Examples-section “Posets as skeleta of prosets” (here). So far it is just a glorified pointer to the new entry relation between preorders and (0,1)-categories.

    diff, v31, current

  2. strict univalent categories are skeletal but do not violate the principle of equivalence.

    Anonymous

    diff, v32, current

  3. adding more examples of skeletal categories

    Anonymous

    diff, v32, current

    • CommentRowNumber10.
    • CommentAuthorHurkyl
    • CommentTimeSep 1st 2022
    • (edited Sep 1st 2022)

    It’s not enough for the core to be a setoid: a univalent category is skeletal iff its core is a set.

    Furthermore, skeletal categories need not be univalent.

    I think the phrase “violate the principle of equivalence” is being used in a very strange way. How can a category violate it? AFAICT, the relevant fact in this spirit is that Ob:CatSetOb : Cat \to Set does not preserve equivalences.

    • CommentRowNumber11.
    • CommentAuthorGuest
    • CommentTimeSep 1st 2022

    Hurkyl, it is enough for the core of a univalent category to be a setoid, because the Rezk completion condition of a univalent category makes every setoid into a set.

    • CommentRowNumber12.
    • CommentAuthorGuest
    • CommentTimeSep 1st 2022

    A strict category CC is skeletal if for all objects A:Ob(C)A:Ob(C) and B:Ob(C)B:Ob(C) there is a function truncIsoToId(A,B):|AB|A=B\mathrm{truncIsoToId}(A, B):\vert A \cong B \vert \to A = B from the propositional truncation of the set of isomorphisms |AB|\vert A \cong B \vert to the identity type A=BA = B. (I don’t see how this violates the principle of equivalence btw, skeletal strict categories are perfectly definable in homotopy type theory)

    A strict category CC is univalent if the canonical function IdToIso(A,B):A=BAB\mathrm{IdToIso}(A, B):A = B \to A \cong B is an equivalence. The homotopy inverse of IdToIso(A,B)\mathrm{IdToIso}(A, B) is called IsoToId(A,B)\mathrm{IsoToId}(A, B). But since A=BA = B is a proposition for all objects AA and BB in a strict category, ABA \cong B is a proposition as well if the strict category is univalent, and thus ABA \cong B is equivalent to its propositional truncation |AB|\vert A \cong B \vert. And so the Rezk completion condition on a strict univalent category is what makes a strict univalent category skeletal.

    • CommentRowNumber13.
    • CommentAuthorMike Shulman
    • CommentTimeSep 1st 2022

    I agree that it doesn’t make sense to talk about a particular category violating the POE. What violates the POE is the notion of skeletal category.

    diff, v34, current

    • CommentRowNumber14.
    • CommentAuthorMike Shulman
    • CommentTimeSep 1st 2022

    Most of the “Definition” section belonged in a different section like “Constructions”.

    diff, v34, current

    • CommentRowNumber15.
    • CommentAuthorMike Shulman
    • CommentTimeSep 1st 2022

    Clarified that the existing sections pertain to set-level foundations, and added a new section on skeleta in intensional/homotopy type theory.

    diff, v34, current

    • CommentRowNumber16.
    • CommentAuthorGuest
    • CommentTimeSep 5th 2022

    There are two query boxes on this page.

    • CommentRowNumber17.
    • CommentAuthoranuyts
    • CommentTimeNov 29th 2022

    Point out that skeletal categories can have non-trivial automorphisms.

    diff, v35, current

    • CommentRowNumber18.
    • CommentAuthorUrs
    • CommentTimeNov 29th 2022

    It seems to me that this addendum should be superfluous unless the previous sentence was really unclear. So I took the liberty of instead adjusting the lead-in sentence a little, and then appending a sentence pointing to gaunt categories. Also added the qualification that we are talking about strict categories.

    (all here)

    diff, v36, current

    • CommentRowNumber19.
    • CommentAuthorUrs
    • CommentTimeMay 12th 2023

    added a sentence on and a pointer to the special case of skeletal groupoids (a page that had been missing, even as a redirect, but which I am creating now).

    diff, v37, current

    • CommentRowNumber20.
    • CommentAuthorUrs
    • CommentTimeJun 5th 2023
    • (edited Jun 5th 2023)

    added pointer to:

    diff, v39, current

    • CommentRowNumber21.
    • CommentAuthorUrs
    • CommentTimeJun 5th 2023

    added pointer to:

    diff, v39, current

    • CommentRowNumber22.
    • CommentAuthorUrs
    • CommentTimeJun 5th 2023
    • (edited Jun 5th 2023)

    added pointer to:

    diff, v39, current

  4. Added the category of Archimedean ordered fields and monotonic field homomorphisms to the list of examples - impredicatively this is just the subset of the power set of the real numbers consisting of the Archimedean ordered subfields of the real numbers.

    Peter Wells

    diff, v40, current

    • CommentRowNumber24.
    • CommentAuthorUrs
    • CommentTimeFeb 1st 2024

    moving this old query-box out of the entry, which seems to have resolved itself:


    +– {: .query} I removed ’non-ana’, since I don't think that ’strongly equivalent’ would ever be used in an ’ana-’ sense. —Toby

    Addendum: Actually, I don't know why I asked whether you meant weakly or strongly here, since obviously one can prove that two ana-equivalent categories are weakly equivalent! It seems that the discussion above used the terms ’equivalence’ and ’ana-equivalence’ where equivalence of categories uses ’strong equivalence’ and ’weak equivalence’ or ’ana-equivalence’; so I just changed it. And then I added another entry, which maybe you should remove if Freyd & Scedrov don't actually address it. On the other hand, if they really talk about weak equivalence instead of ana-equivalence (although if they define it in elementary terms, it's hard to tell the difference), maybe there's no need to say ’ana-’ at all on this page.

    =–


    diff, v41, current