Products of subalgebras #
In this file we define the product of subalgebras as a subalgebra of the product algebra.
Main definitions #
Subalgebra.pi: the product of subalgebras.
def
Subalgebra.pi
{ι : Type u_1}
{R : Type u_2}
{S : ι → Type u_3}
[CommSemiring R]
[(i : ι) → Semiring (S i)]
[(i : ι) → Algebra R (S i)]
(s : Set ι)
(t : (i : ι) → Subalgebra R (S i))
:
Subalgebra R ((i : ι) → S i)
The product of subalgebras as a subalgebra.
Equations
- Subalgebra.pi s t = { carrier := (Submodule.pi s fun (i : ι) => Subalgebra.toSubmodule (t i)).carrier, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, algebraMap_mem' := ⋯ }
Instances For
@[simp]
theorem
Subalgebra.coe_pi
{ι : Type u_1}
{R : Type u_2}
{S : ι → Type u_3}
[CommSemiring R]
[(i : ι) → Semiring (S i)]
[(i : ι) → Algebra R (S i)]
(s : Set ι)
(t : (i : ι) → Subalgebra R (S i))
:
@[simp]
theorem
Subalgebra.pi_toSubsemiring
{ι : Type u_1}
{R : Type u_2}
{S : ι → Type u_3}
[CommSemiring R]
[(i : ι) → Semiring (S i)]
[(i : ι) → Algebra R (S i)]
(s : Set ι)
(t : (i : ι) → Subalgebra R (S i))
:
(pi s t).toSubsemiring = { carrier := (Submodule.pi s fun (i : ι) => toSubmodule (t i)).carrier, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯,
zero_mem' := ⋯ }
@[simp]
theorem
Subalgebra.mem_pi
{ι : Type u_1}
{R : Type u_2}
{S : ι → Type u_3}
[CommSemiring R]
[(i : ι) → Semiring (S i)]
[(i : ι) → Algebra R (S i)]
{s : Set ι}
{t : (i : ι) → Subalgebra R (S i)}
{x : (i : ι) → S i}
:
@[simp]
theorem
Subalgebra.pi_toSubmodule
{ι : Type u_1}
{R : Type u_2}
{S : ι → Type u_3}
[CommSemiring R]
[(i : ι) → Semiring (S i)]
[(i : ι) → Algebra R (S i)]
{s : Set ι}
{t : (i : ι) → Subalgebra R (S i)}
:
theorem
Subalgebra.pi_mono
{ι : Type u_1}
{R : Type u_2}
{S : ι → Type u_3}
[CommSemiring R]
[(i : ι) → Semiring (S i)]
[(i : ι) → Algebra R (S i)]
{s : Set ι}
{t₁ t₂ : (i : ι) → Subalgebra R (S i)}
(h : ∀ i ∈ s, t₁ i ≤ t₂ i)
: