Automorphisms of scalar extensions

For a module V over a commutative ring R, this file packages

A ↦ Autₐ(A ⊗[R] V)

as a functor from commutative R-algebras to groups. A morphism φ : A ⟶ B acts by base change of the automorphism, Module.End.mapValueGL; this file only indexes that operation by the bundled category of commutative algebras and packages the result as a functor.

The public characterization uses the canonical map A ⊗[R] V → B ⊗[R] V. Scalar extension of an automorphism commutes with this map, and its value on a pure tensor is consequently determined by the original automorphism on 1 ⊗ₜ v.

No finiteness, freeness, projectivity, flatness, or nontriviality hypothesis is used. In particular, the construction includes zero rings and the zero module. This is only the fixed-module automorphism functor; no representability or functoriality in V is asserted.

Main declarations

• GeneralLinear.scalarExtensionAutomorphisms: the automorphism group at a value algebra.
• GeneralLinear.mapScalarExtensionAutomorphisms: extension of automorphisms along a value-algebra morphism.
• GeneralLinear.scalarExtensionAutomorphismsFunctor: the resulting group-valued functor.

References

• J. S. Milne, Algebraic Groups (2017), §2.8 and Chapter 4(a).
• The Stacks Project, Tags 00CV and 05G3.

@[reducible, inline]

abbrev TauCeti.GeneralLinear.scalarExtensionAutomorphisms {R : Type u} [CommRing R] {V : Type v} [AddCommMonoid V] [Module R V] (A : CommAlgCat R) : GrpCat

The group of linear automorphisms of the scalar extension A ⊗[R] V.

Equations

• TauCeti.GeneralLinear.scalarExtensionAutomorphisms A = ↧(LinearMap.GeneralLinearGroup (↑A) (TensorProduct R (↑A) V))

def TauCeti.GeneralLinear.scalarExtensionMap {R : Type u} [CommRing R] {V : Type v} [AddCommMonoid V] [Module R V] {A B : CommAlgCat R} (φ : A ⟶ B) : TensorProduct R (↑A) V →ₗ[R] TensorProduct R (↑B) V

The canonical map between scalar extensions induced by a morphism of value algebras.

Equations

• TauCeti.GeneralLinear.scalarExtensionMap φ = LinearMap.rTensor V (CommAlgCat.Hom.hom φ).toLinearMap

@[simp]

theorem TauCeti.GeneralLinear.scalarExtensionMap_tmul {R : Type u} [CommRing R] {V : Type v} [AddCommMonoid V] [Module R V] {A B : CommAlgCat R} (φ : A ⟶ B) (a : ↑A) (v : V) : (scalarExtensionMap φ) (a ⊗ₜ[R] v) = (CommAlgCat.Hom.hom φ) a ⊗ₜ[R] v

The canonical map between scalar extensions sends a pure tensor to the corresponding pure tensor with its scalar mapped into the target algebra.

theorem TauCeti.GeneralLinear.scalarExtensionMap_eq_map {R : Type u} [CommRing R] {V : Type v} [AddCommMonoid V] [Module R V] {A B : CommAlgCat R} (φ : A ⟶ B) : scalarExtensionMap φ = TensorProduct.map (CommAlgCat.Hom.hom φ).toLinearMap LinearMap.id

The canonical map between scalar extensions is the value-algebra morphism tensored with the identity of the module.

theorem TauCeti.GeneralLinear.scalarExtensionMap_injective {R : Type u} [CommRing R] {V : Type v} [AddCommMonoid V] [Module R V] [Module.Flat R V] {A B : CommAlgCat R} (φ : A ⟶ B) (hφ : Function.Injective ⇑(CommAlgCat.Hom.hom φ)) : Function.Injective ⇑(scalarExtensionMap φ)

Over a flat module, the canonical map between scalar extensions inherits injectivity from the value-algebra morphism.

@[simp]

theorem TauCeti.GeneralLinear.scalarExtensionMap_id {R : Type u} [CommRing R] {V : Type v} [AddCommMonoid V] [Module R V] (A : CommAlgCat R) : scalarExtensionMap (CategoryTheory.CategoryStruct.id A) = LinearMap.id

The canonical map associated to the identity morphism is the identity linear map.

@[simp]

theorem TauCeti.GeneralLinear.scalarExtensionMap_comp {R : Type u} [CommRing R] {V : Type v} [AddCommMonoid V] [Module R V] {A B C : CommAlgCat R} (φ : A ⟶ B) (ψ : B ⟶ C) : scalarExtensionMap (CategoryTheory.CategoryStruct.comp φ ψ) = scalarExtensionMap ψ ∘ₗ scalarExtensionMap φ

Canonical maps between scalar extensions compose covariantly.

@[simp]

theorem TauCeti.GeneralLinear.scalarExtensionMap_smul {R : Type u} [CommRing R] {V : Type v} [AddCommMonoid V] [Module R V] {A B : CommAlgCat R} (φ : A ⟶ B) (a : ↑A) (x : TensorProduct R (↑A) V) : (scalarExtensionMap φ) (a • x) = (CommAlgCat.Hom.hom φ) a • (scalarExtensionMap φ) x

The canonical map between scalar extensions is semilinear for the value-algebra morphism.

noncomputable def TauCeti.GeneralLinear.mapScalarExtensionAutomorphisms {R : Type u} [CommRing R] {V : Type v} [AddCommMonoid V] [Module R V] {A B : CommAlgCat R} (φ : A ⟶ B) : scalarExtensionAutomorphisms A ⟶ scalarExtensionAutomorphisms B

Extend a scalar-extension automorphism along a morphism of value algebras.

This is Module.End.mapValueGL at the underlying algebra morphism, bundled as a morphism of groups; all of its computation rules come from there.

Equations

• TauCeti.GeneralLinear.mapScalarExtensionAutomorphisms φ = GrpCat.ofHom (Module.End.mapValueGL (CommAlgCat.Hom.hom φ))

@[simp]

theorem TauCeti.GeneralLinear.val_mapScalarExtensionAutomorphisms {R : Type u} [CommRing R] {V : Type v} [AddCommMonoid V] [Module R V] {A B : CommAlgCat R} (φ : A ⟶ B) (g : ↑(scalarExtensionAutomorphisms A)) : ↑((CategoryTheory.ConcreteCategory.hom (mapScalarExtensionAutomorphisms φ)) g) = Module.End.mapValue (CommAlgCat.Hom.hom φ) ↑g

The underlying endomorphism of an extended automorphism is the base change of the underlying endomorphism.

@[simp]

theorem TauCeti.GeneralLinear.mapScalarExtensionAutomorphisms_tmul {R : Type u} [CommRing R] {V : Type v} [AddCommMonoid V] [Module R V] {A B : CommAlgCat R} (φ : A ⟶ B) (g : ↑(scalarExtensionAutomorphisms A)) (b : ↑B) (v : V) : ↑((CategoryTheory.ConcreteCategory.hom (mapScalarExtensionAutomorphisms φ)) g) (b ⊗ₜ[R] v) = b • (scalarExtensionMap φ) (↑g (1 ⊗ₜ[R] v))

Scalar extension of an automorphism is characterized on pure tensors by its value on the canonical copy of the original module.

@[simp]

theorem TauCeti.GeneralLinear.mapScalarExtensionAutomorphisms_apply_scalarExtensionMap {R : Type u} [CommRing R] {V : Type v} [AddCommMonoid V] [Module R V] {A B : CommAlgCat R} (φ : A ⟶ B) (g : ↑(scalarExtensionAutomorphisms A)) (x : TensorProduct R (↑A) V) : ↑((CategoryTheory.ConcreteCategory.hom (mapScalarExtensionAutomorphisms φ)) g) ((scalarExtensionMap φ) x) = (scalarExtensionMap φ) (↑g x)

Extending an automorphism commutes with the canonical map between scalar extensions.

theorem TauCeti.GeneralLinear.eq_mapScalarExtensionAutomorphisms_of_apply_scalarExtensionMap_eq {R : Type u} [CommRing R] {V : Type v} [AddCommMonoid V] [Module R V] {A B : CommAlgCat R} (φ : A ⟶ B) (g : ↑(scalarExtensionAutomorphisms A)) (h : ↑(scalarExtensionAutomorphisms B)) (h_apply : ∀ (x : TensorProduct R (↑A) V), ↑h ((scalarExtensionMap φ) x) = (scalarExtensionMap φ) (↑g x)) : h = (CategoryTheory.ConcreteCategory.hom (mapScalarExtensionAutomorphisms φ)) g

A target automorphism that intertwines the canonical map with g is the scalar extension of g.

theorem TauCeti.GeneralLinear.mapScalarExtensionAutomorphisms_injective {R : Type u} [CommRing R] {V : Type v} [AddCommMonoid V] [Module R V] {A B : CommAlgCat R} (φ : A ⟶ B) (hφ : Function.Injective ⇑(scalarExtensionMap φ)) : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (mapScalarExtensionAutomorphisms φ))

Extension of automorphisms is injective as soon as the canonical map between scalar extensions is. An automorphism of A ⊗[R] V is determined by its values on the pure tensors 1 ⊗ v, and those values are recorded faithfully by the canonical map.

@[simp]

theorem TauCeti.GeneralLinear.mapScalarExtensionAutomorphisms_id {R : Type u} [CommRing R] {V : Type v} [AddCommMonoid V] [Module R V] (A : CommAlgCat R) : mapScalarExtensionAutomorphisms (CategoryTheory.CategoryStruct.id A) = CategoryTheory.CategoryStruct.id (scalarExtensionAutomorphisms A)

Extension of scalar-extension automorphisms preserves identity morphisms of value algebras.

@[simp]

theorem TauCeti.GeneralLinear.mapScalarExtensionAutomorphisms_comp {R : Type u} [CommRing R] {V : Type v} [AddCommMonoid V] [Module R V] {A B C : CommAlgCat R} (φ : A ⟶ B) (ψ : B ⟶ C) : mapScalarExtensionAutomorphisms (CategoryTheory.CategoryStruct.comp φ ψ) = CategoryTheory.CategoryStruct.comp (mapScalarExtensionAutomorphisms φ) (mapScalarExtensionAutomorphisms ψ)

Extension of scalar-extension automorphisms preserves composition of value-algebra morphisms.

noncomputable def TauCeti.GeneralLinear.scalarExtensionAutomorphismsFunctor {R : Type u} [CommRing R] {V : Type v} [AddCommMonoid V] [Module R V] : CategoryTheory.Functor (CommAlgCat R) GrpCat

The group-valued functor of linear automorphisms of scalar extensions of V.

Equations

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

@[simp]

theorem TauCeti.GeneralLinear.scalarExtensionAutomorphismsFunctor_obj {R : Type u} [CommRing R] {V : Type v} [AddCommMonoid V] [Module R V] (A : CommAlgCat R) : scalarExtensionAutomorphismsFunctor.obj A = scalarExtensionAutomorphisms A

The functor takes a value algebra to the automorphism group of the corresponding scalar extension.

@[simp]

theorem TauCeti.GeneralLinear.scalarExtensionAutomorphismsFunctor_map {R : Type u} [CommRing R] {V : Type v} [AddCommMonoid V] [Module R V] {A B : CommAlgCat R} (φ : A ⟶ B) : scalarExtensionAutomorphismsFunctor.map φ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (mapScalarExtensionAutomorphisms φ) (CategoryTheory.eqToHom ⋯))

The functor takes a morphism of value algebras to the corresponding extension of automorphisms.