Comodule algebras and Hopf–Galois extensions

Let H be an R-bialgebra. A (right) H-comodule algebra is an R-algebra A with a right H-comodule structure whose coaction ρ : A → A ⊗[R] H is a homomorphism of algebras. When H and A are commutative this is a right action X × G → X of the affine monoid scheme G = Spec H on the affine scheme X = Spec A, over Spec R; the regular comodule algebra H is the action of G on itself by right translation.

The coinvariants A^{co H} are the elements a with ρ a = a ⊗ 1, the functions on X which are invariant under G. They form a subalgebra of A. For the action of a closed subgroup on the ambient group by right translation, the analogous constructions are the coinvariants TauCeti.HopfIdeal.coinvariants of a Hopf ideal and its canonical map TauCeti.HopfIdeal.canonicalMap.

Let B be an algebra over which A is an algebra, acting by coinvariants. Geometrically q : X ⟶ Y = Spec B is a G-invariant morphism. The Galois map

β : A ⊗[B] A → A ⊗[R] H, a ⊗ a' ↦ (a ⊗ 1) ρ(a')

is the coordinate map of X × G ⟶ X ×_Y X, (x, g) ↦ (x, x g). When A is faithfully flat over B and β is bijective, A is an H-Galois extension of B: X ⟶ Y is a G-torsor for the faithfully flat topology, trivialised by its own base change X ×_Y X ≅ X × G.

The main result says that the base of a torsor is recovered as the invariant algebra: if A is faithfully flat over B and β is injective, then B maps isomorphically onto A^{co H} (TauCeti.ComoduleAlgebra.coinvariants_eq_range). The proof is faithfully flat descent: for a ∈ A^{co H}, both a ⊗ 1 and 1 ⊗ a are sent by β to a ⊗ 1, so they agree in A ⊗[B] A, and the equalizer of A ⇉ A ⊗[B] A is B. Consequently Spec A ⟶ Spec B is a categorical quotient in affine schemes: an invariant algebra map into A factors uniquely through B (TauCeti.ComoduleAlgebra.existsUnique_comp_eq).

For a commutative Hopf algebra H, the Galois map of the regular comodule algebra H over R is the tensor shear HopfAlgebra.tensorShearMulRight, which is bijective (TauCeti.ComoduleAlgebra.galoisMap_self_bijective). When H is moreover faithfully flat over R (for instance when R is a field), H is therefore an H-Galois extension of R: the trivial torsor G ⟶ Spec R.

Main definitions

• TauCeti.ComoduleAlgebra: a right comodule algebra over a bialgebra.
• TauCeti.ComoduleAlgebra.coactAlgHom: the coaction as an algebra homomorphism.
• TauCeti.ComoduleAlgebra.coinvariants: the subalgebra of coinvariants.
• TauCeti.ComoduleAlgebra.spanSubcomodule: the ideal generated by a set of coinvariants, as a subcomodule.
• TauCeti.ComoduleAlgebra.coactAlgHomOver: the coaction as a B-algebra homomorphism, for an algebra B acting by coinvariants.
• TauCeti.ComoduleAlgebra.galoisMap: the Galois map A ⊗[B] A → A ⊗[R] H.
• TauCeti.ComoduleAlgebra.coinvariantsEquiv: for a faithfully flat extension with injective Galois map, the algebra isomorphism B ≃ A^{co H}.

Main results

• TauCeti.ComoduleAlgebra.coinvariants_eq_range: if A is faithfully flat over B and the Galois map is injective, the coinvariants are exactly the image of B.
• TauCeti.ComoduleAlgebra.existsUnique_comp_eq: under the same hypotheses, every invariant algebra map into A factors uniquely through B.
• TauCeti.ComoduleAlgebra.galoisMap_self_bijective: the regular comodule algebra of a commutative Hopf algebra has bijective Galois map.

References

• S. Montgomery, Hopf Algebras and Their Actions on Rings, CBMS Regional Conference Series in Mathematics 82, AMS, 1993, §4.1 (comodule algebras and coinvariants) and §8.1 (Hopf–Galois extensions).
• H. F. Kreimer and M. Takeuchi, Hopf algebras and Galois extensions of an algebra, Indiana Univ. Math. J. 30 (1981), 675–692.
• M. Demazure and A. Grothendieck, Schémas en groupes (SGA 3), Exposé IV, §5 (torsors) and Exposé V, §4.

class TauCeti.ComoduleAlgebra (R : Type u) (H : Type v) (A : Type w) [CommSemiring R] [Semiring H] [Bialgebra R H] [Semiring A] [Algebra R A] extends TauCeti.Comodule R H A : Type (max v w)

A right comodule algebra over an R-bialgebra H: an R-algebra A with a right H-comodule structure whose coaction A → A ⊗[R] H is multiplicative and unital, so that it is a homomorphism of R-algebras. For commutative H and A it is an action of the affine monoid scheme Spec H on the affine scheme Spec A.

• coact : A →ₗ[R] TensorProduct R A H
• coassoc : ↑(TensorProduct.assoc R A H H) ∘ₗ LinearMap.rTensor H coact ∘ₗ coact = LinearMap.lTensor A CoalgebraStruct.comul ∘ₗ coact
• lTensor_counit_comp_coact : LinearMap.lTensor A CoalgebraStruct.counit ∘ₗ coact = (TensorProduct.mk R A R).flip 1
• coact_one : Comodule.coact 1 = 1

  The coaction is unital.

• coact_mul (a b : A) : Comodule.coact (a * b) = Comodule.coact a * Comodule.coact b

  The coaction is multiplicative.

noncomputable def TauCeti.ComoduleAlgebra.coactAlgHom (R : Type u) (H : Type v) (A : Type w) [CommSemiring R] [Semiring H] [Bialgebra R H] [Semiring A] [Algebra R A] [ComoduleAlgebra R H A] : A →ₐ[R] TensorProduct R A H

The coaction of a comodule algebra, as a homomorphism of R-algebras A →ₐ[R] A ⊗[R] H.

@[simp]

theorem TauCeti.ComoduleAlgebra.coactAlgHom_apply {R : Type u} {H : Type v} {A : Type w} [CommSemiring R] [Semiring H] [Bialgebra R H] [Semiring A] [Algebra R A] [ComoduleAlgebra R H A] (a : A) : (coactAlgHom R H A) a = Comodule.coact a

@[simp]

theorem TauCeti.ComoduleAlgebra.toLinearMap_coactAlgHom (R : Type u) (H : Type v) (A : Type w) [CommSemiring R] [Semiring H] [Bialgebra R H] [Semiring A] [Algebra R A] [ComoduleAlgebra R H A] : (coactAlgHom R H A).toLinearMap = Comodule.coact

@[simp]

theorem TauCeti.ComoduleAlgebra.coact_algebraMap (R : Type u) (H : Type v) (A : Type w) [CommSemiring R] [Semiring H] [Bialgebra R H] [Semiring A] [Algebra R A] [ComoduleAlgebra R H A] (r : R) : Comodule.coact ((algebraMap R A) r) = (algebraMap R A) r ⊗ₜ[R] 1

The coaction sends a scalar r to r ⊗ 1.

noncomputable def TauCeti.ComoduleAlgebra.coinvariants (R : Type u) (H : Type v) (A : Type w) [CommSemiring R] [Semiring H] [Bialgebra R H] [Semiring A] [Algebra R A] [ComoduleAlgebra R H A] : Subalgebra R A

The coinvariants A^{co H} of a comodule algebra: the subalgebra of elements a with coact a = a ⊗ 1, the equalizer of the coaction and a ↦ a ⊗ 1. These are the functions on Spec A invariant under the action of Spec H. Its underlying set is the fixed subcomodule TauCeti.Comodule.fixedSubcomodule (TauCeti.ComoduleAlgebra.coe_coinvariants).

@[simp]

theorem TauCeti.ComoduleAlgebra.mem_coinvariants {R : Type u} {H : Type v} {A : Type w} [CommSemiring R] [Semiring H] [Bialgebra R H] [Semiring A] [Algebra R A] [ComoduleAlgebra R H A] {a : A} : a ∈ coinvariants R H A ↔ Comodule.coact a = a ⊗ₜ[R] 1

theorem TauCeti.ComoduleAlgebra.coe_coinvariants {R : Type u} {H : Type v} {A : Type w} [CommSemiring R] [Semiring H] [Bialgebra R H] [Semiring A] [Algebra R A] [ComoduleAlgebra R H A] : ↑(coinvariants R H A) = ↑(Comodule.fixedSubcomodule R H A)

noncomputable def TauCeti.ComoduleAlgebra.mulLeftHom {R : Type u} {H : Type v} {A : Type w} [CommSemiring R] [Semiring H] [Bialgebra R H] [Semiring A] [Algebra R A] [ComoduleAlgebra R H A] (a : A) (ha : a ∈ coinvariants R H A) : Comodule.Hom R H A A

Left multiplication by an invariant element of a comodule algebra, as a comodule endomorphism.

@[simp]

theorem TauCeti.ComoduleAlgebra.mulLeftHom_apply {R : Type u} {H : Type v} {A : Type w} [CommSemiring R] [Semiring H] [Bialgebra R H] [Semiring A] [Algebra R A] [ComoduleAlgebra R H A] (a : A) (ha : a ∈ coinvariants R H A) (b : A) : (mulLeftHom a ha) b = a * b

theorem TauCeti.ComoduleAlgebra.coact_mem_map_includeLeft_span {R : Type u} {H : Type v} {A : Type w} [CommSemiring R] [Semiring H] [Bialgebra R H] [Semiring A] [Algebra R A] [ComoduleAlgebra R H A] {S : Set A} (hS : S ⊆ ↑(coinvariants R H A)) {a : A} (ha : a ∈ Ideal.span S) : Comodule.coact a ∈ Ideal.map Algebra.TensorProduct.includeLeft (Ideal.span S)

An ideal generated by coinvariants is stable under the coaction. The coaction carries the ideal generated by a set of coinvariants into the ideal it generates in A ⊗[R] H: the closed subscheme cut out by invariant functions is stable under the action.

noncomputable def TauCeti.ComoduleAlgebra.spanSubcomodule {R : Type u} {H : Type v} {A : Type w} [CommSemiring R] [Semiring H] [Bialgebra R H] [Semiring A] [Algebra R A] [ComoduleAlgebra R H A] {S : Set A} (hS : S ⊆ ↑(coinvariants R H A)) : Subcomodule R H A

The ideal generated by a set of coinvariants, as a subcomodule: the action restricts to it, and so descends to the quotient by it.

@[simp]

theorem TauCeti.ComoduleAlgebra.mem_spanSubcomodule {R : Type u} {H : Type v} {A : Type w} [CommSemiring R] [Semiring H] [Bialgebra R H] [Semiring A] [Algebra R A] [ComoduleAlgebra R H A] {S : Set A} (hS : S ⊆ ↑(coinvariants R H A)) {a : A} : a ∈ spanSubcomodule hS ↔ a ∈ Ideal.span S

Membership in the subcomodule of an ideal generated by coinvariants is membership in the ideal.

theorem TauCeti.ComoduleAlgebra.range_le_coinvariants_iff {R : Type u} {H : Type v} {A : Type w} [CommSemiring R] [Semiring H] [Bialgebra R H] [Semiring A] [Algebra R A] [ComoduleAlgebra R H A] {C : Type x} [Semiring C] [Algebra R C] (φ : C →ₐ[R] A) : φ.range ≤ coinvariants R H A ↔ (coactAlgHom R H A).comp φ = Algebra.TensorProduct.includeLeft.comp φ

An algebra map φ : C → A lands in the coinvariants exactly when it is invariant: composing it with the coaction or with a ↦ a ⊗ 1 gives the same map.

@[instance_reducible]

instance TauCeti.ComoduleAlgebra.instSelf (R : Type u) (H : Type v) [CommSemiring R] [Semiring H] [Bialgebra R H] : ComoduleAlgebra R H H

The regular comodule algebra: a bialgebra is a comodule algebra over itself, with coaction the comultiplication. It is the action of a monoid scheme on itself by right translation.

@[simp]

theorem TauCeti.ComoduleAlgebra.coactAlgHom_self {R : Type u} {H : Type v} [CommSemiring R] [Semiring H] [Bialgebra R H] : coactAlgHom R H H = Bialgebra.comulAlgHom R H

The Galois map

noncomputable def TauCeti.ComoduleAlgebra.coactAlgHomOver {R : Type u} {H : Type v} {A : Type w} [CommSemiring R] [Semiring H] [Bialgebra R H] [CommSemiring A] [Algebra R A] [ComoduleAlgebra R H A] (B : Type x) [CommSemiring B] [Algebra R B] [Algebra B A] [IsScalarTower R B A] (hB : ∀ (b : B), (algebraMap B A) b ∈ coinvariants R H A) : A →ₐ[B] TensorProduct R A H

The coaction, regarded as a B-algebra homomorphism when B acts on A by coinvariants.

@[simp]

theorem TauCeti.ComoduleAlgebra.coactAlgHomOver_apply {R : Type u} {H : Type v} {A : Type w} [CommSemiring R] [Semiring H] [Bialgebra R H] [CommSemiring A] [Algebra R A] [ComoduleAlgebra R H A] (B : Type x) [CommSemiring B] [Algebra R B] [Algebra B A] [IsScalarTower R B A] (hB : ∀ (b : B), (algebraMap B A) b ∈ coinvariants R H A) (a : A) : (coactAlgHomOver B hB) a = Comodule.coact a

noncomputable def TauCeti.ComoduleAlgebra.galoisMap {R : Type u} {H : Type v} {A : Type w} [CommSemiring R] [Semiring H] [Bialgebra R H] [CommSemiring A] [Algebra R A] [ComoduleAlgebra R H A] (B : Type x) [CommSemiring B] [Algebra R B] [Algebra B A] [IsScalarTower R B A] (hB : ∀ (b : B), (algebraMap B A) b ∈ coinvariants R H A) : TensorProduct B A A →ₐ[A] TensorProduct R A H

The Galois map A ⊗[B] A → A ⊗[R] H, a ⊗ a' ↦ (a ⊗ 1) coact(a'), of a comodule algebra A over an algebra B acting by coinvariants. It is the coordinate map of (x, g) ↦ (x, x g) : Spec A × Spec H ⟶ Spec A ×_{Spec B} Spec A, and it is linear over the first copy of A.

@[simp]

theorem TauCeti.ComoduleAlgebra.galoisMap_tmul {R : Type u} {H : Type v} {A : Type w} [CommSemiring R] [Semiring H] [Bialgebra R H] [CommSemiring A] [Algebra R A] [ComoduleAlgebra R H A] {B : Type x} [CommSemiring B] [Algebra R B] [Algebra B A] [IsScalarTower R B A] (hB : ∀ (b : B), (algebraMap B A) b ∈ coinvariants R H A) (a a' : A) : (galoisMap B hB) (a ⊗ₜ[B] a') = a ⊗ₜ[R] 1 * Comodule.coact a'

theorem TauCeti.ComoduleAlgebra.galoisMap_comp_includeLeft {R : Type u} {H : Type v} {A : Type w} [CommSemiring R] [Semiring H] [Bialgebra R H] [CommSemiring A] [Algebra R A] [ComoduleAlgebra R H A] {B : Type x} [CommSemiring B] [Algebra R B] [Algebra B A] [IsScalarTower R B A] (hB : ∀ (b : B), (algebraMap B A) b ∈ coinvariants R H A) : (AlgHom.restrictScalars R (galoisMap B hB)).comp Algebra.TensorProduct.includeLeft = Algebra.TensorProduct.includeLeft

The Galois map sends a ⊗ 1 to a ⊗ 1: it restricts to a ↦ a ⊗ 1 on the first factor.

theorem TauCeti.ComoduleAlgebra.galoisMap_comp_includeRight {R : Type u} {H : Type v} {A : Type w} [CommSemiring R] [Semiring H] [Bialgebra R H] [CommSemiring A] [Algebra R A] [ComoduleAlgebra R H A] {B : Type x} [CommSemiring B] [Algebra R B] [Algebra B A] [IsScalarTower R B A] (hB : ∀ (b : B), (algebraMap B A) b ∈ coinvariants R H A) : (AlgHom.restrictScalars R (galoisMap B hB)).comp (AlgHom.restrictScalars R Algebra.TensorProduct.includeRight) = coactAlgHom R H A

The Galois map restricts to the coaction on the second factor.

The coinvariants of a faithfully flat Galois extension

theorem TauCeti.ComoduleAlgebra.coinvariants_eq_range {R : Type u} {H : Type v} {A : Type w} [CommSemiring R] [Semiring H] [Bialgebra R H] [CommRing A] [Algebra R A] [ComoduleAlgebra R H A] {B : Type x} [CommRing B] [Algebra R B] [Algebra B A] [IsScalarTower R B A] [Module.FaithfullyFlat B A] (hB : ∀ (b : B), (algebraMap B A) b ∈ coinvariants R H A) (hinj : Function.Injective ⇑(galoisMap B hB)) : coinvariants R H A = (IsScalarTower.toAlgHom R B A).range

The base of a torsor is its invariant algebra. Let A be a comodule algebra which is faithfully flat over an algebra B acting by coinvariants. If the Galois map A ⊗[B] A → A ⊗[R] H is injective, in particular if A is an H-Galois extension of B, then the coinvariants of A are exactly the image of B.

noncomputable def TauCeti.ComoduleAlgebra.coinvariantsEquiv {R : Type u} {H : Type v} {A : Type w} [CommSemiring R] [Semiring H] [Bialgebra R H] [CommRing A] [Algebra R A] [ComoduleAlgebra R H A] {B : Type x} [CommRing B] [Algebra R B] [Algebra B A] [IsScalarTower R B A] [Module.FaithfullyFlat B A] (hB : ∀ (b : B), (algebraMap B A) b ∈ coinvariants R H A) (hinj : Function.Injective ⇑(galoisMap B hB)) : B ≃ₐ[R] ↥(coinvariants R H A)

For a faithfully flat comodule algebra over B with injective Galois map, the isomorphism B ≃ A^{co H} induced by the algebra map B → A.

@[simp]

theorem TauCeti.ComoduleAlgebra.coe_coinvariantsEquiv_apply {R : Type u} {H : Type v} {A : Type w} [CommSemiring R] [Semiring H] [Bialgebra R H] [CommRing A] [Algebra R A] [ComoduleAlgebra R H A] {B : Type x} [CommRing B] [Algebra R B] [Algebra B A] [IsScalarTower R B A] [Module.FaithfullyFlat B A] (hB : ∀ (b : B), (algebraMap B A) b ∈ coinvariants R H A) (hinj : Function.Injective ⇑(galoisMap B hB)) (b : B) : ↑((coinvariantsEquiv hB hinj) b) = (algebraMap B A) b

@[simp]

theorem TauCeti.ComoduleAlgebra.algebraMap_coinvariantsEquiv_symm_apply {R : Type u} {H : Type v} {A : Type w} [CommSemiring R] [Semiring H] [Bialgebra R H] [CommRing A] [Algebra R A] [ComoduleAlgebra R H A] {B : Type x} [CommRing B] [Algebra R B] [Algebra B A] [IsScalarTower R B A] [Module.FaithfullyFlat B A] (hB : ∀ (b : B), (algebraMap B A) b ∈ coinvariants R H A) (hinj : Function.Injective ⇑(galoisMap B hB)) (a : ↥(coinvariants R H A)) : (algebraMap B A) ((coinvariantsEquiv hB hinj).symm a) = ↑a

theorem TauCeti.ComoduleAlgebra.existsUnique_comp_eq {R : Type u} {H : Type v} {A : Type w} [CommSemiring R] [Semiring H] [Bialgebra R H] [CommRing A] [Algebra R A] [ComoduleAlgebra R H A] {B : Type x} [CommRing B] [Algebra R B] [Algebra B A] [IsScalarTower R B A] [Module.FaithfullyFlat B A] (hB : ∀ (b : B), (algebraMap B A) b ∈ coinvariants R H A) (hinj : Function.Injective ⇑(galoisMap B hB)) {C : Type u_1} [Semiring C] [Algebra R C] (φ : C →ₐ[R] A) (hφ : (coactAlgHom R H A).comp φ = Algebra.TensorProduct.includeLeft.comp φ) : ∃! ψ : C →ₐ[R] B, (IsScalarTower.toAlgHom R B A).comp ψ = φ

The categorical quotient in affine schemes. Let A be a comodule algebra which is faithfully flat over B, acting by coinvariants, with injective Galois map. An algebra map φ : C → A which is invariant, in the sense that coact ∘ φ = (· ⊗ 1) ∘ φ, factors uniquely through B.

The regular comodule algebra of a Hopf algebra

theorem TauCeti.ComoduleAlgebra.galoisMap_self_bijective {R : Type u} {H : Type v} [CommSemiring R] [CommSemiring H] [HopfAlgebra R H] : Function.Bijective ⇑(galoisMap R ⋯)

The trivial torsor. For a commutative Hopf algebra H, the Galois map of the regular comodule algebra H over R is the tensor shear a ⊗ b ↦ (a ⊗ 1) Δ b, which is bijective. When H is faithfully flat over R, the action of Spec H on itself by right translation therefore makes it a torsor over Spec R.