feat(algebra/algebra/subalgebra): add subalgebra.prod (#7782)

We add a basic API for product of subalgebras.

src/algebra/algebra/subalgebra.lean

@@ -621,6 +621,33 @@ by { ext, refl }
   (equiv_of_eq S T hST).trans (equiv_of_eq T U hTU) = equiv_of_eq S U (trans hST hTU) :=
 rfl
 
+section prod
+
+variables (S₁ : subalgebra R B)
+
+/-- The product of two subalgebras is a subalgebra. -/
+def prod : subalgebra R (A × B) :=
+{ carrier := set.prod S S₁,
+  algebra_map_mem' := λ r, ⟨algebra_map_mem _ _, algebra_map_mem _ _⟩,
+  .. S.to_subsemiring.prod S₁.to_subsemiring }
+
+@[simp] lemma coe_prod :
+  (prod S S₁ : set (A × B)) = set.prod S S₁ := rfl
+
+lemma prod_to_submodule :
+  (S.prod S₁).to_submodule = S.to_submodule.prod S₁.to_submodule := rfl
+
+@[simp] lemma mem_prod {S : subalgebra R A} {S₁ : subalgebra R B} {x : A × B} :
+  x ∈ prod S S₁ ↔ x.1 ∈ S ∧ x.2 ∈ S₁ := set.mem_prod
+
+@[simp] lemma prod_top : (prod ⊤ ⊤ : subalgebra R (A × B)) = ⊤ :=
+by ext; simp
+
+lemma 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
+
+end prod
+
 end subalgebra
 
 section nat

src/ring_theory/adjoin/basic.lean

@@ -55,6 +55,14 @@ le_antisymm (adjoin_le h₁) h₂
 theorem adjoin_eq (S : subalgebra R A) : adjoin R ↑S = S :=
 adjoin_eq_of_le _ (set.subset.refl _) subset_adjoin
 
+lemma coe_inf (S T : subalgebra R A) : (↑(S ⊓ T) : set A) = (S : set A) ∩ (T : set A) :=
+begin
+  apply le_antisymm,
+  { simp },
+  { rw ←galois_insertion.l_inf_u (@algebra.gi R A _ _ _),
+    exact algebra.subset_adjoin }
+end
+
 variables (R A)
 @[simp] theorem adjoin_empty : adjoin R (∅ : set A) = ⊥ :=
 show adjoin R ⊥ = ⊥, by { apply galois_connection.l_bot, exact algebra.gc }
@@ -98,6 +106,18 @@ le_antisymm
     ⟨subset_adjoin (set.mem_insert _ _), adjoin_mono (set.subset_insert _ _)⟩))
   (algebra.adjoin_mono (set.insert_subset_insert algebra.subset_adjoin))
 
+lemma adjoint_prod_le (s : set A) (t : set B) :
+  adjoin R (set.prod s t) ≤ (adjoin R s).prod (adjoin R t) :=
+adjoin_le $ set.prod_mono subset_adjoin subset_adjoin
+
+@[simp] lemma prod_inf_prod {S T : subalgebra R A} {S₁ T₁ : subalgebra R B} :
+  S.prod S₁ ⊓ T.prod T₁ = (S ⊓ T).prod (S₁ ⊓ T₁) :=
+begin
+  refine set_like.coe_injective _,
+  rw [subalgebra.coe_prod, coe_inf, coe_inf, coe_inf, subalgebra.coe_prod, subalgebra.coe_prod,
+    set.prod_inter_prod]
+end
+
 end semiring
 
 section comm_semiring