Products of subalgebras

In this file we define the product of two subalgebras as a subalgebra of the product algebra.

Main definitions

• Subalgebra.prod: the product of two subalgebras.

def Subalgebra.prod {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] (S : Subalgebra R A) (S₁ : Subalgebra R B) : Subalgebra R (A × B)

The product of two subalgebras is a subalgebra.

Equations

• S.prod S₁ = { carrier := ↑S ×ˢ ↑S₁, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, algebraMap_mem' := ⋯ }

@[simp]

theorem Subalgebra.coe_prod {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] (S : Subalgebra R A) (S₁ : Subalgebra R B) : ↑(S.prod S₁) = ↑S ×ˢ ↑S₁

theorem Subalgebra.prod_toSubmodule {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] (S : Subalgebra R A) (S₁ : Subalgebra R B) : Subalgebra.toSubmodule (S.prod S₁) = (Subalgebra.toSubmodule S).prod (Subalgebra.toSubmodule S₁)

@[simp]

theorem Subalgebra.mem_prod {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] {S : Subalgebra R A} {S₁ : Subalgebra R B} {x : A × B} : x ∈ S.prod S₁ ↔ x.1 ∈ S ∧ x.2 ∈ S₁

@[simp]

theorem Subalgebra.prod_top {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] : ⊤.prod ⊤ = ⊤

theorem Subalgebra.prod_mono {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] {S T : Subalgebra R A} {S₁ T₁ : Subalgebra R B} : S ≤ T → S₁ ≤ T₁ → S.prod S₁ ≤ T.prod T₁

@[simp]

theorem Subalgebra.prod_inf_prod {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] {S T : Subalgebra R A} {S₁ T₁ : Subalgebra R B} : S.prod S₁ ⊓ T.prod T₁ = (S ⊓ T).prod (S₁ ⊓ T₁)