Documentation

Mathlib.Algebra.Algebra.Subalgebra.Prod

Products of subalgebras #

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

Main definitions #

source
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' := ⋯ }
Instances For
    source
    @[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₁
    source
    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₁)
    source
    @[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₁
    source
    @[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 ⊤ = ⊤
    source
    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 : Subalgebra R A} {T : Subalgebra R A} {S₁ : Subalgebra R B} {T₁ : Subalgebra R B} :
    S ≤ T → S₁ ≤ T₁ → S.prod S₁ ≤ T.prod T₁
    source
    @[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 : Subalgebra R A} {T : Subalgebra R A} {S₁ : Subalgebra R B} {T₁ : Subalgebra R B} :
    S.prod S₁ ⊓ T.prod T₁ = (S ⊓ T).prod (S₁ ⊓ T₁)