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 comma 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 finite 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 k-theory lie-theory limits linear linear-algebra locale localization logic mathematics 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.
    • CommentAuthorstevevickers
    • CommentTimeNov 29th 2018
    The page finite set list various notions of finiteness, but one seems to be missing: sets that are Kuratowski finite with decidable equality. On the face of it that is the same as Bishop finiteness (isomorphic with some [n]), by taking an enumeration of the elements and using decidability of equality to omit duplicates.

    However, existence of that enumeration is weaker than choosing one. The distinction can be seen in sheaves over the circle S^1. The twisted double cover is, locally, Kuratowski finite with decidable equality. It even has a well-defined cardinality of 2. Locally, but not globally, it is isomorphic to [2].

    To force global Bishop finiteness, or a theory of finite sets that is equivalent to that of natural numbers, you need the extra structure of a decidable total order.

    To put it another way, the notion of Bishop finiteness splits into local (weaker) and global versions.

    Does anyone have any views on what would be a widely acceptable terminology for this? In my paper "[Strongly algebraic = SFP (topically)](http://www.cs.bham.ac.uk/~sjv/papersfull.php#SFP)" I referred to the stronger version as "strongly finite" or "finite cardinal"".
    • CommentRowNumber2.
    • CommentAuthorUlrik
    • CommentTimeNov 29th 2018

    I’m not sure I understand. I think the “exists” on the page is meant to represent mere existence (truncated sigma in HoTT). Your example falls under this definition.

    • CommentRowNumber3.
    • CommentAuthorMike Shulman
    • CommentTimeNov 29th 2018
    • (edited Nov 29th 2018)

    I think Steve is right. Check out finite object for a discussion of this local vs global distinction.

    If “finite” is to be a mere property of a set, then the “global” notions cannot be defined inside the “usual” higher-order internal logic of a topos, which is why the page finite set only discusses the notions that internalize to the “local” ones. Steve is saying we can however define them if we regard finiteness as a structure. Equivalently, we can define them in the internal dependent type theory of the topos, as non-truncated “properties” using a Σ\Sigma instead of an \exists. If we want a consistent way to refer to the latter notions, I suppose “strongly” isn’t too bad, although a more descriptive word might be something like “algebraically”.

    By the way, Steve, if you want to make [links](like this) you need to select the “Markdown+Itex” radio button below the text box when you post (which should be the default).

    • CommentRowNumber4.
    • CommentAuthorUlrik
    • CommentTimeNov 29th 2018
    • (edited Nov 29th 2018)

    Oh I see. But there’s still some further distinction, then, between finite sets of the form Fin(n)Fin(n) for some element n:Natn:Nat, and those of the form Fin(n)Fin(n) for an external natural number nn. (These differ over disconnected bases.)

    So maybe we can say strongly finite and externally finite, respectively?

    Edit to add: Instead of strongly finite set we could also just say totally ordered finite set. That seems to be unambiguous.

    • CommentRowNumber5.
    • CommentAuthorMike Shulman
    • CommentTimeNov 29th 2018

    Yes, that’s true.

    I don’t like “totally ordered” because I wouldn’t want to consider the ordering part of the structure. That is, an isomorphism between strongly finite sets shouldn’t have to respect the orderings.

    • CommentRowNumber6.
    • CommentAuthorUlrik
    • CommentTimeNov 30th 2018

    Now I’m confused again: If you want the identity type of StronglyFiniteSet to correspond to isomorphism, then you’re back to the usual (Bishop / decidable K) FinSet, right? (Form the pregroupoid of strongly finite sets and isomorphisms and Rezk/stack complete.)

    I thought the point was that StronglyFiniteSet should be equivalent to (internal) Nat. But maybe the point is really that you’re interested in the pregroupoid (or precategory) structure on Nat/StronglyFiniteSet?

    • CommentRowNumber7.
    • CommentAuthorstevevickers
    • CommentTimeDec 1st 2018

    It’s true that if “strongly finite” has the total order as part of the structure, then the corresponding homomorphisms have to preserve it. However, that doesn’t stop you considering other morphisms and in fact that’s exactly what you do when constructing the classifying toposes for various theories. There are five examples in which each is classified by a presheaf topos [C,Set][C, Set] where CC has strongly finite sets as objects, but varied morphisms. More economically, we can take the objects to be natural numbers. Then CC can be constructed internally in any elementary topos with nno (or arithmetic universe, for that matter).

    1. Sets CC has, for morphisms, arbitrary functions between the corresponding finite cardinals.

    2. Sets with decidable equality. The corresponding structure, which must be preserved by homomorphisms, is the inequality relation. Hence homomorphisms are injective. The morphisms of CC are injective functions between the finite cardinals.

    3. Kuratowski finite sets. The structure is the finite subset (element of the free semilattice) that contains all the elements, and homomorphisms preserve this and so are surjective. The morphisms of CC are surjective functions between the finite cardinals.

    4. Kuratowski finite sets with decidable equality Homomorphisms are isomorphisms The morphisms of CC are isomorphisms between the finite cardinals, so CC is a groupoid.

    5. Kuratowski finite sets with decidable equality and decidable total order. Homomorphisms are order preserving isos - so there’s at most one. The morphisms of CC are identity functions between the finite cardinals, so CC is just the discrete category on N.

    A similar principle applies to theories of algebras, where the classifying topos is that of covariant functors to SetSet from the category of finitely presented algebras. Again, “finitely” is interpreted in the strong way, so that we have the category of strongly finite presentations.