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) :
    toSubmodule (S.prod S₁) = (toSubmodule S).prod (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 T : Subalgebra R A} {S₁ 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 T : Subalgebra R A} {S₁ T₁ : Subalgebra R B} :
    S.prod S₁ ⊓ T.prod T₁ = (S ⊓ T).prod (S₁ ⊓ T₁)
    source
    theorem Subalgebra.center_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] :
    center R (A × B) = (center R A).prod (center R B)
    source
    @[simp]
    theorem AlgHom.range_prodMap {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [Semiring C] [Algebra R C] [Semiring D] [Algebra R D] (f : A →ₐ[R] B) (g : C →ₐ[R] D) :
    (f.prodMap g).range = f.range.prod g.range