Mathlib.Algebra.Algebra.Subalgebra.Prod

Subalgebra.prod definition

: Subalgebra R (A × B)

Full source

/-- The product of two subalgebras is a subalgebra. -/
def prod : Subalgebra R (A × B) :=
  { S.toSubsemiring.prod S₁.toSubsemiring with
    carrier := S ×ˢ S₁
    algebraMap_mem' := fun _ => ⟨algebraMap_mem _ _, algebraMap_mem _ _⟩ }

Product of subalgebras

Informal description

Given two subalgebras $S$ of an $R$-algebra $A$ and $S_1$ of an $R$-algebra $B$, their product $S \times S_1$ is a subalgebra of the product algebra $A \times B$. The underlying set of this subalgebra is the Cartesian product of the underlying sets of $S$ and $S_1$, and it is closed under the algebra operations and contains the image of the algebra map from $R$.

Subalgebra.coe_prod theorem

: (prod S S₁ : Set (A × B)) = (S : Set A) ×ˢ (S₁ : Set B)

Full source

@[simp]
theorem coe_prod : (prod S S₁ : Set (A × B)) = (S : Set A) ×ˢ (S₁ : Set B) :=
  rfl

Underlying Set of Product Subalgebra Equals Cartesian Product of Underlying Sets

Informal description

For any subalgebras $S$ of an $R$-algebra $A$ and $S_1$ of an $R$-algebra $B$, the underlying set of their product subalgebra $S \times S_1$ in $A \times B$ is equal to the Cartesian product of the underlying sets of $S$ and $S_1$, i.e., $(S \times S_1) = S \timesˢ S_1$.

Subalgebra.prod_toSubmodule theorem

: toSubmodule (S.prod S₁) = (toSubmodule S).prod (toSubmodule S₁)

Full source

theorem prod_toSubmodule : toSubmodule (S.prod S₁) = (toSubmodule S).prod (toSubmodule S₁) := rfl

Submodule Structure of Product Subalgebra Equals Product of Submodule Structures

Informal description

For any subalgebras $S$ of an $R$-algebra $A$ and $S_1$ of an $R$-algebra $B$, the underlying submodule of the product subalgebra $S \times S_1$ is equal to the product of the underlying submodules of $S$ and $S_1$.

Subalgebra.mem_prod theorem

{S : Subalgebra R A} {S₁ : Subalgebra R B} {x : A × B} : x ∈ prod S S₁ ↔ x.1 ∈ S ∧ x.2 ∈ S₁

Full source

@[simp]
theorem mem_prod {S : Subalgebra R A} {S₁ : Subalgebra R B} {x : A × B} :
    x ∈ prod S S₁x ∈ prod S S₁ ↔ x.1 ∈ S ∧ x.2 ∈ S₁ := Set.mem_prod

Membership Condition for Product of Subalgebras: $x \in S \times S_1 \leftrightarrow x_1 \in S \land x_2 \in S_1$

Informal description

Let $R$ be a commutative semiring, and let $A$ and $B$ be $R$-algebras. For any subalgebras $S \subseteq A$ and $S_1 \subseteq B$, and any element $x = (x_1, x_2) \in A \times B$, we have $x \in S \times S_1$ if and only if $x_1 \in S$ and $x_2 \in S_1$.

Subalgebra.prod_top theorem

: (prod ⊤ ⊤ : Subalgebra R (A × B)) = ⊤

Full source

@[simp]
theorem prod_top : (prod ⊤ ⊤ : Subalgebra R (A × B)) = ⊤ := by ext; simp

Product of Top Subalgebras is Top Subalgebra of Product Algebra

Informal description

The product of the top subalgebras of $R$-algebras $A$ and $B$ is equal to the top subalgebra of the product algebra $A \times B$. In other words, $A \times B$ is the product of $A$ and $B$ as subalgebras.

Subalgebra.prod_mono theorem

{S T : Subalgebra R A} {S₁ T₁ : Subalgebra R B} : S ≤ T → S₁ ≤ T₁ → prod S S₁ ≤ prod T T₁

Full source

theorem prod_mono {S T : Subalgebra R A} {S₁ T₁ : Subalgebra R B} :
    S ≤ T → S₁ ≤ T₁ → prod S S₁ ≤ prod T T₁ :=
  Set.prod_mono

Monotonicity of Subalgebra Product with Respect to Inclusion

Informal description

Let $R$ be a commutative semiring, and let $A$ and $B$ be $R$-algebras. For any subalgebras $S, T \subseteq A$ and $S_1, T_1 \subseteq B$, if $S \subseteq T$ and $S_1 \subseteq T_1$, then the product subalgebra $S \times S_1$ is contained in the product subalgebra $T \times T_1$ as subalgebras of $A \times B$.

Subalgebra.prod_inf_prod theorem

{S T : Subalgebra R A} {S₁ T₁ : Subalgebra R B} : S.prod S₁ ⊓ T.prod T₁ = (S ⊓ T).prod (S₁ ⊓ T₁)

Full source

@[simp]
theorem prod_inf_prod {S T : Subalgebra R A} {S₁ T₁ : Subalgebra R B} :
    S.prod S₁ ⊓ T.prod T₁ = (S ⊓ T).prod (S₁ ⊓ T₁) :=
  SetLike.coe_injective Set.prod_inter_prod

Infimum of Product Subalgebras Equals Product of Infima

Informal description

For any subalgebras $S, T$ of an $R$-algebra $A$ and subalgebras $S_1, T_1$ of an $R$-algebra $B$, the infimum of the product subalgebras $S \times S_1$ and $T \times T_1$ in the product algebra $A \times B$ is equal to the product of the infima $(S \sqcap T) \times (S_1 \sqcap T_1)$. In symbols: $$ (S \times S_1) \sqcap (T \times T_1) = (S \sqcap T) \times (S_1 \sqcap T_1). $$

Main definitions