Scalar towers on the quotient of a presentation

The module relations.Quotient presented by relations : Module.Relations A is the quotient of the free module relations.G →₀ A by the span of the relations. Mathlib equips it with its A-module structure only. When A is itself an algebra over a ring S — a group ring R[G] over R, say — the free module is an S-module compatibly with its A-module structure, and so is the quotient. This file records that S-module structure and the scalar tower, which is what lets a presented A-module be tensored over S, as in the base change of a module over an integral group ring ℤ_p[G] to ℚ_p.

Main results

• Module.Relations.Quotient.module': the S-module structure on relations.Quotient for a ring S acting on A compatibly with multiplication.
• Module.Relations.Quotient.isScalarTower: S, A and relations.Quotient form a scalar tower.

@[instance_reducible]

noncomputable instance Module.Relations.Quotient.module' {A : Type u_1} [Ring A] (relations : Relations A) (S : Type u_2) [Semiring S] [Module S A] [IsScalarTower S A A] : Module S relations.Quotient

The quotient of a presentation of an A-module is a module over any ring S acting on A compatibly with multiplication, by the S-module structure of the quotient of the free A-module relations.G →₀ A.

Equations

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

instance Module.Relations.Quotient.isScalarTower {A : Type u_1} [Ring A] (relations : Relations A) (S : Type u_2) [Semiring S] [Module S A] [IsScalarTower S A A] : IsScalarTower S A relations.Quotient

The S- and A-module structures on the quotient of a presentation form a scalar tower.