The exterior algebra of a comodule

Let H be a commutative bialgebra over a commutative ring R and M a right H-comodule. The exterior algebra ExteriorAlgebra R M is again a right H-comodule, with the coaction determined multiplicatively by that of M: in Sweedler notation m ↦ m₍₀₎ ⊗ m₍₁₎,

ι m₁ * ⋯ * ι mₙ ↦ ∏ᵢ (ι mᵢ₍₀₎ ⊗ mᵢ₍₁₎).

Since H is commutative, ExteriorAlgebra R M ⊗[R] H is an algebra in which the image of the coaction of M still squares to zero, so the coaction extends to an algebra homomorphism exteriorAlgebraCoact : ExteriorAlgebra R M →ₐ[R] ExteriorAlgebra R M ⊗[R] H; the comodule laws then hold because they hold on generators. This coaction preserves the exterior grading, so every exterior power ⋀[R]^n M is a subcomodule. The points of H act on the scalar extension of the exterior algebra by algebra endomorphisms, compatibly with their action on M through the comodule morphism Hom.exteriorAlgebraι (by baseChange_comp_endOfPoint).

For an affine group G = Spec H with a representation M, this is the representation of G on ⋀ M and its homogeneous pieces. Chevalley's theorem realizing a closed subgroup as the stabilizer of a line uses the line spanned by the top exterior product of a subrepresentation.

Following Comodule.tensor, Comodule.exteriorAlgebra is not a global instance.

Main declarations

• TauCeti.Comodule.exteriorAlgebraCoact: the coaction of the exterior algebra, as an algebra homomorphism.
• TauCeti.Comodule.exteriorAlgebra: the right H-comodule structure on ExteriorAlgebra R M.
• TauCeti.Comodule.Hom.exteriorAlgebraι and TauCeti.Comodule.Hom.exteriorAlgebraMap: the inclusion of generators and the functoriality of the exterior algebra, as comodule morphisms.
• TauCeti.Comodule.exteriorAlgebraCoact_mem_decomposeTensor: the coaction preserves degrees.
• TauCeti.Comodule.exteriorPowerSubcomodule: the exterior power ⋀[R]^n M as a subcomodule.
• TauCeti.Comodule.exteriorAlgebraEndOfPoint: the action of a point on the scalar extension of the exterior algebra, as an algebra homomorphism.

References

• W. C. Waterhouse, Introduction to Affine Group Schemes, §3.2.
• J. S. Milne, Algebraic Groups (2017), Theorem 4.27 and Lemma 4.28.

noncomputable def TauCeti.Comodule.exteriorAlgebraCoact (R : Type u_1) (H : Type u_2) (M : Type u_3) [CommRing R] [CommSemiring H] [Bialgebra R H] [AddCommGroup M] [Module R M] [Comodule R H M] : ExteriorAlgebra R M →ₐ[R] TensorProduct R (ExteriorAlgebra R M) H

The coaction of the exterior algebra of a comodule, as an algebra homomorphism: it sends a generator ι m to ι m₍₀₎ ⊗ m₍₁₎, the coaction of m followed by the inclusion of generators.

Equations

• TauCeti.Comodule.exteriorAlgebraCoact R H M = (ExteriorAlgebra.lift R) ⟨LinearMap.rTensor H (ExteriorAlgebra.ι R) ∘ₗ TauCeti.Comodule.coact, ⋯⟩

@[simp]

theorem TauCeti.Comodule.exteriorAlgebraCoact_ι {R : Type u_1} {H : Type u_2} {M : Type u_3} [CommRing R] [CommSemiring H] [Bialgebra R H] [AddCommGroup M] [Module R M] [Comodule R H M] (m : M) : (exteriorAlgebraCoact R H M) ((ExteriorAlgebra.ι R) m) = (LinearMap.rTensor H (ExteriorAlgebra.ι R)) (coact m)

theorem TauCeti.Comodule.exteriorAlgebraCoact_coassoc {R : Type u_1} {H : Type u_2} {M : Type u_3} [CommRing R] [CommSemiring H] [Bialgebra R H] [AddCommGroup M] [Module R M] [Comodule R H M] : ↑(TensorProduct.assoc R (ExteriorAlgebra R M) H H) ∘ₗ LinearMap.rTensor H (exteriorAlgebraCoact R H M).toLinearMap ∘ₗ (exteriorAlgebraCoact R H M).toLinearMap = LinearMap.lTensor (ExteriorAlgebra R M) CoalgebraStruct.comul ∘ₗ (exteriorAlgebraCoact R H M).toLinearMap

Coassociativity of the coaction of the exterior algebra.

theorem TauCeti.Comodule.exteriorAlgebraCoact_counit {R : Type u_1} {H : Type u_2} {M : Type u_3} [CommRing R] [CommSemiring H] [Bialgebra R H] [AddCommGroup M] [Module R M] [Comodule R H M] : LinearMap.lTensor (ExteriorAlgebra R M) CoalgebraStruct.counit ∘ₗ (exteriorAlgebraCoact R H M).toLinearMap = (TensorProduct.mk R (ExteriorAlgebra R M) R).flip 1

The counit law for the coaction of the exterior algebra.

@[implicit_reducible]

noncomputable def TauCeti.Comodule.exteriorAlgebra (R : Type u_1) (H : Type u_2) (M : Type u_3) [CommRing R] [CommSemiring H] [Bialgebra R H] [AddCommGroup M] [Module R M] [Comodule R H M] : Comodule R H (ExteriorAlgebra R M)

The exterior algebra of a right comodule over a commutative bialgebra, with the multiplicative coaction exteriorAlgebraCoact.

Following Comodule.tensor, this is deliberately not a global instance. Select it explicitly, or register it as a local instance.

Equations

• TauCeti.Comodule.exteriorAlgebra R H M = { coact := (TauCeti.Comodule.exteriorAlgebraCoact R H M).toLinearMap, coassoc := ⋯, lTensor_counit_comp_coact := ⋯ }

@[simp]

theorem TauCeti.Comodule.exteriorAlgebra_coact {R : Type u_1} {H : Type u_2} {M : Type u_3} [CommRing R] [CommSemiring H] [Bialgebra R H] [AddCommGroup M] [Module R M] [Comodule R H M] : coact = (exteriorAlgebraCoact R H M).toLinearMap

The coaction of the exterior-algebra comodule is exteriorAlgebraCoact.

noncomputable def TauCeti.Comodule.Hom.exteriorAlgebraι (R : Type u_1) (H : Type u_2) (M : Type u_3) [CommRing R] [CommSemiring H] [Bialgebra R H] [AddCommGroup M] [Module R M] [Comodule R H M] : Hom R H M (ExteriorAlgebra R M)

The inclusion ι : M → ExteriorAlgebra R M of generators, as a comodule morphism.

Equations

• TauCeti.Comodule.Hom.exteriorAlgebraι R H M = { toLinearMap := ExteriorAlgebra.ι R, map_coact := ⋯ }

@[simp]

theorem TauCeti.Comodule.Hom.exteriorAlgebraι_toLinearMap {R : Type u_1} {H : Type u_2} {M : Type u_3} [CommRing R] [CommSemiring H] [Bialgebra R H] [AddCommGroup M] [Module R M] [Comodule R H M] : (exteriorAlgebraι R H M).toLinearMap = ExteriorAlgebra.ι R

@[simp]

theorem TauCeti.Comodule.Hom.exteriorAlgebraι_apply {R : Type u_1} {H : Type u_2} {M : Type u_3} [CommRing R] [CommSemiring H] [Bialgebra R H] [AddCommGroup M] [Module R M] [Comodule R H M] (m : M) : (exteriorAlgebraι R H M) m = (ExteriorAlgebra.ι R) m

noncomputable def TauCeti.Comodule.Hom.exteriorAlgebraMap {R : Type u_1} {H : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [CommSemiring H] [Bialgebra R H] [AddCommGroup M] [Module R M] [Comodule R H M] [AddCommGroup N] [Module R N] [Comodule R H N] (f : Hom R H M N) : Hom R H (ExteriorAlgebra R M) (ExteriorAlgebra R N)

The map of exterior algebras induced by a comodule morphism, as a comodule morphism.

Equations

• f.exteriorAlgebraMap = { toLinearMap := (ExteriorAlgebra.map f.toLinearMap).toLinearMap, map_coact := ⋯ }

@[simp]

theorem TauCeti.Comodule.Hom.exteriorAlgebraMap_toLinearMap {R : Type u_1} {H : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [CommSemiring H] [Bialgebra R H] [AddCommGroup M] [Module R M] [Comodule R H M] [AddCommGroup N] [Module R N] [Comodule R H N] (f : Hom R H M N) : f.exteriorAlgebraMap.toLinearMap = (ExteriorAlgebra.map f.toLinearMap).toLinearMap

@[simp]

theorem TauCeti.Comodule.Hom.exteriorAlgebraMap_apply {R : Type u_1} {H : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [CommSemiring H] [Bialgebra R H] [AddCommGroup M] [Module R M] [Comodule R H M] [AddCommGroup N] [Module R N] [Comodule R H N] (f : Hom R H M N) (x : ExteriorAlgebra R M) : f.exteriorAlgebraMap x = (ExteriorAlgebra.map f.toLinearMap) x

theorem TauCeti.Comodule.Hom.exteriorAlgebraMap_id {R : Type u_1} {H : Type u_2} {M : Type u_3} [CommRing R] [CommSemiring H] [Bialgebra R H] [AddCommGroup M] [Module R M] [Comodule R H M] : (id R H M).exteriorAlgebraMap = id R H (ExteriorAlgebra R M)

The exterior-algebra functor on comodules preserves identities.

theorem TauCeti.Comodule.Hom.exteriorAlgebraMap_comp {R : Type u_1} {H : Type u_2} {M : Type u_3} {N : Type u_4} {P : Type u_5} [CommRing R] [CommSemiring H] [Bialgebra R H] [AddCommGroup M] [Module R M] [Comodule R H M] [AddCommGroup N] [Module R N] [Comodule R H N] [AddCommGroup P] [Module R P] [Comodule R H P] (g : Hom R H N P) (f : Hom R H M N) : (g.comp f).exteriorAlgebraMap = g.exteriorAlgebraMap.comp f.exteriorAlgebraMap

The exterior-algebra functor on comodules preserves composition.

@[simp]

theorem TauCeti.Comodule.Hom.exteriorAlgebraMap_comp_exteriorAlgebraι {R : Type u_1} {H : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [CommSemiring H] [Bialgebra R H] [AddCommGroup M] [Module R M] [Comodule R H M] [AddCommGroup N] [Module R N] [Comodule R H N] (f : Hom R H M N) : f.exteriorAlgebraMap.comp (exteriorAlgebraι R H M) = (exteriorAlgebraι R H N).comp f

The exterior-algebra functor is compatible with the inclusion of generators.

theorem TauCeti.Comodule.exteriorAlgebraCoact_mem_decomposeTensor {R : Type u_1} {H : Type u_2} {M : Type u_3} [CommRing R] [CommSemiring H] [Bialgebra R H] [AddCommGroup M] [Module R M] [Comodule R H M] {n : ℕ} {x : ExteriorAlgebra R M} (hx : x ∈ ⋀[R]^n M) : (exteriorAlgebraCoact R H M) x ∈ DirectSum.decomposeTensor (fun (i : ℕ) => ⋀[R]^i M) H n

The coaction of the exterior algebra preserves the exterior grading: it maps ⋀[R]^n M into the image of ⋀[R]^n M ⊗[R] H.

noncomputable def TauCeti.Comodule.exteriorPowerSubcomodule (R : Type u_1) (H : Type u_2) (M : Type u_3) [CommRing R] [CommSemiring H] [Bialgebra R H] [AddCommGroup M] [Module R M] [Comodule R H M] (n : ℕ) : Subcomodule R H (ExteriorAlgebra R M)

The exterior power ⋀[R]^n M as a subcomodule of the exterior algebra.

Equations

• TauCeti.Comodule.exteriorPowerSubcomodule R H M n = TauCeti.Subcomodule.ofSubmodule (⋀[R]^n M) ⋯

@[simp]

theorem TauCeti.Comodule.exteriorPowerSubcomodule_toSubmodule {R : Type u_1} {H : Type u_2} {M : Type u_3} [CommRing R] [CommSemiring H] [Bialgebra R H] [AddCommGroup M] [Module R M] [Comodule R H M] (n : ℕ) : (exteriorPowerSubcomodule R H M n).toSubmodule = ⋀[R]^n M

@[simp]

theorem TauCeti.Comodule.mem_exteriorPowerSubcomodule {R : Type u_1} {H : Type u_2} {M : Type u_3} [CommRing R] [CommSemiring H] [Bialgebra R H] [AddCommGroup M] [Module R M] [Comodule R H M] {n : ℕ} {x : ExteriorAlgebra R M} : x ∈ exteriorPowerSubcomodule R H M n ↔ x ∈ ⋀[R]^n M

noncomputable def TauCeti.Comodule.exteriorAlgebraEndOfPoint {R : Type u_1} {H : Type u_2} {M : Type u_3} [CommRing R] [CommSemiring H] [Bialgebra R H] [AddCommGroup M] [Module R M] [Comodule R H M] {A : Type u_6} [CommSemiring A] [Algebra R A] (g : H →ₐ[R] A) : TensorProduct R A (ExteriorAlgebra R M) →ₐ[A] TensorProduct R A (ExteriorAlgebra R M)

The action of an A-point g of H on the scalar extension A ⊗[R] ExteriorAlgebra R M, as an A-algebra homomorphism. Its underlying linear map is endOfPoint (exteriorAlgebraEndOfPoint_toLinearMap), so points act on the exterior algebra multiplicatively.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.Comodule.exteriorAlgebraEndOfPoint_toLinearMap {R : Type u_1} {H : Type u_2} {M : Type u_3} [CommRing R] [CommSemiring H] [Bialgebra R H] [AddCommGroup M] [Module R M] [Comodule R H M] {A : Type u_6} [CommSemiring A] [Algebra R A] (g : H →ₐ[R] A) : (exteriorAlgebraEndOfPoint g).toLinearMap = endOfPoint (ExteriorAlgebra R M) g

The algebra homomorphism exteriorAlgebraEndOfPoint g is the action endOfPoint of the point g on the exterior-algebra comodule.

@[simp]

theorem TauCeti.Comodule.exteriorAlgebraEndOfPoint_apply {R : Type u_1} {H : Type u_2} {M : Type u_3} [CommRing R] [CommSemiring H] [Bialgebra R H] [AddCommGroup M] [Module R M] [Comodule R H M] {A : Type u_6} [CommSemiring A] [Algebra R A] (g : H →ₐ[R] A) (x : TensorProduct R A (ExteriorAlgebra R M)) : (exteriorAlgebraEndOfPoint g) x = (endOfPoint (ExteriorAlgebra R M) g) x

theorem TauCeti.Comodule.endOfPoint_exteriorAlgebra_one {R : Type u_1} {H : Type u_2} {M : Type u_3} [CommRing R] [CommSemiring H] [Bialgebra R H] [AddCommGroup M] [Module R M] [Comodule R H M] {A : Type u_6} [CommSemiring A] [Algebra R A] (g : H →ₐ[R] A) : (endOfPoint (ExteriorAlgebra R M) g) 1 = 1

Points fix the unit of the scalar extension of the exterior algebra.

theorem TauCeti.Comodule.endOfPoint_exteriorAlgebra_mul {R : Type u_1} {H : Type u_2} {M : Type u_3} [CommRing R] [CommSemiring H] [Bialgebra R H] [AddCommGroup M] [Module R M] [Comodule R H M] {A : Type u_6} [CommSemiring A] [Algebra R A] (g : H →ₐ[R] A) (x y : TensorProduct R A (ExteriorAlgebra R M)) : (endOfPoint (ExteriorAlgebra R M) g) (x * y) = (endOfPoint (ExteriorAlgebra R M) g) x * (endOfPoint (ExteriorAlgebra R M) g) y

Points act on the scalar extension of the exterior algebra multiplicatively.