The Galois 2-cocycle of a split algebra

Let A be a K-algebra and L a field equipped with a K-algebra structure, and suppose we are given descent data in the form of an L-algebra isomorphism φ : L ⊗[K] A ≃ₐ[L] Mₙ(L). This file attaches to φ a 2-cocycle of Aut_K(L) with values in Lˣ, in the normalization of TauCeti.TwoCocycle.

Each σ : L ≃ₐ[K] L acts on L ⊗[K] A by σ ⊗ 1 and on Mₙ(L) entrywise, and both actions are σ-semilinear. Transporting σ ⊗ 1 along φ and undoing the entrywise action gives the automorphism splittingAut φ σ = φ ∘ (σ ⊗ 1) ∘ φ⁻¹ ∘ σ⁻¹ of Mₙ(L), which is L-linear. By Skolem–Noether (TauCeti.exists_unit_conj_of_algEquiv) it is conjugation by some g_σ ∈ GL_n(L), determined up to Lˣ. The automorphisms satisfy splittingAut φ (στ) = splittingAut φ σ ∘ σ ∘ splittingAut φ τ ∘ σ⁻¹, so g_στ and g_σ · σ(g_τ) induce the same conjugation and differ by a unit scalar; this scalar is the cocycle: c(σ, τ) · g_σ · σ(g_τ) = g_στ.

The construction is carried out for an arbitrary family of conjugators in TauCeti.TwoCocycle.ofConjugators, since the cocycle depends on the conjugators and not only on φ; TauCeti.cocycleOfSplitting is the cocycle of the conjugators chosen by TauCeti.splittingConjugator. Only the choice of conjugators, via Skolem–Noether, needs L to be a field: splittingAut and its lemmas are stated for a commutative semiring L, and TauCeti.TwoCocycle.ofConjugators for a commutative ring L.

Up to coboundaries the cocycle depends on neither choice. Two families of conjugators for the same φ differ by unit scalars, and their cocycles by the coboundary of those scalars; and two splittings into the same Mₙ(L) differ, by Skolem–Noether, by an inner automorphism of Mₙ(L), which transforms the conjugators of one into conjugators of the other without changing the cocycle. Splittings into matrix algebras of different index types reduce to this case by reindexing, which does not change the cocycle either.

Main definitions

• TauCeti.splittingAut φ σ: the L-algebra automorphism φ ∘ (σ ⊗ 1) ∘ φ⁻¹ ∘ σ⁻¹ of Mₙ(L).
• TauCeti.splittingConjugator φ σ: a chosen g_σ ∈ GL_n(L) with splittingAut φ σ equal to conjugation by g_σ.
• TauCeti.TwoCocycle.ofConjugators φ g hg: the 2-cocycle of a family g of conjugators, the unit scalars c(σ, τ) with c(σ, τ) · g_σ · σ(g_τ) = g_στ.
• TauCeti.cocycleOfSplitting φ: the cocycle of the chosen conjugators.

Main results

• TauCeti.splittingAut_mul: the twisted multiplicativity of σ ↦ splittingAut φ σ.
• TauCeti.TwoCocycle.ofConjugators_toFun_eq_iff: the value c(σ, τ) is the unique unit u with u · g_σ · σ(g_τ) = g_στ.
• TauCeti.cocycleOfSplitting_toFun_eq_iff: the same characterization of cocycleOfSplitting φ with respect to the chosen conjugators splittingConjugator φ σ.
• TauCeti.TwoCocycle.cohomologous_ofConjugators: two families of conjugators for the same splitting give cohomologous cocycles.
• TauCeti.cohomologous_cocycleOfSplitting: two splittings φ : L ⊗[K] A ≃ₐ[L] Mₙ(L) and φ' : L ⊗[K] A ≃ₐ[L] Mₘ(L) give cohomologous cocycles.

Implementation notes

The sign of the cocycle is chosen with the crossed product in mind: for the crossed product A = (L, Aut_K(L), c), split by a ⊗ x ↦ (v ↦ a · v · x) into the L-linear endomorphisms of A as a right L-vector space with basis u_σ, the conjugators satisfy c(σ, τ) · g_σ · σ(g_τ) = g_στ for the defining cocycle c. The connecting map of 1 → Lˣ → GL_n(L) → PGL_n(L) → 1, which reads g_σ · σ(g_τ) = δ(σ, τ) · g_στ, is the inverse cocycle and presents the opposite algebra.

References

• P. Gille and T. Szamuely, Central Simple Algebras and Galois Cohomology (2006), Ch. 2 and §4.4.
• J.-P. Serre, Local Fields, GTM 67 (1979), Chapter X.

noncomputable def TauCeti.splittingAut {K : Type u} [CommSemiring K] {A : Type w} [Semiring A] [Algebra K A] {n : Type u_1} [Fintype n] [DecidableEq n] {L : Type v} [CommSemiring L] [Algebra K L] (φ : TensorProduct K L A ≃ₐ[L] Matrix n n L) (σ : L ≃ₐ[K] L) : Matrix n n L ≃ₐ[L] Matrix n n L

The automorphism φ ∘ (σ ⊗ 1) ∘ φ⁻¹ ∘ σ⁻¹ of Mₙ(L) attached to a splitting φ : L ⊗[K] A ≃ₐ[L] Mₙ(L) and σ : L ≃ₐ[K] L, where σ⁻¹ acts on matrices entrywise. The two semilinear twists cancel, so it is an automorphism of L-algebras.

Equations

• TauCeti.splittingAut φ σ = AlgEquiv.ofRingEquiv ⋯

theorem TauCeti.splittingAut_apply {K : Type u} [CommSemiring K] {A : Type w} [Semiring A] [Algebra K A] {n : Type u_1} [Fintype n] [DecidableEq n] {L : Type v} [CommSemiring L] [Algebra K L] (φ : TensorProduct K L A ≃ₐ[L] Matrix n n L) (σ : L ≃ₐ[K] L) (m : Matrix n n L) : (splittingAut φ σ) m = φ ((Algebra.TensorProduct.congr σ AlgEquiv.refl) (φ.symm (m.map ⇑σ.symm)))

The defining formula of splittingAut.

@[simp]

theorem TauCeti.splittingAut_map {K : Type u} [CommSemiring K] {A : Type w} [Semiring A] [Algebra K A] {n : Type u_1} [Fintype n] [DecidableEq n] {L : Type v} [CommSemiring L] [Algebra K L] (φ : TensorProduct K L A ≃ₐ[L] Matrix n n L) (σ : L ≃ₐ[K] L) (m : Matrix n n L) : (splittingAut φ σ) (m.map ⇑σ) = φ ((Algebra.TensorProduct.congr σ AlgEquiv.refl) (φ.symm m))

On an entrywise image σ(m), splittingAut φ σ is σ ⊗ 1 transported along φ.

theorem TauCeti.splittingAut_mul {K : Type u} [CommSemiring K] {A : Type w} [Semiring A] [Algebra K A] {n : Type u_1} [Fintype n] [DecidableEq n] {L : Type v} [CommSemiring L] [Algebra K L] (φ : TensorProduct K L A ≃ₐ[L] Matrix n n L) (σ τ : L ≃ₐ[K] L) (m : Matrix n n L) : (splittingAut φ (σ * τ)) (m.map ⇑σ) = (splittingAut φ σ) (((splittingAut φ τ) m).map ⇑σ)

Twisted multiplicativity: splittingAut φ (στ) = splittingAut φ σ ∘ σ ∘ splittingAut φ τ ∘ σ⁻¹, the cocycle condition for σ ↦ splittingAut φ σ with values in the automorphisms of Mₙ(L).

noncomputable def TauCeti.TwoCocycle.ofConjugators {K : Type u} [CommSemiring K] {A : Type w} [Semiring A] [Algebra K A] {n : Type u_1} [Fintype n] [DecidableEq n] {L : Type v} [CommRing L] [Algebra K L] (φ : TensorProduct K L A ≃ₐ[L] Matrix n n L) [Nonempty n] (g : (L ≃ₐ[K] L) → GL n L) (hg : ∀ (σ : L ≃ₐ[K] L) (m : Matrix n n L), ↑(g σ) * m * ↑(g σ)⁻¹ = (splittingAut φ σ) m) : TwoCocycle K L

The 2-cocycle of a family of conjugators for a splitting φ : L ⊗[K] A ≃ₐ[L] Mₙ(L): given g_σ ∈ GL_n(L) with splittingAut φ σ equal to conjugation by g_σ for every σ, the value c(σ, τ) is the unit scalar with c(σ, τ) · g_σ · σ(g_τ) = g_στ, characterized by TauCeti.TwoCocycle.ofConjugators_toFun_eq_iff.

Equations

• TauCeti.TwoCocycle.ofConjugators φ g hg = { toFun := fun (σ τ : L ≃ₐ[K] L) => ⋯.choose, isMulCocycle₂ := ⋯ }

@[simp]

theorem TauCeti.TwoCocycle.scalar_ofConjugators_mul {K : Type u} [CommSemiring K] {A : Type w} [Semiring A] [Algebra K A] {n : Type u_1} [Fintype n] [DecidableEq n] {L : Type v} [CommRing L] [Algebra K L] (φ : TensorProduct K L A ≃ₐ[L] Matrix n n L) [Nonempty n] (g : (L ≃ₐ[K] L) → GL n L) (hg : ∀ (σ : L ≃ₐ[K] L) (m : Matrix n n L), ↑(g σ) * m * ↑(g σ)⁻¹ = (splittingAut φ σ) m) (σ τ : L ≃ₐ[K] L) : (Matrix.GeneralLinearGroup.scalar n) ((ofConjugators φ g hg).toFun σ τ) * (g σ * (Matrix.GeneralLinearGroup.map ↑σ) (g τ)) = g (σ * τ)

The defining property of TwoCocycle.ofConjugators: c(σ, τ) · g_σ · σ(g_τ) = g_στ.

theorem TauCeti.TwoCocycle.ofConjugators_toFun_eq_iff {K : Type u} [CommSemiring K] {A : Type w} [Semiring A] [Algebra K A] {n : Type u_1} [Fintype n] [DecidableEq n] {L : Type v} [CommRing L] [Algebra K L] (φ : TensorProduct K L A ≃ₐ[L] Matrix n n L) [Nonempty n] (g : (L ≃ₐ[K] L) → GL n L) (hg : ∀ (σ : L ≃ₐ[K] L) (m : Matrix n n L), ↑(g σ) * m * ↑(g σ)⁻¹ = (splittingAut φ σ) m) (σ τ : L ≃ₐ[K] L) (u : Lˣ) : (ofConjugators φ g hg).toFun σ τ = u ↔ (Matrix.GeneralLinearGroup.scalar n) u * (g σ * (Matrix.GeneralLinearGroup.map ↑σ) (g τ)) = g (σ * τ)

Characterization of the cocycle of a conjugator family: c(σ, τ) is the unique unit u with u · g_σ · σ(g_τ) = g_στ.

theorem TauCeti.TwoCocycle.cohomologous_ofConjugators {K : Type u} [CommSemiring K] {A : Type w} [Semiring A] [Algebra K A] {n : Type u_1} [Fintype n] [DecidableEq n] {L : Type v} [CommRing L] [Algebra K L] (φ : TensorProduct K L A ≃ₐ[L] Matrix n n L) [Nonempty n] (g g' : (L ≃ₐ[K] L) → GL n L) (hg : ∀ (σ : L ≃ₐ[K] L) (m : Matrix n n L), ↑(g σ) * m * ↑(g σ)⁻¹ = (splittingAut φ σ) m) (hg' : ∀ (σ : L ≃ₐ[K] L) (m : Matrix n n L), ↑(g' σ) * m * ↑(g' σ)⁻¹ = (splittingAut φ σ) m) : (ofConjugators φ g hg).Cohomologous (ofConjugators φ g' hg')

The cocycle does not depend on the choice of conjugators, up to coboundaries: two families g and g' of conjugators for the same splitting φ differ by unit scalars b(σ), with g'_σ = b(σ) · g_σ, and their cocycles differ by the coboundary of b⁻¹.

noncomputable def TauCeti.splittingConjugator {K : Type u} [CommSemiring K] {A : Type w} [Semiring A] [Algebra K A] {n : Type u_1} [Fintype n] [DecidableEq n] {L : Type v} [Field L] [Algebra K L] (φ : TensorProduct K L A ≃ₐ[L] Matrix n n L) [Nonempty n] (σ : L ≃ₐ[K] L) : GL n L

A chosen conjugator g_σ ∈ GL_n(L) for splittingAut φ σ, so that splittingAut φ σ is m ↦ g_σ * m * g_σ⁻¹. It is determined by φ and σ only up to a unit scalar.

Equations

• TauCeti.splittingConjugator φ σ = ⋯.choose

@[simp]

theorem TauCeti.splittingConjugator_mul_mul_inv {K : Type u} [CommSemiring K] {A : Type w} [Semiring A] [Algebra K A] {n : Type u_1} [Fintype n] [DecidableEq n] {L : Type v} [Field L] [Algebra K L] (φ : TensorProduct K L A ≃ₐ[L] Matrix n n L) [Nonempty n] (σ : L ≃ₐ[K] L) (m : Matrix n n L) : ↑(splittingConjugator φ σ) * m * (↑(splittingConjugator φ σ))⁻¹ = (splittingAut φ σ) m

splittingAut φ σ is conjugation by splittingConjugator φ σ. It is stated with the matrix inverse (↑g_σ)⁻¹, the simp normal form of ↑(g_σ⁻¹) under Matrix.coe_units_inv.

noncomputable def TauCeti.cocycleOfSplitting {K : Type u} [CommSemiring K] {A : Type w} [Semiring A] [Algebra K A] {n : Type u_1} [Fintype n] [DecidableEq n] {L : Type v} [Field L] [Algebra K L] (φ : TensorProduct K L A ≃ₐ[L] Matrix n n L) [Nonempty n] : TwoCocycle K L

The cocycle of a split algebra with chosen descent data: for a splitting φ : L ⊗[K] A ≃ₐ[L] Mₙ(L) with n nonempty, the 2-cocycle of the conjugators splittingConjugator φ σ, that is, the unit scalars c(σ, τ) with c(σ, τ) · g_σ · σ(g_τ) = g_στ.

Equations

• TauCeti.cocycleOfSplitting φ = TauCeti.TwoCocycle.ofConjugators φ (TauCeti.splittingConjugator φ) ⋯

@[simp]

theorem TauCeti.scalar_cocycleOfSplitting_mul {K : Type u} [CommSemiring K] {A : Type w} [Semiring A] [Algebra K A] {n : Type u_1} [Fintype n] [DecidableEq n] {L : Type v} [Field L] [Algebra K L] (φ : TensorProduct K L A ≃ₐ[L] Matrix n n L) [Nonempty n] (σ τ : L ≃ₐ[K] L) : (Matrix.GeneralLinearGroup.scalar n) ((cocycleOfSplitting φ).toFun σ τ) * (splittingConjugator φ σ * (Matrix.GeneralLinearGroup.map ↑σ) (splittingConjugator φ τ)) = splittingConjugator φ (σ * τ)

The defining property of cocycleOfSplitting: with g_σ = splittingConjugator φ σ, c(σ, τ) · g_σ · σ(g_τ) = g_στ.

theorem TauCeti.cocycleOfSplitting_toFun_eq_iff {K : Type u} [CommSemiring K] {A : Type w} [Semiring A] [Algebra K A] {n : Type u_1} [Fintype n] [DecidableEq n] {L : Type v} [Field L] [Algebra K L] (φ : TensorProduct K L A ≃ₐ[L] Matrix n n L) [Nonempty n] (σ τ : L ≃ₐ[K] L) (u : Lˣ) : (cocycleOfSplitting φ).toFun σ τ = u ↔ (Matrix.GeneralLinearGroup.scalar n) u * (splittingConjugator φ σ * (Matrix.GeneralLinearGroup.map ↑σ) (splittingConjugator φ τ)) = splittingConjugator φ (σ * τ)

Characterization of the cocycle of a split algebra: with g_σ = splittingConjugator φ σ, c(σ, τ) is the unique unit u with u · g_σ · σ(g_τ) = g_στ.

theorem TauCeti.cohomologous_cocycleOfSplitting {K : Type u} [CommSemiring K] {A : Type w} [Semiring A] [Algebra K A] {n : Type u_1} [Fintype n] [DecidableEq n] {L : Type v} [Field L] [Algebra K L] (φ : TensorProduct K L A ≃ₐ[L] Matrix n n L) [Nonempty n] {m : Type u_2} [Fintype m] [DecidableEq m] [Nonempty m] (φ' : TensorProduct K L A ≃ₐ[L] Matrix m m L) : (cocycleOfSplitting φ).Cohomologous (cocycleOfSplitting φ')

The cocycle of a split algebra does not depend on the splitting, up to coboundaries: two L-algebra isomorphisms φ : L ⊗[K] A ≃ₐ[L] Mₙ(L) and φ' : L ⊗[K] A ≃ₐ[L] Mₘ(L) give cohomologous cocycles. The index types n and m have the same cardinality, since Mₙ(L) and Mₘ(L) are isomorphic, so φ' is reduced to a splitting into Mₙ(L) by reindexing.