claimroutineinferred_dep

Subset products of radicands are non-squares

Claim·§8.4 A separate odd valuation for each radicand·inside lemPrivate odd valuation for each radicand

Statement (paper)

For every nonempty subset I⊆{1,…,j}I\subseteq\{1,\ldots,j\}, the product ∏ℓ∈IDℓ\prod_{\ell\in I}D_\ell has valuation vℓ(∏m∈IDm)=1v_\ell\left(\prod_{m\in I}D_m\right)=1 at every ℓ∈I\ell\in I, and therefore ∏ℓ∈IDℓ\prod_{\ell\in I}D_\ell is not a square in M×M^\times.

In plain English

For every nonempty I⊆{1,…,j}I\subseteq\{1,\ldots,j\}, the product ∏m∈IDm\prod_{m\in I}D_m has valuation exactly 1 under vℓv_\ell for each ℓ∈I\ell\in I, so it is not a square in M×M^\times.

Why it's here

Each vℓv_\ell sees only the factor DℓD_\ell (valuation 1) and treats the other DmD_m as units (valuation 0), so the valuations add up to 1 on the product. A square has even valuation under every integer-valued valuation, so the product cannot be a square. Since this holds for every nonempty subset, it gives independence of the classes of D1,…,DjD_1,\ldots,D_j modulo squares, which is the parent lemma's conclusion.
Classified routine:
Direct consequence of the earlier claims giving each radicand a private valuation: additivity of valuations gives valuation 1 on the product, and squares have even valuation. This is the standard criterion for independence of square classes (Kummer theory).

Uses

claimPlane case: order along irreducible Q_ellclaimPower-series valuation of order oneclaimPrivate valuation in the line caseclaimFractional-linear case gives private simple zero

Used by

Nothing in the paper

Sources

PaperOpen
Section
§8.4 A separate odd valuation for each radicand
Page
—
Label
—
Line
sections/07-algebra.tex:587
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Odd valuations give square-class independence" rests on claim-alg-private-valuations-1
  • info
    inferred_dep
    outline: "Odd valuations give square-class independence" rests on claim-alg-private-valuations-4
  • info
    inferred_dep
    outline: "Odd valuations give square-class independence" rests on claim-alg-private-valuations-6
  • info
    inferred_dep
    outline: "Odd valuations give square-class independence" rests on claim-alg-private-valuations-7