Documentation

TauCeti.Algebra.BrauerGroup.TwoTorsionBaseChange

Base change of the 2-torsion Brauer subgroup #

Scalar extension preserves the subgroup of Brauer classes whose square is trivial. This file restricts the Brauer-group base-change homomorphism to that subgroup and records its functoriality. It also restricts the identification TauCeti.BrauerGroup.uliftEquiv of the Brauer group of K with that of its universe lift ULift K to the 2-torsion subgroups.

source
def TauCeti.BrauerGroup.twoTorsionBaseChange (K : Type u) [Field K] (L : Type u) [Field L] [Algebra K L] :
↥(twoTorsion K) →* ↥(twoTorsion L)

The restriction of Brauer base change to the 2-torsion subgroups.

Instances For
    source
    @[simp]
    theorem TauCeti.BrauerGroup.coe_twoTorsionBaseChange (K : Type u) [Field K] (L : Type u) [Field L] [Algebra K L] (x : ↥(twoTorsion K)) :
    ↑((twoTorsionBaseChange K L) x) = (baseChange K L) ↑x

    Coercing the restricted base-change homomorphism to the Brauer group gives ordinary base change.

    source
    @[simp]
    theorem TauCeti.BrauerGroup.twoTorsionBaseChange_self (K : Type u) [Field K] :
    twoTorsionBaseChange K K = MonoidHom.id ↥(twoTorsion K)

    Base change along the identity restricts to the identity on 2-torsion.

    source
    @[simp]
    theorem TauCeti.BrauerGroup.twoTorsionBaseChange_comp (K : Type u) [Field K] (L : Type u) [Field L] [Algebra K L] (M : Type u) [Field M] [Algebra K M] [Algebra L M] [IsScalarTower K L M] :
    (twoTorsionBaseChange L M).comp (twoTorsionBaseChange K L) = twoTorsionBaseChange K M

    Restricted base change composes along a tower of field extensions.

    source
    noncomputable def TauCeti.BrauerGroup.twoTorsionUliftEquiv (K : Type u) [Field K] :
    ↥(twoTorsion K) ≃* ↥(twoTorsion (ULift.{w, u} K))

    The 2-torsion of the Brauer group of a universe lift. The restriction of TauCeti.BrauerGroup.uliftEquiv, scalar extension from K to ULift K, to the 2-torsion subgroups.

    Instances For
      source
      @[simp]
      theorem TauCeti.BrauerGroup.coe_twoTorsionUliftEquiv (K : Type u) [Field K] (x : ↥(twoTorsion K)) :
      ↑((twoTorsionUliftEquiv K) x) = (uliftEquiv K) ↑x

      Coercing the restricted identification to the Brauer group gives uliftEquiv.

      source
      @[simp]
      theorem TauCeti.BrauerGroup.coe_twoTorsionUliftEquiv_symm (K : Type u) [Field K] (y : ↥(twoTorsion (ULift.{w, u} K))) :
      ↑((twoTorsionUliftEquiv K).symm y) = (uliftEquiv K).symm ↑y

      Coercing the inverse of the restricted identification to the Brauer group gives the inverse of uliftEquiv.