Module

QuadraticSquareClasses.lean

Nyll.GaloisCohomology.Kummer.Concrete.QuadraticSquareClasses

4 declarations indexed from sourceView source ↗

Module documentation

Square classes in quadratic Galois extensions

The nontrivial automorphism has exactly the base field as its fixed field. An anti-invariant generator gives the two base-field square classes which become squares in the extension.

Imports5

Mathlib.FieldTheory.Galois.Basic
Mathlib.SetTheory.Cardinal.Finite
Mathlib.Algebra.Ring.Parity
Mathlib.Tactic.LinearCombination
Mathlib.Tactic.FieldSimp

Imported by2

theorem

quadratic_aut_fixed_iff

L26 ↗

KummerTheory.quadratic_aut_fixed_iff

Documentation

An element fixed by the nonidentity quadratic automorphism lies in the base field.

Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace KummerTheory
universe u v

Lean source · statement

theorem quadratic_aut_fixed_iff
    {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L] [IsGalois K L]
    (hdim : Module.finrank K L = 2) (τ : Gal(L/K)) (hτ : τ ≠ 1) (z : L) :
    τ z = z ↔ ∃ x : K, algebraMap K L x = z

theorem

quadratic_aut_apply_twice

L47 ↗

KummerTheory.quadratic_aut_apply_twice

Documentation

Every automorphism of a quadratic Galois extension is an involution.

Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace KummerTheory
universe u v

Lean source · statement

theorem quadratic_aut_apply_twice
    {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L] [IsGalois K L]
    (hdim : Module.finrank K L = 2) (τ : Gal(L/K)) (z : L) :
    τ (τ z) = z

theorem

exists_quadratic_antiInvariant

L58 ↗

KummerTheory.exists_quadratic_antiInvariant

Documentation

In characteristic zero a nonidentity quadratic automorphism supplies a nonsquare radicand.

Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace KummerTheory
universe u v

Lean source · statement

theorem exists_quadratic_antiInvariant
    {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L] [IsGalois K L]
    [CharZero K] (hdim : Module.finrank K L = 2) (τ : Gal(L/K)) (hτ : τ ≠ 1) :
    ∃ a : K, ∃ α : L, α ≠ 0 ∧ α ^ 2 = algebraMap K L a ∧
      τ α = -α ∧ ¬ IsSquare a

theorem

isSquare_algebraMap_iff_of_quadratic

L92 ↗

KummerTheory.isSquare_algebraMap_iff_of_quadratic

Documentation

A base-field element becomes a square exactly in the trivial or defining square class.

Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace KummerTheory
universe u v

Lean source · statement

theorem isSquare_algebraMap_iff_of_quadratic
    {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L] [IsGalois K L]
    (hdim : Module.finrank K L = 2) (τ : Gal(L/K)) (hτ : τ ≠ 1)
    (a : K) (α : L) (hα0 : α ≠ 0)
    (hαsq : α ^ 2 = algebraMap K L a) (hanti : τ α = -α) (c : K) :
    IsSquare (algebraMap K L c) ↔ IsSquare c ∨ IsSquare (c / a)

Module documentation

Square classes in quadratic Galois extensions

Declarations

quadratic_aut_fixed_iff

quadratic_aut_apply_twice

exists_quadratic_antiInvariant

isSquare_algebraMap_iff_of_quadratic