Tensor squares of subrings

This file defines the canonical map from the integral tensor square of a subring of an algebra to the tensor square of the ambient algebra, together with its range and basic membership lemmas.

Main definitions and results

• Subring.tensorSquareMap: the canonical map from the integral tensor square.
• Subring.tensorSquareMap_injective: over a rational algebra, the canonical map is injective.
• Subring.tensorSquareRange: the range of the canonical map.
• Subring.tensorSquareEquivRange: over a rational algebra, the canonical equivalence onto that range.
• Subring.mem_tensorSquareRange_iff: membership in the range in terms of a preimage.
• Subring.tmul_mem_tensorSquareRange: pure tensors of subring elements lie in the range.

noncomputable def Subring.tensorSquareMap (R : Type u) {A : Type v} [CommRing R] [Ring A] [Algebra R A] (S : Subring A) : TensorProduct ℤ ↥S ↥S →ₐ[ℤ] TensorProduct R A A

The canonical map from the integral tensor square of a subring to the tensor square of the ambient algebra. On pure tensors, it applies the subring inclusion in both factors.

Equations

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

@[simp]

theorem Subring.tensorSquareMap_tmul (R : Type u) {A : Type v} [CommRing R] [Ring A] [Algebra R A] (S : Subring A) (x y : ↥S) : (tensorSquareMap R S) (x ⊗ₜ[ℤ] y) = ↑x ⊗ₜ[R] ↑y

The canonical tensor-square map sends a pure tensor to the pure tensor of the underlying ambient elements.

theorem Subring.tensorSquareMap_injective {A : Type v} [Ring A] [Algebra ℚ A] (S : Subring A) : Function.Injective ⇑(tensorSquareMap ℚ S)

The canonical map from the integer tensor square of a subring of a rational algebra to the rational tensor square of the ambient algebra is injective.

noncomputable def Subring.tensorSquareRange (R : Type u) {A : Type v} [CommRing R] [Ring A] [Algebra R A] (S : Subring A) : Subring (TensorProduct R A A)

The range of the canonical map from the integral tensor square of a subring to the tensor square of the ambient algebra.

Equations

• Subring.tensorSquareRange R S = (Subring.tensorSquareMap R S).range

@[simp]

theorem Subring.mem_tensorSquareRange_iff (R : Type u) {A : Type v} [CommRing R] [Ring A] [Algebra R A] (S : Subring A) (z : TensorProduct R A A) : z ∈ tensorSquareRange R S ↔ ∃ (t : TensorProduct ℤ ↥S ↥S), (tensorSquareMap R S) t = z

Membership in the tensor-square range is equivalent to having an integral tensor preimage.

theorem Subring.tmul_mem_tensorSquareRange (R : Type u) {A : Type v} [CommRing R] [Ring A] [Algebra R A] (S : Subring A) {x y : A} (hx : x ∈ S) (hy : y ∈ S) : x ⊗ₜ[R] y ∈ tensorSquareRange R S

A pure tensor whose two factors lie in a subring belongs to its tensor-square range.

noncomputable def Subring.tensorSquareEquivRange {A : Type v} [Ring A] [Algebra ℚ A] (S : Subring A) : TensorProduct ℤ ↥S ↥S ≃ₐ[ℤ] ↥(tensorSquareRange ℚ S)

The canonical equivalence from the integer tensor square of a subring of a rational algebra onto its range in the rational tensor square.

Equations

• S.tensorSquareEquivRange = AlgEquiv.ofInjective (Subring.tensorSquareMap ℚ S) ⋯

@[simp]

theorem Subring.coe_tensorSquareEquivRange_apply {A : Type v} [Ring A] [Algebra ℚ A] (S : Subring A) (t : TensorProduct ℤ ↥S ↥S) : ↑(S.tensorSquareEquivRange t) = (tensorSquareMap ℚ S) t

The equivalence onto the tensor-square range acts by the canonical tensor-square map.