Semilinear functoriality of symmetric algebras

Let φ : R →+* S be a morphism of commutative semirings, M an R-module and N an S-module. A φ-semilinear map f : M →ₛₗ[φ] N induces a ring homomorphism SymmetricAlgebra R M →+* SymmetricAlgebra S N, which is φ on scalars and sends the generator of m to the generator of f m. It preserves the homogeneous pieces.

This is the change-of-rings version of SymmetricAlgebra.map. For a presheaf of modules over a presheaf of rings, the restriction maps are semilinear over the restriction maps of the rings, so this construction is what makes the sectionwise symmetric algebras and symmetric powers of a presheaf of modules into presheaves.

Main declarations

• SymmetricAlgebra.mapₛₗ: the ring homomorphism induced by a semilinear map;
• SymmetricAlgebra.mapₛₗ_comp_mapₛₗ and SymmetricAlgebra.mapₛₗ_eq_id: functoriality, with the ring homomorphisms and semilinear maps related by pointwise equations, so that they apply to maps that only agree propositionally (as for the restriction maps of a presheaf);
• TauCeti.SymmetricAlgebra.mapₛₗ_mem_homogeneousSubmodule and TauCeti.SymmetricAlgebra.map_mem_homogeneousSubmodule: the induced maps preserve degrees;
• TauCeti.SymmetricAlgebra.homogeneousSubmoduleMapₛₗ: the induced semilinear map between homogeneous pieces of the same degree.

noncomputable def SymmetricAlgebra.mapₛₗ {R : Type u₁} {S : Type u₂} [CommSemiring R] [CommSemiring S] {M : Type v₁} {N : Type v₂} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module S N] {φ : R →+* S} (f : M →ₛₗ[φ] N) : SymmetricAlgebra R M →+* SymmetricAlgebra S N

The ring homomorphism between symmetric algebras induced by a semilinear map f : M →ₛₗ[φ] N: it is φ on scalars and sends the generator of m to the generator of f m.

Equations

• SymmetricAlgebra.mapₛₗ f = (SymmetricAlgebra.lift { toFun := fun (m : M) => (SymmetricAlgebra.ι S N) (f m), map_add' := ⋯, map_smul' := ⋯ }).toRingHom

@[simp]

theorem SymmetricAlgebra.mapₛₗ_algebraMap {R : Type u₁} {S : Type u₂} [CommSemiring R] [CommSemiring S] {M : Type v₁} {N : Type v₂} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module S N] {φ : R →+* S} (f : M →ₛₗ[φ] N) (r : R) : (mapₛₗ f) ((algebraMap R (SymmetricAlgebra R M)) r) = (algebraMap S (SymmetricAlgebra S N)) (φ r)

The map induced by a semilinear map is the original ring homomorphism on scalars.

@[simp]

theorem SymmetricAlgebra.mapₛₗ_ι {R : Type u₁} {S : Type u₂} [CommSemiring R] [CommSemiring S] {M : Type v₁} {N : Type v₂} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module S N] {φ : R →+* S} (f : M →ₛₗ[φ] N) (m : M) : (mapₛₗ f) ((ι R M) m) = (ι S N) (f m)

The map induced by a semilinear map sends a generator to the generator of its image.

theorem SymmetricAlgebra.mapₛₗ_smul {R : Type u₁} {S : Type u₂} [CommSemiring R] [CommSemiring S] {M : Type v₁} {N : Type v₂} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module S N] {φ : R →+* S} (f : M →ₛₗ[φ] N) (r : R) (x : SymmetricAlgebra R M) : (mapₛₗ f) (r • x) = φ r • (mapₛₗ f) x

The map induced by a semilinear map is semilinear.

theorem SymmetricAlgebra.mapₛₗ_eq_map {R : Type u₁} [CommSemiring R] {M : Type v₁} [AddCommMonoid M] [Module R M] {N' : Type u_1} [AddCommMonoid N'] [Module R N'] (f : M →ₗ[R] N') : mapₛₗ f = ↑(map R f)

For a linear map, the induced ring homomorphism underlies SymmetricAlgebra.map.

theorem SymmetricAlgebra.mapₛₗ_eq_id {R : Type u₁} [CommSemiring R] {M : Type v₁} [AddCommMonoid M] [Module R M] {φ : R →+* R} (hφ : ∀ (r : R), φ r = r) {f : M →ₛₗ[φ] M} (hf : ∀ (m : M), f m = m) : mapₛₗ f = RingHom.id (SymmetricAlgebra R M)

The map induced by a semilinear map which is the identity on elements, over a ring homomorphism which is the identity, is the identity.

theorem SymmetricAlgebra.mapₛₗ_comp_mapₛₗ {R : Type u₁} {S : Type u₂} {T : Type u₃} [CommSemiring R] [CommSemiring S] [CommSemiring T] {M : Type v₁} {N : Type v₂} {P : Type v₃} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module S N] [AddCommMonoid P] [Module T P] {φ : R →+* S} {ψ : S →+* T} {χ : R →+* T} (f : M →ₛₗ[φ] N) (g : N →ₛₗ[ψ] P) (h : M →ₛₗ[χ] P) (hχ : ∀ (r : R), ψ (φ r) = χ r) (hh : ∀ (m : M), g (f m) = h m) : (mapₛₗ g).comp (mapₛₗ f) = mapₛₗ h

Composition of semilinear maps becomes composition of the induced ring homomorphisms. The composites are related by pointwise equations, so that this applies to composites which only agree propositionally.

theorem TauCeti.SymmetricAlgebra.mapₛₗ_mem_homogeneousSubmodule {R : Type u₁} {S : Type u₂} [CommSemiring R] [CommSemiring S] {M : Type v₁} {N : Type v₂} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module S N] {φ : R →+* S} (f : M →ₛₗ[φ] N) {n : ℕ} {x : SymmetricAlgebra R M} (hx : x ∈ homogeneousSubmodule R M n) : (SymmetricAlgebra.mapₛₗ f) x ∈ homogeneousSubmodule S N n

The ring homomorphism induced by a semilinear map preserves the homogeneous pieces.

noncomputable def TauCeti.SymmetricAlgebra.homogeneousSubmoduleMapₛₗ {R : Type u₁} {S : Type u₂} [CommSemiring R] [CommSemiring S] {M : Type v₁} {N : Type v₂} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module S N] {φ : R →+* S} (f : M →ₛₗ[φ] N) (n : ℕ) : ↥(homogeneousSubmodule R M n) →ₛₗ[φ] ↥(homogeneousSubmodule S N n)

The semilinear map between degree-n homogeneous pieces induced by a semilinear map: the restriction of SymmetricAlgebra.mapₛₗ.

Equations

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

@[simp]

theorem TauCeti.SymmetricAlgebra.coe_homogeneousSubmoduleMapₛₗ_apply {R : Type u₁} {S : Type u₂} [CommSemiring R] [CommSemiring S] {M : Type v₁} {N : Type v₂} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module S N] {φ : R →+* S} (f : M →ₛₗ[φ] N) (n : ℕ) (x : ↥(homogeneousSubmodule R M n)) : ↑((homogeneousSubmoduleMapₛₗ f n) x) = (SymmetricAlgebra.mapₛₗ f) ↑x

The map between homogeneous pieces induced by a semilinear map is computed in the symmetric algebra by SymmetricAlgebra.mapₛₗ.

theorem TauCeti.SymmetricAlgebra.map_mem_homogeneousSubmodule {R : Type u₁} [CommSemiring R] {M : Type v₁} [AddCommMonoid M] [Module R M] {N' : Type u_1} [AddCommMonoid N'] [Module R N'] (f : M →ₗ[R] N') {n : ℕ} {x : SymmetricAlgebra R M} (hx : x ∈ homogeneousSubmodule R M n) : (SymmetricAlgebra.map R f) x ∈ homogeneousSubmodule R N' n

The algebra homomorphism induced by a linear map preserves the homogeneous pieces.