Quadratic forms and cohomological invariants

The declarations the status of Tau Ceti's roadmap names, and the other results named in the modules where only this status names declarations, or in folders below the areas where only it names 2 or more, as Tau Ceti has them at commit ace60277.

TheoremThe splitting criterion for quaternion algebras #

The splitting criterion for quaternion algebras (Lam III.2.7 and III.4.2, Serre III.1, Gille-Szamuely 1.1.9). For units a and b of a field in which 2 is invertible, the following are equivalent: 1. ℍ[K,a,b] is isomorphic to M₂(K); 2. b is a norm from K[√a] = QuadraticAlgebra K a 0; 3. b = x² - a y² for some x, y ∈ K; 4. the ternary form ⟨1, -a, -b⟩ is isotropic; 5. the norm form of ℍ[K,a,b], that is ⟨1, -a, -b, ab⟩, is isotropic.

TauCeti.QuaternionAlgebra.nonempty_algEquiv_matrix_tfae.{u_1} {K : Type u_1} [Field K]
  [Invertible 2] (a b : Kˣ) :
  [Nonempty (QuaternionAlgebra K (↑a) 0 ↑b ≃ₐ[K] Matrix (Fin 2) (Fin 2) K),
      ∃ z, QuadraticAlgebra.norm z = ↑b, ∃ x y, ↑b = x ^ 2 - ↑a * y ^ 2,
      ¬(QuadraticMap.weightedSumSquares K ![1, -↑a, -↑b]).Anisotropic,
      ¬QuadraticMap.Anisotropic (QuaternionAlgebra.normForm (↑a) 0 ↑b)].TFAE

Lean

Formalized in Tau Ceti as TauCeti.QuaternionAlgebra.nonempty_algEquiv_matrix_tfae.

Sources

LeanTauCeti.QuaternionAlgebra.nonempty_algEquiv_matrix_tfae

Used by 20

Used byThe cup-norm theorem · Quadratic reciprocity is Hilbert reciprocity for two odd primes · Serre's mass formula for the quadratic extensions of ℚ_2 · The totally ramified quadratic extensions of ℚ_2 · Hilbert sign prescription (O'Meara 71:19a) · Local equivalence by invariants · O'Meara 72:1 up to one global representation · The Hasse product formula · The kernel of the idele Hilbert character · The system of local invariants of a regular quadratic form Q over a number field · Serre's formula for the Artin conductor · A Kummer cup over a local field is its Hilbert symbol times a fixed nonzero cup · Lam's comparison of the Clifford and Hasse invariants (Lam V.3.20) · Local classification (O'Meara 63:20, Serre IV Thm 7) · The classification of regular forms over a local field, as an equivalence · The Evens norm of a Kummer class over a local field, as an element of H²(G_K, 𝔽₂) · The Hilbert symbol as a bilinear form over 𝔽₂ · The relative Stiefel–Whitney formula in degree two, on the trace forms themselves (Kahn, Théorème 2 in degree two) · The relative Stiefel–Whitney formula over a local field · The Gram formula for the Kummer cup over ℚ₂

DefinitionThe classification of regular forms over a local field, as an equivalence #

Taking rank, discriminant and local Hasse invariant is a bijection from regular-form classes over a nonarchimedean local field onto admissible triples. Its inverse is the realization map.

TauCeti.RegularFormClass.localInvariantsEquiv.{u_1} {K : Type u_1} [Field K] [ValuativeRel K]
  [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Invertible 2] :
  TauCeti.RegularFormClass K ≃ { I // I.IsAdmissible }

Lean

Formalized in Tau Ceti as TauCeti.RegularFormClass.localInvariantsEquiv.

Sources

LeanTauCeti.RegularFormClass.localInvariantsEquiv

Uses 4

Proof usesLocal classification (O'Meara 63:20, Serre IV Thm 7) · The splitting criterion for quaternion algebras · TauCeti.algebraicExtensionNormedField · Witt's chain theorem in its nontrivial range

TheoremHilbert's product formula #

For a, b ∈ Kˣ in a number field K, the product of the norm-equation Hilbert symbols (a_v, b_v)_v over the finite places and of the real Hilbert symbols (a_w, b_w)_w over the real places of K is 1.

TauCeti.hilbertSymbol_productFormula.{u_1} {K : Type u_1} [Field K] [NumberField K] (a b : Kˣ) :
  (∏ᶠ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)),
        TauCeti.hilbertSymbol (v.unitAtFinitePlace a) (v.unitAtFinitePlace b)) *
      ∏ w, TauCeti.hilbertSymbol ((TauCeti.unitAtRealPlace w) a) ((TauCeti.unitAtRealPlace w) b) =
    1

Lean

Formalized in Tau Ceti as TauCeti.hilbertSymbol_productFormula.

Other forms

Hilbert's product formula over ℚ. Formalized in Tau Ceti as TauCeti.finprod_hilbertSymbol_padic_mul_hilbertSymbol_real_eq_one.

TauCeti.finprod_hilbertSymbol_padic_mul_hilbertSymbol_real_eq_one (a b : ℚˣ) :
  (∏ᶠ (ℓ : Nat.Primes),
        TauCeti.hilbertSymbol ((Units.map ↑(algebraMap ℚ ℚ_[↑ℓ])) a)
          ((Units.map ↑(algebraMap ℚ ℚ_[↑ℓ])) b)) *
      TauCeti.hilbertSymbol ((Units.map ↑(algebraMap ℚ ℝ)) a) ((Units.map ↑(algebraMap ℚ ℝ)) b) =
    1

Sources

LeanTauCeti.hilbertSymbol_productFormula · TauCeti.finprod_hilbertSymbol_padic_mul_hilbertSymbol_real_eq_one

Uses 9 · Used by 2

Proof usesThe cup-norm theorem · Dedekind's different theorem, the tame case · Euler's theorem on an n-th root of unity · The first half of Dedekind's different theorem · Hensel's lemma for the norm · Hilbert reciprocity · The Kummer isomorphism · The local invariant · TauCeti.algebraicExtensionNormedField

Used byThe Hasse product formula · The kernel of the idele Hilbert character

DefinitionThe comparison isomorphism #

The comparison isomorphism Br(K) ≃ H²_cont(G_K, (Kˢ)ˣ) with Mathlib's continuous cohomology, for K in any universe: the explicit comparison brauerExplicitH2Equiv K followed by explicitH2AddEquivContinuousCohomology. It is characterized by brauerCohomologyEquiv_crossedProductClass: the class of the crossed product of a cocycle of a finite Galois L ⊆ Kˢ goes to the continuous class of the inflation of that cocycle; see brauerCohomologyEquiv_unique.

TauCeti.brauerCohomologyEquiv.{u} (K : Type u) [Field K] :
  Additive (BrauerGroup K) ≃+
    ↑(continuousCohomology 2
          (TauCeti.ofDiscreteModule ℤ (TauCeti.AbsoluteGaloisGroup K)
            (TauCeti.UnitsCoeff K))).toModuleCat

Lean

Formalized in Tau Ceti as TauCeti.brauerCohomologyEquiv.

Sources

LeanTauCeti.brauerCohomologyEquiv

Uses 3 · Used by 6

Proof usesArtin--Wedderburn over a separably closed field · The Skolem-Noether theorem · Wedderburn-Artin for central simple algebras

Used byThe cup-norm theorem · A Kummer cup over a local field is its Hilbert symbol times a fixed nonzero cup · TauCeti.brauer2EquivH2_baseChange · The Evens norm of a Kummer class over a local field, as an element of H²(G_K, 𝔽₂) · The relative Stiefel–Whitney formula in degree two, on the trace forms themselves (Kahn, Théorème 2 in degree two) · The relative Stiefel–Whitney formula over a local field

TheoremTauCeti.brauer2EquivH2_baseChange #

Scalar extension of any two-torsion Brauer class corresponds under ι to restriction of its mod-two Galois cohomology class.

TauCeti.brauer2EquivH2_baseChange.{u} {K L : Type u} [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] (σ : L →ₐ[K] SeparableClosure K) [Invertible 2] [Invertible 2]
  (x : ↥(TauCeti.BrauerGroup.twoTorsion K)) :
  (TauCeti.brauer2EquivH2 L) (Additive.ofMul ((TauCeti.BrauerGroup.twoTorsionBaseChange K L) x)) =
    (CategoryTheory.ConcreteCategory.hom (TauCeti.galoisRes K L σ 2))
      ((TauCeti.brauer2EquivH2 K) (Additive.ofMul x))

Lean

Formalized in Tau Ceti as TauCeti.brauer2EquivH2_baseChange.

Sources

LeanTauCeti.brauer2EquivH2_baseChange

Uses 5

Statement usesThe comparison isomorphism

Proof usesArtin--Wedderburn over a separably closed field · The dimension count behind the centralizer theorem, asking only for what it uses · The Skolem-Noether theorem · Wedderburn-Artin for central simple algebras

TheoremThe relative Stiefel–Whitney formula in degree two, on the trace forms themselves (Kahn, Théorème 2 in degree two)#

for a quadratic extension L/K, which is separable as 2 is invertible, and a ∈ Lˣ with Kummer class (a) ∈ H¹(G_L, 𝔽₂),

w₂(Tr_*⟨a⟩) = w₂(Tr_*⟨1⟩) + N^{Ev}((a)) + w₁(Tr_*⟨1⟩) ∪ cor (a),

where the Evens norm N^{Ev} and the corestriction cor are taken along any K-embedding σ of L into a separable closure of K. The two sides are the classes of the regular forms y ↦ Tr_{L/K}(a y²) and y ↦ Tr_{L/K}(y²) on L; their regularity is a hypothesis.

TauCeti.sw2Class_formClass_traceTransfer_smul_sq.{u} {K L : Type u} [Field K] [Invertible 2]
  [Field L] [Algebra K L] [FiniteDimensional K L] [Invertible 2] (σ : L →ₐ[K] SeparableClosure K)
  (hfin : Module.finrank K L = 2) (a : Lˣ) (ha : QuadraticMap.Nondegenerate)
  (h1 : QuadraticMap.Nondegenerate) :
  TauCeti.sw2Class (TauCeti.formClass (QuadraticMap.traceTransfer K (↑a • QuadraticMap.sq)) ha) =
    TauCeti.sw2Class (TauCeti.formClass (QuadraticMap.traceTransfer K QuadraticMap.sq) h1) +
        TauCeti.galoisEvens K L σ hfin (TauCeti.kummerClass a) +
      (((TauCeti.trivialF2TopPairing (TauCeti.AbsoluteGaloisGroup K)).cup 1 1)
          (TauCeti.sw1Class (TauCeti.formClass (QuadraticMap.traceTransfer K QuadraticMap.sq) h1)))
        ((CategoryTheory.ConcreteCategory.hom (TauCeti.galoisCor K L σ 1)) (TauCeti.kummerClass a))

Lean

Formalized in Tau Ceti as TauCeti.sw2Class_formClass_traceTransfer_smul_sq.

Other forms

The relative Stiefel–Whitney formula in degree one. Formalized in Tau Ceti as TauCeti.sw1Class_traceTransfer_mk_rankOne.

TauCeti.sw1Class_traceTransfer_mk_rankOne.{u} {K L : Type u} [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [Invertible 2] [Invertible 2] (σ : L →ₐ[K] SeparableClosure K)
  [Algebra.IsSeparable K L] (a : Lˣ) :
  TauCeti.sw1Class ((TauCeti.RegularFormClass.traceTransfer K) ⟦⟨1, fun x => a⟩⟧) =
    TauCeti.sw1Class ((TauCeti.RegularFormClass.traceTransfer K) 1) +
      (CategoryTheory.ConcreteCategory.hom (TauCeti.galoisCor K L σ 1)) (TauCeti.kummerClass a)

The relative Stiefel–Whitney formula in degree one, on diagonal presentations. Formalized in Tau Ceti as TauCeti.sw1_eq_add_galoisCor_of_equivalent_scharlauTransfer.

TauCeti.sw1_eq_add_galoisCor_of_equivalent_scharlauTransfer.{u} {K L : Type u} [Field K] [Field L]
  [Algebra K L] [FiniteDimensional K L] [Invertible 2] [Invertible 2]
  (σ : L →ₐ[K] SeparableClosure K) (s : L →ₗ[K] K) (a : Lˣ) {m n : ℕ} {t : Fin m → Kˣ}
  {b : Fin n → Kˣ}
  (ht :
    QuadraticMap.Equivalent (QuadraticMap.sq.scharlauTransfer s)
      (QuadraticMap.weightedSumSquares K fun i => ↑(t i)))
  (hb :
    QuadraticMap.Equivalent ((↑a • QuadraticMap.sq).scharlauTransfer s)
      (QuadraticMap.weightedSumSquares K fun i => ↑(b i))) :
  TauCeti.sw1 b =
    TauCeti.sw1 t +
      (CategoryTheory.ConcreteCategory.hom (TauCeti.galoisCor K L σ 1)) (TauCeti.kummerClass a)

The relative Stiefel–Whitney formula in degree one, on diagonal presentations of the trace forms. Formalized in Tau Ceti as TauCeti.sw1_eq_add_galoisCor_of_equivalent_traceTransfer.

TauCeti.sw1_eq_add_galoisCor_of_equivalent_traceTransfer.{u} {K L : Type u} [Field K] [Field L]
  [Algebra K L] [FiniteDimensional K L] [Invertible 2] [Invertible 2]
  (σ : L →ₐ[K] SeparableClosure K) (a : Lˣ) {m n : ℕ} {t : Fin m → Kˣ} {b : Fin n → Kˣ}
  (ht :
    QuadraticMap.Equivalent (QuadraticMap.traceTransfer K QuadraticMap.sq)
      (QuadraticMap.weightedSumSquares K fun i => ↑(t i)))
  (hb :
    QuadraticMap.Equivalent (QuadraticMap.traceTransfer K (↑a • QuadraticMap.sq))
      (QuadraticMap.weightedSumSquares K fun i => ↑(b i))) :
  TauCeti.sw1 b =
    TauCeti.sw1 t +
      (CategoryTheory.ConcreteCategory.hom (TauCeti.galoisCor K L σ 1)) (TauCeti.kummerClass a)

The relative Stiefel–Whitney formula in degree one, on the trace forms themselves. Formalized in Tau Ceti as TauCeti.sw1Class_formClass_traceTransfer_smul_sq.

TauCeti.sw1Class_formClass_traceTransfer_smul_sq.{u} {K L : Type u} [Field K] [Field L]
  [Algebra K L] [FiniteDimensional K L] [Invertible 2] [Invertible 2]
  (σ : L →ₐ[K] SeparableClosure K) (a : Lˣ) (ha : QuadraticMap.Nondegenerate)
  (h1 : QuadraticMap.Nondegenerate) :
  TauCeti.sw1Class (TauCeti.formClass (QuadraticMap.traceTransfer K (↑a • QuadraticMap.sq)) ha) =
    TauCeti.sw1Class (TauCeti.formClass (QuadraticMap.traceTransfer K QuadraticMap.sq) h1) +
      (CategoryTheory.ConcreteCategory.hom (TauCeti.galoisCor K L σ 1)) (TauCeti.kummerClass a)

The relative Stiefel–Whitney formula in degree two, on diagonal presentations of the trace forms. Formalized in Tau Ceti as TauCeti.sw2_eq_add_galoisEvens_add_cup_of_equivalent_traceTransfer.

TauCeti.sw2_eq_add_galoisEvens_add_cup_of_equivalent_traceTransfer.{u} {K L : Type u} [Field K]
  [Invertible 2] [Field L] [Algebra K L] [FiniteDimensional K L] [Invertible 2]
  (σ : L →ₐ[K] SeparableClosure K) (hfin : Module.finrank K L = 2) (a : Lˣ) {m n : ℕ}
  {t : Fin m → Kˣ} {b : Fin n → Kˣ}
  (ht :
    QuadraticMap.Equivalent (QuadraticMap.traceTransfer K QuadraticMap.sq)
      (QuadraticMap.weightedSumSquares K fun i => ↑(t i)))
  (hb :
    QuadraticMap.Equivalent (QuadraticMap.traceTransfer K (↑a • QuadraticMap.sq))
      (QuadraticMap.weightedSumSquares K fun i => ↑(b i))) :
  TauCeti.sw2 b =
    TauCeti.sw2 t + TauCeti.galoisEvens K L σ hfin (TauCeti.kummerClass a) +
      (((TauCeti.trivialF2TopPairing (TauCeti.AbsoluteGaloisGroup K)).cup 1 1) (TauCeti.sw1 t))
        ((CategoryTheory.ConcreteCategory.hom (TauCeti.galoisCor K L σ 1)) (TauCeti.kummerClass a))

Sources

LeanTauCeti.sw2Class_formClass_traceTransfer_smul_sq · TauCeti.sw1Class_traceTransfer_mk_rankOne · TauCeti.sw1_eq_add_galoisCor_of_equivalent_scharlauTransfer · TauCeti.sw1_eq_add_galoisCor_of_equivalent_traceTransfer · TauCeti.sw1Class_formClass_traceTransfer_smul_sq · TauCeti.sw2_eq_add_galoisEvens_add_cup_of_equivalent_traceTransfer

Uses 11

Statement usesThe index-two degree-one Evens norm · The Kummer isomorphism · Shapiro's lemma in degree one

Proof usesArtin--Wedderburn over a separably closed field · The comparison isomorphism · The cup-norm theorem · Serre's formula for the Evens norm of a Kummer class (Serre, Théorème 1′ at n = 2) · The Skolem-Noether theorem · The splitting criterion for quaternion algebras · Wedderburn-Artin for central simple algebras · Witt's chain theorem in its nontrivial range

TheoremThe Evens norm of a Kummer class over a local field, as an element of `H²(G_K, 𝔽₂)`#

if L is generated over a local field K by a square root x ∉ K of d, and a ∈ Lˣ has nonzero trace t, then N^{Ev}((a)) = ε((t, −d · N a)_K · (2, d)_K) • ((c) ∪ (e)) for all c, e with (c, e)_K = -1, where ε sends the signs +1, -1 to 0, 1.

TauCeti.galoisEvens_kummerClass_eq_hilbertSymbol_smul.{u} {K L : Type u} [Field K] [ValuativeRel K]
  [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Invertible 2] [Field L] [Algebra K L]
  [FiniteDimensional K L] [Invertible 2] (σ : L →ₐ[K] SeparableClosure K)
  (hfin : Module.finrank K L = 2) {x : L} {d : Kˣ} (hx : x ∉ Set.range ⇑(algebraMap K L))
  (hx2 : x ^ 2 = (algebraMap K L) ↑d) (a : Lˣ) {t : Kˣ} (ht : ↑t = (Algebra.trace K L) ↑a)
  {c e : Kˣ} (hce : TauCeti.hilbertSymbol c e = -1) :
  TauCeti.galoisEvens K L σ hfin (TauCeti.kummerClass a) =
    TauCeti.additiveIntUnitsAddEquiv
        (Additive.ofMul
          (TauCeti.hilbertSymbol t (-(d * (TauCeti.Algebra.normUnits K) a)) *
            TauCeti.hilbertSymbol (unitOfInvertible 2) d)) •
      (((TauCeti.trivialF2TopPairing (TauCeti.AbsoluteGaloisGroup K)).cup 1 1)
          (TauCeti.kummerClass c))
        (TauCeti.kummerClass e)

Lean

Formalized in Tau Ceti as TauCeti.galoisEvens_kummerClass_eq_hilbertSymbol_smul.

Sources

LeanTauCeti.galoisEvens_kummerClass_eq_hilbertSymbol_smul

Uses 9

Statement usesThe index-two degree-one Evens norm

Proof usesA Kummer cup over a local field is its Hilbert symbol times a fixed nonzero cup · Artin--Wedderburn over a separably closed field · The comparison isomorphism · The Kummer isomorphism · Serre's formula for the Evens norm of a Kummer class (Serre, Théorème 1′ at n = 2) · The Skolem-Noether theorem · The splitting criterion for quaternion algebras · Wedderburn-Artin for central simple algebras

TheoremLam's comparison of the Clifford and Hasse invariants (Lam V.3.20)#

For a class of rank n with discriminant d, c(q) = s(q) · [(-1, d)]^C(n-1,2) · [(-1,-1)]^C(n+1,4), where C(n-1,2) = (n-1)(n-2)/2 and C(n+1,4) = (n+1)n(n-1)(n-2)/24.

TauCeti.RegularFormClass.cliffordInvariant_eq_hasseInvariant_mul.{u} {K : Type u} [Field K]
  [Invertible 2] (x : TauCeti.RegularFormClass K) :
  x.cliffordInvariant =
    x.hasseInvariant *
        TauCeti.BrauerGroup.quaternionClassOnSquareClasses (TauCeti.squareClass (-1)) x.discr ^
          (x.rank - 1).choose 2 *
      TauCeti.BrauerGroup.quaternionClass (-1) (-1) ^ (x.rank + 1).choose 4

Lean

Formalized in Tau Ceti as TauCeti.RegularFormClass.cliffordInvariant_eq_hasseInvariant_mul.

Sources

LeanTauCeti.RegularFormClass.cliffordInvariant_eq_hasseInvariant_mul

Uses 3

Proof usesThe splitting criterion for quaternion algebras · The structure theorem in operator form · Witt's chain theorem in its nontrivial range

DefinitionThe Hilbert symbol as a bilinear form over `𝔽₂`#

Over a nonarchimedean local field in which 2 is invertible, the Hilbert symbol on square classes, read in ZMod 2 through the dictionary +1 ↦ 0, -1 ↦ 1, is a ZMod 2-bilinear form on Kˣ/(Kˣ)². Its sign is the symbol (TauCeti.hilbertSign_hilbertSymbolForm).

TauCeti.hilbertSymbolForm.{u_1} (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K] [Invertible 2] :
  LinearMap.BilinForm (ZMod 2) (TauCeti.SquareClassGroup K)

Lean

Formalized in Tau Ceti as TauCeti.hilbertSymbolForm.

Sources

LeanTauCeti.hilbertSymbolForm

Uses 2

Proof usesThe splitting criterion for quaternion algebras · TauCeti.algebraicExtensionNormedField

TheoremA Kummer cup over a local field is its Hilbert symbol times a fixed nonzero cup #

if (c, e)_K = -1, then (a) ∪ (b) = ε • ((c) ∪ (e)), where ε ∈ ZMod 2 is 0 if (a, b)_K = 1 and 1 if (a, b)_K = -1.

TauCeti.cup_kummerClass_eq_hilbertSymbol_smul.{u} {K : Type u} [Field K] [ValuativeRel K]
  [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Invertible 2] {c e : Kˣ}
  (hce : TauCeti.hilbertSymbol c e = -1) (a b : Kˣ) :
  (((TauCeti.trivialF2TopPairing (TauCeti.AbsoluteGaloisGroup K)).cup 1 1) (TauCeti.kummerClass a))
      (TauCeti.kummerClass b) =
    TauCeti.additiveIntUnitsAddEquiv (Additive.ofMul (TauCeti.hilbertSymbol a b)) •
      (((TauCeti.trivialF2TopPairing (TauCeti.AbsoluteGaloisGroup K)).cup 1 1)
          (TauCeti.kummerClass c))
        (TauCeti.kummerClass e)

Lean

Formalized in Tau Ceti as TauCeti.cup_kummerClass_eq_hilbertSymbol_smul.

Sources

LeanTauCeti.cup_kummerClass_eq_hilbertSymbol_smul

Uses 10 · Used by 2

Proof usesArtin--Wedderburn over a separably closed field · The comparison isomorphism · The cup-norm theorem · Hensel's lemma for the norm · The Skolem-Noether theorem · The splitting criterion for quaternion algebras · TauCeti.algebraicExtensionNormedField · Wedderburn-Artin for central simple algebras · Witt decomposition · Witt's chain theorem in its nontrivial range

Used byThe Evens norm of a Kummer class over a local field, as an element of H²(G_K, 𝔽₂) · The Gram formula for the Kummer cup over ℚ₂

TheoremLocal classification (O'Meara 63:20, Serre IV Thm 7)#

A regular-form class over a nonarchimedean local field is determined by its rank, discriminant and local Hasse invariant.

TauCeti.RegularFormClass.localInvariants_injective.{u_1} {K : Type u_1} [Field K] [ValuativeRel K]
  [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Invertible 2] :
  Function.Injective TauCeti.RegularFormClass.localInvariants

Lean

Formalized in Tau Ceti as TauCeti.RegularFormClass.localInvariants_injective.

Sources

LeanTauCeti.RegularFormClass.localInvariants_injective

Uses 4 · Used by 1

Proof usesHensel's lemma for the norm · The splitting criterion for quaternion algebras · TauCeti.algebraicExtensionNormedField · Witt's chain theorem in its nontrivial range

Used byThe classification of regular forms over a local field, as an equivalence

TheoremThe relative Stiefel–Whitney formula over a local field #

for a quadratic extension L of a local field K and a ∈ Lˣ, the Evens norm N^{Ev}((a)) ∈ H²(G_K, 𝔽₂), taken along any K-embedding σ of L into a separable closure of K, vanishes exactly when the twisted trace form Tr_*⟨a⟩ and the trace form Tr_*⟨1⟩ have the same local Hasse invariant.

TauCeti.galoisEvens_kummerClass_eq_zero_iff_localHasse_eq.{u} {K L : Type u} [Field K]
  [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Invertible 2] [Field L]
  [Algebra K L] [FiniteDimensional K L] [Invertible 2] (σ : L →ₐ[K] SeparableClosure K)
  (hfin : Module.finrank K L = 2) (a : Lˣ) (ha : QuadraticMap.Nondegenerate)
  (h1 : QuadraticMap.Nondegenerate) :
  TauCeti.galoisEvens K L σ hfin (TauCeti.kummerClass a) = 0 ↔
    (TauCeti.formClass (QuadraticMap.traceTransfer K (↑a • QuadraticMap.sq)) ha).localHasse =
      (TauCeti.formClass (QuadraticMap.traceTransfer K QuadraticMap.sq) h1).localHasse

Lean

Formalized in Tau Ceti as TauCeti.galoisEvens_kummerClass_eq_zero_iff_localHasse_eq.

Sources

LeanTauCeti.galoisEvens_kummerClass_eq_zero_iff_localHasse_eq

Uses 13

Statement usesThe index-two degree-one Evens norm

Proof usesArtin--Wedderburn over a separably closed field · The comparison isomorphism · The cup-norm theorem · Hensel's lemma for the norm · The Kummer isomorphism · Serre's formula for the Evens norm of a Kummer class (Serre, Théorème 1′ at n = 2) · The Skolem-Noether theorem · The splitting criterion for quaternion algebras · TauCeti.algebraicExtensionNormedField · Wedderburn-Artin for central simple algebras · Witt decomposition · Witt's chain theorem in its nontrivial range

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

Quadratic forms and cohomological invariants

TheoremThe splitting criterion for quaternion algebras#

Lean

Sources

DefinitionThe classification of regular forms over a local field, as an equivalence#

Lean

Sources

TheoremHilbert's product formula#

Lean

Other forms

Sources

DefinitionThe comparison isomorphism#

Lean

Sources

TheoremTauCeti.brauer2EquivH2_baseChange#

Lean

Sources

TheoremThe relative Stiefel–Whitney formula in degree two, on the trace forms themselves (Kahn, Théorème 2 in degree two)#

Lean

Other forms

Sources

TheoremThe Evens norm of a Kummer class over a local field, as an element of H²(G_K, 𝔽₂)#

Lean

Sources

TheoremLam's comparison of the Clifford and Hasse invariants (Lam V.3.20)#

Lean

Sources

DefinitionThe Hilbert symbol as a bilinear form over 𝔽₂#

Lean

Sources

TheoremA Kummer cup over a local field is its Hilbert symbol times a fixed nonzero cup#

Lean

Sources

TheoremLocal classification (O'Meara 63:20, Serre IV Thm 7)#

Lean

Sources

TheoremThe relative Stiefel–Whitney formula over a local field#

Lean

Sources

TheoremThe splitting criterion for quaternion algebras #

DefinitionThe classification of regular forms over a local field, as an equivalence #

TheoremHilbert's product formula #

DefinitionThe comparison isomorphism #

TheoremTauCeti.brauer2EquivH2_baseChange #

TheoremThe Evens norm of a Kummer class over a local field, as an element of `H²(G_K, 𝔽₂)`#

DefinitionThe Hilbert symbol as a bilinear form over `𝔽₂`#

TheoremA Kummer cup over a local field is its Hilbert symbol times a fixed nonzero cup #

TheoremThe relative Stiefel–Whitney formula over a local field #