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 #

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
    @[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 : Subalgebra R A} {T : Subalgebra R A} {S₁ : Subalgebra R B} {T₁ : Subalgebra R B} :
    S TS₁ 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 : 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₁)