Tensor restriction maps

This file packages the bilinear maps used in the Stepanov restriction step. For submodules R, S, and T of a commutative K-algebra L, an algebra endomorphism φ gives the two twisted products x * φ y and φ x * y. An explicit containment hypothesis promotes either product to a linear map from R ⊗[K] S into T.

The final lemmas record the finite-generation and finrank consequences that are needed when such a tensor restriction map is used as a target map in a rank-nullity argument.

def BGS.HasseWeil.tensorRestriction {K : Type u_1} {L : Type u_2} [Field K] [CommRing L] [Algebra K L] {R S T : Submodule K L} (φ : L →ₐ[K] L) (hmul : ∀ (x : ↥R) (y : ↥S), ↑x * φ ↑y ∈ T) : TensorProduct K ↥R ↥S →ₗ[K] ↥T

The tensor restriction map induced by the twisted product (x, y) ↦ x * φ y, with codomain restricted by hmul.

Equations

• BGS.HasseWeil.tensorRestriction φ hmul = TensorProduct.lift (LinearMap.mk₂ K (fun (x : ↥R) (y : ↥S) => ⟨↑x * φ ↑y, ⋯⟩) ⋯ ⋯ ⋯ ⋯)

@[simp]

theorem BGS.HasseWeil.tensorRestriction_tmul {K : Type u_1} {L : Type u_2} [Field K] [CommRing L] [Algebra K L] {R S T : Submodule K L} (φ : L →ₐ[K] L) (hmul : ∀ (x : ↥R) (y : ↥S), ↑x * φ ↑y ∈ T) (x : ↥R) (y : ↥S) : (tensorRestriction φ hmul) (x ⊗ₜ[K] y) = ⟨↑x * φ ↑y, ⋯⟩

def BGS.HasseWeil.swappedTensorRestriction {K : Type u_1} {L : Type u_2} [Field K] [CommRing L] [Algebra K L] {R S T : Submodule K L} (φ : L →ₐ[K] L) (hmul : ∀ (x : ↥R) (y : ↥S), φ ↑x * ↑y ∈ T) : TensorProduct K ↥R ↥S →ₗ[K] ↥T

The swapped tensor restriction map induced by the twisted product (x, y) ↦ φ x * y, with codomain restricted by hmul.

Equations

• BGS.HasseWeil.swappedTensorRestriction φ hmul = TensorProduct.lift (LinearMap.mk₂ K (fun (x : ↥R) (y : ↥S) => ⟨φ ↑x * ↑y, ⋯⟩) ⋯ ⋯ ⋯ ⋯)

@[simp]

theorem BGS.HasseWeil.swappedTensorRestriction_tmul {K : Type u_1} {L : Type u_2} [Field K] [CommRing L] [Algebra K L] {R S T : Submodule K L} (φ : L →ₐ[K] L) (hmul : ∀ (x : ↥R) (y : ↥S), φ ↑x * ↑y ∈ T) (x : ↥R) (y : ↥S) : (swappedTensorRestriction φ hmul) (x ⊗ₜ[K] y) = ⟨φ ↑x * ↑y, ⋯⟩

theorem BGS.HasseWeil.moduleFinite_tensorProduct {K : Type u_1} {L : Type u_2} [Field K] [CommRing L] [Algebra K L] {R S : Submodule K L} [Module.Finite K ↥R] [Module.Finite K ↥S] : Module.Finite K (TensorProduct K ↥R ↥S)

A tensor product of finite modules is finite. This named bridge keeps downstream restriction arguments independent of the tensor-product instance search details.

theorem BGS.HasseWeil.moduleFinite_range_tensorProductMap {K : Type u_1} {L : Type u_2} [Field K] [CommRing L] [Algebra K L] {R S : Submodule K L} {U : Type u_3} [AddCommGroup U] [Module K U] [Module.Finite K ↥R] [Module.Finite K ↥S] (f : TensorProduct K ↥R ↥S →ₗ[K] U) : Module.Finite K ↥f.range

The range of a linear map out of a tensor product of finite modules is finite.

theorem BGS.HasseWeil.finrank_range_tensorProductMap_le {K : Type u_1} {L : Type u_2} [Field K] [CommRing L] [Algebra K L] {R S : Submodule K L} {U : Type u_3} [AddCommGroup U] [Module K U] [Module.Finite K ↥R] [Module.Finite K ↥S] (f : TensorProduct K ↥R ↥S →ₗ[K] U) : Module.finrank K ↥f.range ≤ Module.finrank K ↥R * Module.finrank K ↥S

The range of a linear map out of R ⊗ S has finrank at most the product of the two input finranks.

theorem BGS.HasseWeil.moduleFinite_of_surjective_tensorProductMap {K : Type u_1} {L : Type u_2} [Field K] [CommRing L] [Algebra K L] {R S : Submodule K L} {U : Type u_3} [AddCommGroup U] [Module K U] [Module.Finite K ↥R] [Module.Finite K ↥S] (f : TensorProduct K ↥R ↥S →ₗ[K] U) (hf : Function.Surjective ⇑f) : Module.Finite K U

A surjective linear map out of R ⊗ S makes its target finite.

theorem BGS.HasseWeil.finrank_le_mul_of_surjective_tensorProductMap {K : Type u_1} {L : Type u_2} [Field K] [CommRing L] [Algebra K L] {R S : Submodule K L} {U : Type u_3} [AddCommGroup U] [Module K U] [Module.Finite K ↥R] [Module.Finite K ↥S] (f : TensorProduct K ↥R ↥S →ₗ[K] U) (hf : Function.Surjective ⇑f) : Module.finrank K U ≤ Module.finrank K ↥R * Module.finrank K ↥S

A surjective linear map out of R ⊗ S bounds the target finrank by the product of the two input finranks.