Documentation

TauCeti.Algebra.CrossedProduct.Quadratic

The cocycle of a quadratic extension #

Let L be a commutative K-algebra whose automorphism group Aut_K(L) has order two, generated by σ. For b ∈ Kˣ, the quadratic cocycle TauCeti.TwoCocycle.quadratic h b is the 2-cocycle of Aut_K(L) with values in Lˣ whose only nontrivial value is c(σ, σ) = b. It is the cocycle behind the quaternion algebra: when char K ≠ 2 and L = K(√a), its crossed product is generated over L by u_σ with u_σ² = b and u_σ √a = -√a u_σ, which are the relations of (a, b)_K.

For L/K Galois this cocycle computes the second cohomology of the cyclic group Gal(L/K) of order two:

Kˣ / N_{L/K}(Lˣ) ≃ H²(Gal(L/K), Lˣ), [b] ↦ [quadratic h b]

(TauCeti.quadraticNormQuotientEquiv). Indeed the quadratic cocycle is the carry cocycle of b at the generator σ, so its class is TauCeti.cyclicClass of b (TauCeti.TwoCocycle.cohomologyClass_quadratic). Consequently every cocycle is cohomologous to a quadratic one, and the quadratic cocycle of b is a coboundary exactly when b is a norm from L. Since the group of order two has a unique generator, this identification involves no choice.

Main definitions #

Main results #

References #

source
noncomputable def TauCeti.TwoCocycle.quadratic {K : Type u_1} {L : Type u_2} [CommSemiring K] [CommRing L] [Algebra K L] (h : Nat.card (L ≃ₐ[K] L) = 2) (b : Kˣ) :
TwoCocycle K L

The quadratic cocycle of b ∈ Kˣ, for an automorphism group Aut_K(L) of order two: the 2-cocycle c with c(σ, σ) = b for the nontrivial automorphism σ, and c(σ, τ) = 1 whenever σ or τ is trivial.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.TwoCocycle.quadratic_toFun_one_right {K : Type u_1} {L : Type u_2} [CommSemiring K] [CommRing L] [Algebra K L] (h : Nat.card (L ≃ₐ[K] L) = 2) (b : Kˣ) (σ : L ≃ₐ[K] L) :
    (quadratic h b).toFun σ 1 = 1

    The quadratic cocycle is trivial when its second argument is; with TauCeti.TwoCocycle.toFun_one_left, it is also trivial when its first argument is.

    source
    @[simp]
    theorem TauCeti.TwoCocycle.quadratic_toFun_of_ne_one_of_ne_one {K : Type u_1} {L : Type u_2} [CommSemiring K] [CommRing L] [Algebra K L] (h : Nat.card (L ≃ₐ[K] L) = 2) (b : Kˣ) {σ τ : L ≃ₐ[K] L} (hσ : σ ≠ 1) (hτ : τ ≠ 1) :
    (quadratic h b).toFun σ τ = (Units.map ↑(algebraMap K L)) b

    On two nontrivial automorphisms, which are both the generator, the quadratic cocycle of b takes the value b.

    source
    @[simp]
    theorem TauCeti.TwoCocycle.quadratic_one {K : Type u_1} {L : Type u_2} [CommSemiring K] [CommRing L] [Algebra K L] (h : Nat.card (L ≃ₐ[K] L) = 2) :
    quadratic h 1 = 1

    The quadratic cocycle of 1 is trivial.

    source
    @[simp]
    theorem TauCeti.TwoCocycle.quadratic_mul {K : Type u_1} {L : Type u_2} [CommSemiring K] [CommRing L] [Algebra K L] (h : Nat.card (L ≃ₐ[K] L) = 2) (a b : Kˣ) :
    quadratic h (a * b) = quadratic h a * quadratic h b

    The quadratic cocycle is multiplicative in b.

    source
    theorem TauCeti.TwoCocycle.cohomologyClass_quadratic {K L : Type} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] (h : Nat.card Gal(L/K) = 2) {σ : Gal(L/K)} (hσ : ∀ (τ : Gal(L/K)), τ ∈ Subgroup.zpowers σ) (b : Kˣ) :
    (quadratic h b).cohomologyClass = (cyclicClass hσ) (Additive.ofMul b)

    The quadratic cocycle is the carry cocycle. When the automorphism group Aut_K(L) has order two and is generated by σ, the class of the quadratic cocycle of b in H²(Aut_K(L), Lˣ) is the class of b under two-periodicity at σ.

    source
    @[simp]
    theorem TauCeti.TwoCocycle.cohomologyClass_quadratic_eq_zero_iff {K L : Type} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (h : Nat.card Gal(L/K) = 2) (b : Kˣ) :
    (quadratic h b).cohomologyClass = 0 ↔ b ∈ normGroup K L

    The class of the quadratic cocycle of b vanishes exactly when b is a norm from L.

    source
    @[simp]
    theorem TauCeti.TwoCocycle.cohomologyClass_quadratic_eq_iff {K L : Type} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (h : Nat.card Gal(L/K) = 2) (a b : Kˣ) :
    (quadratic h a).cohomologyClass = (quadratic h b).cohomologyClass ↔ a / b ∈ normGroup K L

    The classes of the quadratic cocycles of a and b agree exactly when a / b is a norm from L.

    source
    theorem TauCeti.TwoCocycle.cohomologous_quadratic_iff {K L : Type} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (h : Nat.card Gal(L/K) = 2) (a b : Kˣ) :
    (quadratic h a).Cohomologous (quadratic h b) ↔ a / b ∈ normGroup K L

    The quadratic cocycles of a and b are cohomologous exactly when a / b is a norm from L.

    source
    theorem TauCeti.TwoCocycle.exists_cohomologous_quadratic {K L : Type} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (h : Nat.card Gal(L/K) = 2) (z : TwoCocycle K L) :
    ∃ (b : Kˣ), z.Cohomologous (quadratic h b)

    Every 2-cocycle of a quadratic Galois extension is cohomologous to a quadratic cocycle.

    source
    noncomputable def TauCeti.quadraticNormQuotientEquiv {K L : Type} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (h : Nat.card Gal(L/K) = 2) :
    Additive (Kˣ ⧸ normGroup K L) ≃+ ↑(groupCohomology.H2 (Rep.ofMulDistribMulAction Gal(L/K) Lˣ))

    H² of a quadratic Galois extension is the norm quotient: Kˣ / N_{L/K}(Lˣ) ≃ H²(Gal(L/K), Lˣ), sending the class of b to the class of the quadratic cocycle of b (quadraticNormQuotientEquiv_mk).

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.quadraticNormQuotientEquiv_mk {K L : Type} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (h : Nat.card Gal(L/K) = 2) (b : Kˣ) :
      (quadraticNormQuotientEquiv h) (Additive.ofMul ↑b) = (TwoCocycle.quadratic h b).cohomologyClass

      quadraticNormQuotientEquiv sends the class of b ∈ Kˣ to the class of the quadratic cocycle of b.