Processing math: 100%
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 definitions 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 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 nforum 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.
    • CommentAuthorTobyBartels
    • CommentTimeJun 8th 2012

    To anybody who can think constructively (Mike at least):

    Given a real number a, and let X be the Kuratowski-finite set {y,z} such that y=z iff a0 (in the strong sense of apartness). Consider the ring of polynomials with real coefficients and variables from the set X. Are the polynomials ay and az equal?

    (The polynomial functions from X to defined by them are certainly equal, but I’m asking about polynomials as formal expressions. For example, the polynomials x and x2 are not equal, even in the ring of one-variable polynomials with coefficients from 𝔽2.)

    • CommentRowNumber2.
    • CommentAuthorMike Shulman
    • CommentTimeJun 8th 2012

    I must be missing something; why are the polynomial functions they define equal?

    • CommentRowNumber3.
    • CommentAuthorIngoBlechschmidt
    • CommentTimeJun 9th 2012
    • (edited Jun 9th 2012)

    I believe the following argument shows that the polynomial functions are equal:

    Let φX, we want to show aφ(y)=aφ(z). For any n1, we have a0 or |a|1n. In both cases the inequality |aφ(y)aφ(z)|1n|φ(y)φ(z)| follows. As |φ(y)φ(z)| is fixed, this shows that indeed |aφ(y)aφ(z)|=0.

    I don’t have an answer to the original question.

    • CommentRowNumber4.
    • CommentAuthorMike Shulman
    • CommentTimeJun 9th 2012

    Nice argument! I’m afraid I don’t have an answer to the original question either, though. I don’t see any reason why they should be equal, but I don’t immediately see how to build a counterexample either.

    • CommentRowNumber5.
    • CommentAuthorjcmckeown
    • CommentTimeJun 10th 2012

    I shouldn't be distracting myself with this, but what does "=" mean, here? Or is that part of the question, too?

    • CommentRowNumber6.
    • CommentAuthorMike Shulman
    • CommentTimeJun 10th 2012

    Well, the real numbers are a set, as are Toby’s set X and the polynomial ring, so = means equality in those sets. Are you asking about how those sets are defined? The set X, for instance, is defined as the quotient of the two-element set {y,z} by the equivalence relation which sets yz iff a0 (and of course yy and zz unconditionally).

    • CommentRowNumber7.
    • CommentAuthorTobyBartels
    • CommentTimeJun 10th 2012

    JC is right to ask; the question is what equality in [X] should be. Of course, [X] is the free commutative -algebra on the set X, but what’s an -algebra? If this is simply a set equipped with some operations and commutative diagrams (including one unary scalar multiplication operation for each real number), then ay=az in [X] iff a=0 or a0 (so if ay=az for every a, then the lesser limited principle of omniscience holds). However, if an -algebra is equipped with a tight apartness that all operations respect and a binary scalar multiplication operation ×BB that also respects it and the usual apartness on (in the sense of being strongly extensional), then ay=az necessarily. So that answers my question, I guess.

    • CommentRowNumber8.
    • CommentAuthorMike Shulman
    • CommentTimeJun 11th 2012

    Hmm, I was about to say that I thought Ingo’s argument would work for polynomials too. Namely, define the norm of a polynomial to be the supremum of the absolute values of its coefficients. Then since either |a|<1n or a0, in both cases ayaz<2n, and this holds for all n, so ayaz=0 and thus ay=az. What definition of [X] is that using?

    • CommentRowNumber9.
    • CommentAuthorTobyBartels
    • CommentTimeJun 11th 2012
    • (edited Jun 11th 2012)

    How do you know that this supremum exists? (It always exists as a lower real number, but the comparison law is invalid for those, so we must prove that the supremum is located.) In particular, the norm of ayaz is 0 if y=z, but this norm is a if yz.

    With the second definition of [X] (with apartness), I we can prove that ayaz must have a located norm (although we can’t prove this for an arbitrary polynomial in [X]), so the argument will still go through; but not with the first definition.

    • CommentRowNumber10.
    • CommentAuthorMike Shulman
    • CommentTimeJun 11th 2012

    Ah, right. (You can probably tell that I don’t work with constructive real numbers much.)