Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit cd39118

Browse files
committed
feat(*/prod): prod_prod_prod equivs (#19235)
These send `((a, b), (c, d))` to `((a, c), (b, d))`, and this commit provides this bundled as `equiv`, `add_equiv`, `mul_equiv`, `ring_equiv`, and `linear_equiv`. We already have something analogous for `tensor_product`.
1 parent baa8830 commit cd39118

File tree

4 files changed

+82
-2
lines changed

4 files changed

+82
-2
lines changed

src/algebra/group/prod.lean

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -465,6 +465,26 @@ def prod_comm : M × N ≃* N × M :=
465465

466466
variables {M' N' : Type*} [mul_one_class M'] [mul_one_class N']
467467

468+
section
469+
variables (M N M' N')
470+
471+
/-- Four-way commutativity of `prod`. The name matches `mul_mul_mul_comm`. -/
472+
@[to_additive prod_prod_prod_comm "Four-way commutativity of `prod`.
473+
The name matches `mul_mul_mul_comm`", simps apply]
474+
def prod_prod_prod_comm : (M × N) × (M' × N') ≃* (M × M') × (N × N') :=
475+
{ to_fun := λ mnmn, ((mnmn.1.1, mnmn.2.1), (mnmn.1.2, mnmn.2.2)),
476+
inv_fun := λ mmnn, ((mmnn.1.1, mmnn.2.1), (mmnn.1.2, mmnn.2.2)),
477+
map_mul' := λ mnmn mnmn', rfl,
478+
..equiv.prod_prod_prod_comm M N M' N', }
479+
480+
@[simp, to_additive] lemma prod_prod_prod_comm_to_equiv :
481+
(prod_prod_prod_comm M N M' N').to_equiv = equiv.prod_prod_prod_comm M N M' N' := rfl
482+
483+
@[simp] lemma prod_prod_prod_comm_symm :
484+
(prod_prod_prod_comm M N M' N').symm = prod_prod_prod_comm M M' N N' := rfl
485+
486+
end
487+
468488
/--Product of multiplicative isomorphisms; the maps come from `equiv.prod_congr`.-/
469489
@[to_additive prod_congr "Product of additive isomorphisms; the maps come from `equiv.prod_congr`."]
470490
def prod_congr (f : M ≃* M') (g : N ≃* N') : M × N ≃* M' × N' :=

src/algebra/ring/prod.lean

Lines changed: 28 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -212,7 +212,9 @@ end prod_map
212212
end ring_hom
213213

214214
namespace ring_equiv
215-
variables {R S} [non_assoc_semiring R] [non_assoc_semiring S]
215+
variables {R S R' S'}
216+
variables [non_assoc_semiring R] [non_assoc_semiring S]
217+
variables [non_assoc_semiring R'] [non_assoc_semiring S']
216218

217219
/-- Swapping components as an equivalence of (semi)rings. -/
218220
def prod_comm : R × S ≃+* S × R :=
@@ -229,6 +231,31 @@ ring_hom.ext $ λ _, rfl
229231
(ring_hom.snd S R).comp ↑(prod_comm : R × S ≃+* S × R) = ring_hom.fst R S :=
230232
ring_hom.ext $ λ _, rfl
231233

234+
section
235+
variables (R R' S S')
236+
237+
/-- Four-way commutativity of `prod`. The name matches `mul_mul_mul_comm`. -/
238+
@[simps apply]
239+
def prod_prod_prod_comm : (R × R') × (S × S') ≃+* (R × S) × (R' × S') :=
240+
{ to_fun := λ rrss, ((rrss.1.1, rrss.2.1), (rrss.1.2, rrss.2.2)),
241+
inv_fun := λ rsrs, ((rsrs.1.1, rsrs.2.1), (rsrs.1.2, rsrs.2.2)),
242+
.. add_equiv.prod_prod_prod_comm R R' S S',
243+
.. mul_equiv.prod_prod_prod_comm R R' S S' }
244+
245+
@[simp] lemma prod_prod_prod_comm_symm :
246+
(prod_prod_prod_comm R R' S S').symm = prod_prod_prod_comm R S R' S' := rfl
247+
248+
@[simp] lemma prod_prod_prod_comm_to_add_equiv :
249+
(prod_prod_prod_comm R R' S S').to_add_equiv = add_equiv.prod_prod_prod_comm R R' S S' := rfl
250+
251+
@[simp] lemma prod_prod_prod_comm_to_mul_equiv :
252+
(prod_prod_prod_comm R R' S S').to_mul_equiv = mul_equiv.prod_prod_prod_comm R R' S S' := rfl
253+
254+
@[simp] lemma prod_prod_prod_comm_to_equiv :
255+
(prod_prod_prod_comm R R' S S').to_equiv = equiv.prod_prod_prod_comm R R' S S' := rfl
256+
257+
end
258+
232259
variables (R S) [subsingleton S]
233260

234261
/-- A ring `R` is isomorphic to `R × S` when `S` is the zero ring -/

src/linear_algebra/prod.lean

Lines changed: 23 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -227,7 +227,7 @@ def prod_map (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₄) : (M × M₂) →
227227

228228
lemma coe_prod_map (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₄) :
229229
⇑(f.prod_map g) = prod.map f g := rfl
230-
230+
231231
@[simp] theorem prod_map_apply (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₄) (x) :
232232
f.prod_map g x = (f x.1, g x.2) := rfl
233233

@@ -559,6 +559,28 @@ def prod_comm (R M N : Type*) [semiring R] [add_comm_monoid M] [add_comm_monoid
559559
map_smul' := λ r ⟨m, n⟩, rfl,
560560
..add_equiv.prod_comm }
561561

562+
section
563+
variables (R M M₂ M₃ M₄)
564+
variables [semiring R]
565+
variables [add_comm_monoid M] [add_comm_monoid M₂] [add_comm_monoid M₃] [add_comm_monoid M₄]
566+
variables [module R M] [module R M₂] [module R M₃] [module R M₄]
567+
568+
/-- Four-way commutativity of `prod`. The name matches `mul_mul_mul_comm`. -/
569+
@[simps apply]
570+
def prod_prod_prod_comm : ((M × M₂) × (M₃ × M₄)) ≃ₗ[R] (M × M₃) × (M₂ × M₄) :=
571+
{ to_fun := λ mnmn, ((mnmn.1.1, mnmn.2.1), (mnmn.1.2, mnmn.2.2)),
572+
inv_fun := λ mmnn, ((mmnn.1.1, mmnn.2.1), (mmnn.1.2, mmnn.2.2)),
573+
map_smul' := λ c mnmn, rfl,
574+
..add_equiv.prod_prod_prod_comm M M₂ M₃ M₄ }
575+
576+
@[simp] lemma prod_prod_prod_comm_symm :
577+
(prod_prod_prod_comm R M M₂ M₃ M₄).symm = prod_prod_prod_comm R M M₃ M₂ M₄ := rfl
578+
579+
@[simp] lemma prod_prod_prod_comm_to_add_equiv :
580+
(prod_prod_prod_comm R M M₂ M₃ M₄).to_add_equiv = add_equiv.prod_prod_prod_comm M M₂ M₃ M₄ := rfl
581+
582+
end
583+
562584
section
563585

564586
variables [semiring R]

src/logic/equiv/basic.lean

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -105,6 +105,17 @@ def prod_comm (α β : Type*) : α × β ≃ β × α :=
105105
@[simps] def prod_assoc (α β γ : Sort*) : (α × β) × γ ≃ α × (β × γ) :=
106106
⟨λ p, (p.1.1, p.1.2, p.2), λ p, ((p.1, p.2.1), p.2.2), λ ⟨⟨a, b⟩, c⟩, rfl, λ ⟨a, ⟨b, c⟩⟩, rfl⟩
107107

108+
/-- Four-way commutativity of `prod`. The name matches `mul_mul_mul_comm`. -/
109+
@[simps apply]
110+
def prod_prod_prod_comm (α β γ δ : Type*) : (α × β) × (γ × δ) ≃ (α × γ) × (β × δ) :=
111+
{ to_fun := λ abcd, ((abcd.1.1, abcd.2.1), (abcd.1.2, abcd.2.2)),
112+
inv_fun := λ acbd, ((acbd.1.1, acbd.2.1), (acbd.1.2, acbd.2.2)),
113+
left_inv := λ ⟨⟨a, b⟩, ⟨c, d⟩⟩, rfl,
114+
right_inv := λ ⟨⟨a, c⟩, ⟨b, d⟩⟩, rfl, }
115+
116+
@[simp] lemma prod_prod_prod_comm_symm (α β γ δ : Type*) :
117+
(prod_prod_prod_comm α β γ δ).symm = prod_prod_prod_comm α γ β δ := rfl
118+
108119
/-- Functions on `α × β` are equivalent to functions `α → β → γ`. -/
109120
@[simps {fully_applied := ff}] def curry (α β γ : Type*) :
110121
(α × β → γ) ≃ (α → β → γ) :=

0 commit comments

Comments
 (0)