Restriction of crossed products to an intermediate scalar ring

For a scalar tower from commutative semirings K and L to a commutative ring E, restricting a cocycle of Aut_K(E) to Aut_L(E) embeds its crossed product in the original crossed product. The embedding sends each coefficient to itself and each basis element u_σ to u_{σ|K}. Its image consists exactly of the elements whose supported automorphisms fix the image of algebraMap L E. When E has no zero divisors, this image is the centralizer of the image of L under inc c ∘ algebraMap L E.

This identifies the algebra of a restricted cocycle, the algebraic ingredient in comparing scalar extension of Brauer classes with restriction in Galois cohomology. Neither finiteness nor a Galois hypothesis is needed for the embedding or its centralizer description.

References

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

def TauCeti.TwoCocycle.restrict {K : Type u_1} {E : Type u_3} [CommSemiring K] [CommRing E] [Algebra K E] (c : TwoCocycle K E) (L : Type u_4) [CommSemiring L] [Algebra K L] [Algebra L E] [IsScalarTower K L E] : TwoCocycle L E

Restrict a cocycle to the automorphisms fixing the intermediate scalar ring L.

@[simp]

theorem TauCeti.TwoCocycle.restrict_toFun {K : Type u_1} {L : Type u_2} {E : Type u_3} [CommSemiring K] [CommSemiring L] [CommRing E] [Algebra K L] [Algebra K E] [Algebra L E] [IsScalarTower K L E] (c : TwoCocycle K E) (σ τ : E ≃ₐ[L] E) : (c.restrict L).toFun σ τ = c.toFun (AlgEquiv.restrictScalars K σ) (AlgEquiv.restrictScalars K τ)

Restriction evaluates the original cocycle on the underlying K-automorphisms.

@[simp]

theorem TauCeti.TwoCocycle.restrict_one {K : Type u_1} {L : Type u_2} {E : Type u_3} [CommSemiring K] [CommSemiring L] [CommRing E] [Algebra K L] [Algebra K E] [Algebra L E] [IsScalarTower K L E] : restrict 1 L = 1

Restriction preserves the trivial cocycle.

@[simp]

theorem TauCeti.TwoCocycle.restrict_mul {K : Type u_1} {L : Type u_2} {E : Type u_3} [CommSemiring K] [CommSemiring L] [CommRing E] [Algebra K L] [Algebra K E] [Algebra L E] [IsScalarTower K L E] (c d : TwoCocycle K E) : (c * d).restrict L = c.restrict L * d.restrict L

Restriction preserves multiplication of cocycles.

@[simp]

theorem TauCeti.TwoCocycle.restrict_inv {K : Type u_1} {L : Type u_2} {E : Type u_3} [CommSemiring K] [CommSemiring L] [CommRing E] [Algebra K L] [Algebra K E] [Algebra L E] [IsScalarTower K L E] (c : TwoCocycle K E) : c⁻¹.restrict L = (c.restrict L)⁻¹

Restriction preserves inversion of cocycles.

@[simp]

theorem TauCeti.TwoCocycle.restrict_div {K : Type u_1} {L : Type u_2} {E : Type u_3} [CommSemiring K] [CommSemiring L] [CommRing E] [Algebra K L] [Algebra K E] [Algebra L E] [IsScalarTower K L E] (c d : TwoCocycle K E) : (c / d).restrict L = c.restrict L / d.restrict L

Restriction preserves division of cocycles.

@[simp]

theorem TauCeti.TwoCocycle.restrict_pow {K : Type u_1} {L : Type u_2} {E : Type u_3} [CommSemiring K] [CommSemiring L] [CommRing E] [Algebra K L] [Algebra K E] [Algebra L E] [IsScalarTower K L E] (c : TwoCocycle K E) (n : ℕ) : (c ^ n).restrict L = c.restrict L ^ n

Restriction preserves natural powers of cocycles.

@[simp]

theorem TauCeti.TwoCocycle.restrict_zpow {K : Type u_1} {L : Type u_2} {E : Type u_3} [CommSemiring K] [CommSemiring L] [CommRing E] [Algebra K L] [Algebra K E] [Algebra L E] [IsScalarTower K L E] (c : TwoCocycle K E) (n : ℤ) : (c ^ n).restrict L = c.restrict L ^ n

Restriction preserves integer powers of cocycles.

@[instance_reducible, instance 100]

noncomputable instance TauCeti.CrossedProduct.instAlgebraRestrict {K : Type u_1} {L : Type u_2} {E : Type u_3} [CommSemiring K] [CommSemiring L] [CommRing E] [Algebra K L] [Algebra K E] [Algebra L E] [IsScalarTower K L E] (c : TwoCocycle K E) : Algebra K (CrossedProduct (c.restrict L))

The restricted crossed product is a K-algebra through its L-algebra structure.

@[instance 100]

instance TauCeti.CrossedProduct.instIsScalarTowerRestrictBase {K : Type u_1} {L : Type u_2} {E : Type u_3} [CommSemiring K] [CommSemiring L] [CommRing E] [Algebra K L] [Algebra K E] [Algebra L E] [IsScalarTower K L E] (c : TwoCocycle K E) : IsScalarTower K L (CrossedProduct (c.restrict L))

The restricted crossed product carries a scalar tower from K through L.

@[instance 100]

instance TauCeti.CrossedProduct.instIsScalarTowerRestrict {K : Type u_1} {L : Type u_2} {E : Type u_3} [CommSemiring K] [CommSemiring L] [CommRing E] [Algebra K L] [Algebra K E] [Algebra L E] [IsScalarTower K L E] (c : TwoCocycle K E) : IsScalarTower K E (CrossedProduct (c.restrict L))

The induced K-action is compatible with the left coefficient action of E.

noncomputable def TauCeti.CrossedProduct.restrictHom {K : Type u_1} {L : Type u_2} {E : Type u_3} [CommSemiring K] [CommSemiring L] [CommRing E] [Algebra K L] [Algebra K E] [Algebra L E] [IsScalarTower K L E] (c : TwoCocycle K E) : CrossedProduct (c.restrict L) →ₐ[K] CrossedProduct c

The embedding of the crossed product of the restricted cocycle, compatible with the K-algebra structure induced by its L-algebra structure.

@[simp]

theorem TauCeti.CrossedProduct.restrictHom_smul_basis {K : Type u_1} {L : Type u_2} {E : Type u_3} [CommSemiring K] [CommSemiring L] [CommRing E] [Algebra K L] [Algebra K E] [Algebra L E] [IsScalarTower K L E] (c : TwoCocycle K E) (σ : E ≃ₐ[L] E) (x : E) : (restrictHom c) (x • (basis (c.restrict L)) σ) = x • (basis c) (AlgEquiv.restrictScalars K σ)

The embedding preserves a coefficient times a basis element.

@[simp]

theorem TauCeti.CrossedProduct.restrictHom_basis {K : Type u_1} {L : Type u_2} {E : Type u_3} [CommSemiring K] [CommSemiring L] [CommRing E] [Algebra K L] [Algebra K E] [Algebra L E] [IsScalarTower K L E] (c : TwoCocycle K E) (σ : E ≃ₐ[L] E) : (restrictHom c) ((basis (c.restrict L)) σ) = (basis c) (AlgEquiv.restrictScalars K σ)

The embedding sends each basis element to the basis element of the underlying automorphism.

@[simp]

theorem TauCeti.CrossedProduct.restrictHom_inc {K : Type u_1} {L : Type u_2} {E : Type u_3} [CommSemiring K] [CommSemiring L] [CommRing E] [Algebra K L] [Algebra K E] [Algebra L E] [IsScalarTower K L E] (c : TwoCocycle K E) (x : E) : (restrictHom c) ((inc (c.restrict L)) x) = (inc c) x

The embedding preserves the coefficient ring.

@[simp]

theorem TauCeti.CrossedProduct.repr_restrictHom {K : Type u_1} {L : Type u_2} {E : Type u_3} [CommSemiring K] [CommSemiring L] [CommRing E] [Algebra K L] [Algebra K E] [Algebra L E] [IsScalarTower K L E] (c : TwoCocycle K E) (a : CrossedProduct (c.restrict L)) : (basis c).repr ((restrictHom c) a) = Finsupp.mapDomain (AlgEquiv.restrictScalars K) ((basis (c.restrict L)).repr a)

Coordinates of the embedding are extended by zero along restriction of scalars.

theorem TauCeti.CrossedProduct.restrictHom_injective {K : Type u_1} {L : Type u_2} {E : Type u_3} [CommSemiring K] [CommSemiring L] [CommRing E] [Algebra K L] [Algebra K E] [Algebra L E] [IsScalarTower K L E] (c : TwoCocycle K E) : Function.Injective ⇑(restrictHom c)

Restriction of crossed products is injective.

theorem TauCeti.CrossedProduct.mem_range_restrictHom_iff {K : Type u_1} {L : Type u_2} {E : Type u_3} [CommSemiring K] [CommSemiring L] [CommRing E] [Algebra K L] [Algebra K E] [Algebra L E] [IsScalarTower K L E] (c : TwoCocycle K E) (a : CrossedProduct c) : a ∈ (restrictHom c).range ↔ ∀ σ ∉ Set.range (AlgEquiv.restrictScalars K), ((basis c).repr a) σ = 0

An element is in the restricted crossed product exactly when its coefficients vanish outside the automorphisms fixing L.

theorem TauCeti.CrossedProduct.range_restrictHom_eq_centralizer {K : Type u_1} {L : Type u_2} {E : Type u_3} [CommSemiring K] [CommSemiring L] [CommRing E] [Algebra K L] [Algebra K E] [Algebra L E] [IsScalarTower K L E] (c : TwoCocycle K E) [NoZeroDivisors E] : (restrictHom c).range = Subalgebra.centralizer K (Set.range fun (x : L) => (inc c) ((algebraMap L E) x))

The image of the restricted crossed product is the centralizer of the image of L under inc c ∘ algebraMap L E. This holds for any scalar tower with no zero divisors in E, without finiteness or Galois assumptions.

noncomputable def TauCeti.CrossedProduct.restrictAlgEquivCentralizer {K : Type u_1} {L : Type u_2} {E : Type u_3} [CommSemiring K] [CommSemiring L] [CommRing E] [Algebra K L] [Algebra K E] [Algebra L E] [IsScalarTower K L E] (c : TwoCocycle K E) [NoZeroDivisors E] : CrossedProduct (c.restrict L) ≃ₐ[K] ↥(Subalgebra.centralizer K (Set.range fun (x : L) => (inc c) ((algebraMap L E) x)))

The restricted crossed product is canonically equivalent as a K-algebra to the centralizer of the image of L under inc c ∘ algebraMap L E.

@[simp]

theorem TauCeti.CrossedProduct.coe_restrictAlgEquivCentralizer_apply {K : Type u_1} {L : Type u_2} {E : Type u_3} [CommSemiring K] [CommSemiring L] [CommRing E] [Algebra K L] [Algebra K E] [Algebra L E] [IsScalarTower K L E] (c : TwoCocycle K E) [NoZeroDivisors E] (a : CrossedProduct (c.restrict L)) : ↑((restrictAlgEquivCentralizer c) a) = (restrictHom c) a

The centralizer equivalence has the same underlying value as the restriction embedding.