Restricting additive automorphisms to invariant subgroups

An additive automorphism of an abelian group which preserves an additive subgroup restricts to an integral linear automorphism of that subgroup. Base change gives an automorphism of every scalar extension of the subgroup, compatibly with further scalar extension.

Main declarations

• AddEquiv.invariantRestrict: restriction to an invariant additive subgroup.
• AddEquiv.baseChangeInvariantRestrictUnit: the induced automorphism after scalar extension.
• AddEquiv.baseChange_invariantRestrict_map_baseChange_basis: its action on a base-changed basis when the original restriction is monomial in that basis.
• AddEquiv.baseChangeInvariantRestrictUnit_pow_eq_one: transport of an exponent bound to scalar extensions.
• AddEquiv.mapScalarExtensionAutomorphisms_baseChangeInvariantRestrictUnit: compatibility with further scalar extension.

Restriction to an invariant subgroup

def AddEquiv.invariantRestrict {V : Type u} [AddCommGroup V] {S : Type u_1} [SetLike S V] [AddSubgroupClass S V] (θ : V ≃+ V) (M : S) (hθ : ∀ (v : V), θ v ∈ M ↔ v ∈ M) : ↥M ≃ₗ[ℤ] ↥M

An additive automorphism of V that restricts to a bijection of an additive subgroup M, viewed as an integral linear automorphism of M.

Equations

• θ.invariantRestrict M hθ = { toFun := fun (v : ↥M) => ⟨θ ↑v, ⋯⟩, map_add' := ⋯, map_smul' := ⋯, invFun := fun (v : ↥M) => ⟨θ.symm ↑v, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem AddEquiv.coe_invariantRestrict_apply {V : Type u} [AddCommGroup V] {S : Type u_1} [SetLike S V] [AddSubgroupClass S V] (θ : V ≃+ V) (M : S) (hθ : ∀ (v : V), θ v ∈ M ↔ v ∈ M) (v : ↥M) : ↑((θ.invariantRestrict M hθ) v) = θ ↑v

The restriction of θ to an invariant subgroup acts by θ.

@[simp]

theorem AddEquiv.coe_invariantRestrict_symm_apply {V : Type u} [AddCommGroup V] {S : Type u_1} [SetLike S V] [AddSubgroupClass S V] (θ : V ≃+ V) (M : S) (hθ : ∀ (v : V), θ v ∈ M ↔ v ∈ M) (v : ↥M) : ↑((θ.invariantRestrict M hθ).symm v) = θ.symm ↑v

The inverse of the restriction of θ acts by θ.symm.

theorem AddEquiv.invariantRestrict_symm {V : Type u} [AddCommGroup V] {S : Type u_1} [SetLike S V] [AddSubgroupClass S V] (θ : V ≃+ V) (M : S) (hθ : ∀ (v : V), θ v ∈ M ↔ v ∈ M) : (θ.invariantRestrict M hθ).symm = θ.symm.invariantRestrict M ⋯

Restriction commutes with taking the inverse automorphism.

theorem AddEquiv.coe_invariantRestrict_pow_apply {V : Type u} [AddCommGroup V] {S : Type u_1} [SetLike S V] [AddSubgroupClass S V] (θ : V ≃+ V) (M : S) (hθ : ∀ (v : V), θ v ∈ M ↔ v ∈ M) (n : ℕ) (v : ↥M) : ↑((θ.invariantRestrict M hθ ^ n) v) = (θ.toIntLinearEquiv ^ n) ↑v

Powers of the restriction of θ act by the corresponding powers of θ.

Base change

noncomputable def AddEquiv.baseChangeInvariantRestrictUnit {V : Type u} [AddCommGroup V] {S : Type u_1} [SetLike S V] [AddSubgroupClass S V] {R : Type v} [CommRing R] [Algebra ℤ R] (θ : V ≃+ V) (M : S) (hθ : ∀ (v : V), θ v ∈ M ↔ v ∈ M) : LinearMap.GeneralLinearGroup R (TensorProduct ℤ R ↥M)

The automorphism of R ⊗[ℤ] M obtained by base-changing the restriction of θ.

Equations

• θ.baseChangeInvariantRestrictUnit M hθ = LinearMap.GeneralLinearGroup.ofLinearEquiv (LinearEquiv.baseChange ℤ R (↥M) (↥M) (θ.invariantRestrict M hθ))

theorem AddEquiv.val_baseChangeInvariantRestrictUnit_apply {V : Type u} [AddCommGroup V] {S : Type u_1} [SetLike S V] [AddSubgroupClass S V] {R : Type v} [CommRing R] [Algebra ℤ R] (θ : V ≃+ V) (M : S) (hθ : ∀ (v : V), θ v ∈ M ↔ v ∈ M) (z : TensorProduct ℤ R ↥M) : ↑(θ.baseChangeInvariantRestrictUnit M hθ) z = (LinearEquiv.baseChange ℤ R (↥M) (↥M) (θ.invariantRestrict M hθ)) z

The induced automorphism is the base change of the restriction of θ.

@[simp]

theorem AddEquiv.val_baseChangeInvariantRestrictUnit_tmul {V : Type u} [AddCommGroup V] {S : Type u_1} [SetLike S V] [AddSubgroupClass S V] {R : Type v} [CommRing R] [Algebra ℤ R] (θ : V ≃+ V) (M : S) (hθ : ∀ (v : V), θ v ∈ M ↔ v ∈ M) (r : R) (v : ↥M) : ↑(θ.baseChangeInvariantRestrictUnit M hθ) (r ⊗ₜ[ℤ] v) = r ⊗ₜ[ℤ] (θ.invariantRestrict M hθ) v

The induced automorphism acts on a pure tensor through the restriction of θ.

@[simp]

theorem AddEquiv.val_baseChangeInvariantRestrictUnit_inv_tmul {V : Type u} [AddCommGroup V] {S : Type u_1} [SetLike S V] [AddSubgroupClass S V] {R : Type v} [CommRing R] [Algebra ℤ R] (θ : V ≃+ V) (M : S) (hθ : ∀ (v : V), θ v ∈ M ↔ v ∈ M) (r : R) (v : ↥M) : ↑(θ.baseChangeInvariantRestrictUnit M hθ)⁻¹ (r ⊗ₜ[ℤ] v) = r ⊗ₜ[ℤ] (θ.invariantRestrict M hθ).symm v

The inverse induced automorphism acts on a pure tensor through the inverse restriction.

theorem AddEquiv.baseChange_invariantRestrict_map_baseChange_basis {V : Type u} [AddCommGroup V] {S : Type u_1} [SetLike S V] [AddSubgroupClass S V] {R : Type v} [CommRing R] [Algebra ℤ R] {η : Type u_2} (M : S) (b : Module.Basis η ℤ ↥M) (θ : V ≃+ V) (hθM : ∀ (v : V), θ v ∈ M ↔ v ∈ M) (τ : η → η) (c : η → ℤ) (hθb : ∀ (i : η), (θ.invariantRestrict M hθM) (b i) = c i • b (τ i)) (i : η) : (LinearEquiv.baseChange ℤ R (↥M) (↥M) (θ.invariantRestrict M hθM)) ((Module.Basis.baseChange R b) i) = (algebraMap ℤ R) (c i) • (Module.Basis.baseChange R b) (τ i)

If an invariant restriction sends each basis vector to a scalar multiple of another basis vector, its base change has the corresponding monomial action on the base-changed basis.

theorem AddEquiv.baseChangeInvariantRestrictUnit_pow_eq_one {V : Type u} [AddCommGroup V] {S : Type u_1} [SetLike S V] [AddSubgroupClass S V] {R : Type v} [CommRing R] [Algebra ℤ R] (θ : V ≃+ V) (M : S) (hθ : ∀ (v : V), θ v ∈ M ↔ v ∈ M) {n : ℕ} (hn : ∀ (v : V), (θ.toIntLinearEquiv ^ n) v = v) : θ.baseChangeInvariantRestrictUnit M hθ ^ n = 1

An exponent bound on θ is preserved by restriction and scalar extension.

theorem AddEquiv.mapScalarExtensionAutomorphisms_baseChangeInvariantRestrictUnit {V : Type u} [AddCommGroup V] {S : Type u_1} [SetLike S V] [AddSubgroupClass S V] {A B : CommAlgCat ℤ} (θ : V ≃+ V) (M : S) (hθ : ∀ (v : V), θ v ∈ M ↔ v ∈ M) (φ : A ⟶ B) : (CategoryTheory.ConcreteCategory.hom (TauCeti.GeneralLinear.mapScalarExtensionAutomorphisms φ)) (θ.baseChangeInvariantRestrictUnit M hθ) = θ.baseChangeInvariantRestrictUnit M hθ

Further scalar extension leaves the base-changed restriction unchanged.