feat(algebra/algebra/operations): submodule.map_pow and opposite le…

…mmas (#12374)

To prove `map_pow`, we add `submodule.map_hom` to match the very-recently-added `ideal.map_hom`. 

The opposite lemmas can be used to extend these results for maps that reverse multiplication, by factoring them into an `alg_hom` into the opposite type composed with `mul_opposite.op`.

`(↑(op_linear_equiv R : A ≃ₗ[R] Aᵐᵒᵖ) : A →ₗ[R] Aᵐᵒᵖ)` is really a mouthful, but the elaborator can't seem to work out the type any other way, and `.to_linear_map` appears not to be the preferred form for `simp` lemmas.

src/algebra/algebra/operations.lean

@@ -5,6 +5,7 @@ Authors: Kenny Lau
 -/
 import algebra.algebra.bilinear
 import algebra.module.submodule_pointwise
+import algebra.module.opposites
 
 /-!
 # Multiplication and division of submodules of an algebra.
@@ -30,7 +31,7 @@ multiplication of submodules, division of subodules, submodule semiring
 
 universes uι u v
 
-open algebra set
+open algebra set mul_opposite
 open_locale big_operators
 open_locale pointwise
 
@@ -67,6 +68,26 @@ end
 theorem one_le : (1 : submodule R A) ≤ P ↔ (1 : A) ∈ P :=
 by simpa only [one_eq_span, span_le, set.singleton_subset_iff]
 
+protected lemma map_one {A'} [semiring A'] [algebra R A'] (f : A →ₐ[R] A') :
+  map f.to_linear_map (1 : submodule R A) = 1 :=
+by { ext, simp }
+
+@[simp] lemma map_op_one :
+  map (↑(op_linear_equiv R : A ≃ₗ[R] Aᵐᵒᵖ) : A →ₗ[R] Aᵐᵒᵖ) (1 : submodule R A) = 1 :=
+by { ext, induction x using mul_opposite.rec, simp }
+
+@[simp] lemma comap_op_one :
+  comap (↑(op_linear_equiv R : A ≃ₗ[R] Aᵐᵒᵖ) : A →ₗ[R] Aᵐᵒᵖ) (1 : submodule R Aᵐᵒᵖ) = 1 :=
+by { ext, simp }
+
+@[simp] lemma map_unop_one :
+  map (↑(op_linear_equiv R : A ≃ₗ[R] Aᵐᵒᵖ).symm : Aᵐᵒᵖ →ₗ[R] A) (1 : submodule R Aᵐᵒᵖ) = 1 :=
+by rw [←comap_equiv_eq_map_symm, comap_op_one]
+
+@[simp] lemma comap_unop_one :
+  comap (↑(op_linear_equiv R : A ≃ₗ[R] Aᵐᵒᵖ).symm : Aᵐᵒᵖ →ₗ[R] A) (1 : submodule R A) = 1 :=
+by rw [←map_equiv_eq_comap_symm, map_op_one]
+
 /-- Multiplication of sub-R-modules of an R-algebra A. The submodule `M * N` is the
 smallest R-submodule of `A` containing the elements `m * n` for `m ∈ M` and `n ∈ N`. -/
 instance : has_mul (submodule R A) :=
@@ -172,7 +193,7 @@ le_antisymm (mul_le.2 $ λ mn hmn p hp, let ⟨m, hm, n, hn, hmn⟩ := mem_sup.1
 lemma mul_subset_mul : (↑M : set A) * (↑N : set A) ⊆ (↑(M * N) : set A) :=
 by { rintros _ ⟨i, j, hi, hj, rfl⟩, exact mul_mem_mul hi hj }
 
-lemma map_mul {A'} [semiring A'] [algebra R A'] (f : A →ₐ[R] A') :
+protected lemma map_mul {A'} [semiring A'] [algebra R A'] (f : A →ₐ[R] A') :
   map f.to_linear_map (M * N) = map f.to_linear_map M * map f.to_linear_map N :=
 calc map f.to_linear_map (M * N)
     = ⨆ (i : M), (N.map (lmul R A i)).map f.to_linear_map : map_supr _ _
@@ -193,6 +214,28 @@ calc map f.to_linear_map (M * N)
       simp [fy_eq] }
 end
 
+lemma map_op_mul :
+  map (↑(op_linear_equiv R : A ≃ₗ[R] Aᵐᵒᵖ) : A →ₗ[R] Aᵐᵒᵖ) (M * N) =
+    map (↑(op_linear_equiv R : A ≃ₗ[R] Aᵐᵒᵖ) : A →ₗ[R] Aᵐᵒᵖ) N *
+      map (↑(op_linear_equiv R : A ≃ₗ[R] Aᵐᵒᵖ) : A →ₗ[R] Aᵐᵒᵖ) M :=
+begin
+  apply le_antisymm,
+  { simp_rw map_le_iff_le_comap,
+    refine mul_le.2 (λ m hm n hn, _),
+    rw [mem_comap, map_equiv_eq_comap_symm, map_equiv_eq_comap_symm],
+    show op n * op m ∈ _,
+    exact mul_mem_mul hn hm },
+  { refine mul_le.2 (mul_opposite.rec $ λ m hm, mul_opposite.rec $ λ n hn, _),
+    rw submodule.mem_map_equiv at ⊢ hm hn,
+    exact mul_mem_mul hn hm, }
+end
+
+lemma comap_unop_mul :
+  comap (↑(op_linear_equiv R : A ≃ₗ[R] Aᵐᵒᵖ).symm : Aᵐᵒᵖ →ₗ[R] A) (M * N) =
+    comap (↑(op_linear_equiv R : A ≃ₗ[R] Aᵐᵒᵖ).symm : Aᵐᵒᵖ →ₗ[R] A) N *
+      comap (↑(op_linear_equiv R : A ≃ₗ[R] Aᵐᵒᵖ).symm : Aᵐᵒᵖ →ₗ[R] A) M :=
+by simp_rw [comap_equiv_eq_map_symm, linear_equiv.symm_symm, map_op_mul]
+
 section
 open_locale pointwise
 
@@ -320,6 +363,44 @@ protected theorem pow_induction_on
 submodule.pow_induction_on' M
   (by exact hr) (λ x y i hx hy, hadd x y) (λ m hm i x hx, hmul _ hm _) hx
 
+/-- `submonoid.map` as a `monoid_with_zero_hom`, when applied to `alg_hom`s. -/
+@[simps]
+def map_hom {A'} [semiring A'] [algebra R A'] (f : A →ₐ[R] A') :
+  submodule R A →*₀ submodule R A' :=
+{ to_fun := map f.to_linear_map,
+  map_zero' := submodule.map_bot _,
+  map_one' := submodule.map_one _,
+  map_mul' := λ _ _, submodule.map_mul _ _ _}
+
+/-- The ring of submodules of the opposite algebra is isomorphic to the opposite ring of
+submodules. -/
+@[simps]
+def equiv_opposite : submodule R Aᵐᵒᵖ ≃+* (submodule R A)ᵐᵒᵖ :=
+ring_equiv.symm
+{ to_fun := λ p, p.unop.comap (↑(op_linear_equiv R : A ≃ₗ[R] Aᵐᵒᵖ).symm : Aᵐᵒᵖ →ₗ[R] A),
+  inv_fun := λ p, op $ p.comap (↑(op_linear_equiv R : A ≃ₗ[R] Aᵐᵒᵖ) : A →ₗ[R] Aᵐᵒᵖ),
+  left_inv := λ p, unop_injective $ set_like.coe_injective rfl,
+  right_inv := λ p, set_like.coe_injective $ rfl,
+  map_add' := λ p q, by simp [comap_equiv_eq_map_symm],
+  map_mul' := λ p q, comap_unop_mul _ _ }
+
+protected lemma map_pow {A'} [semiring A'] [algebra R A'] (f : A →ₐ[R] A') (n : ℕ) :
+  map f.to_linear_map (M ^ n) = map f.to_linear_map M ^ n :=
+map_pow (map_hom f) M n
+
+lemma map_op_pow (n : ℕ) :
+  map (↑(op_linear_equiv R : A ≃ₗ[R] Aᵐᵒᵖ) : A →ₗ[R] Aᵐᵒᵖ) (M ^ n) =
+    map (↑(op_linear_equiv R : A ≃ₗ[R] Aᵐᵒᵖ) : A →ₗ[R] Aᵐᵒᵖ) M ^ n :=
+begin
+  rw [map_equiv_eq_comap_symm, map_equiv_eq_comap_symm],
+  exact (equiv_opposite : submodule R Aᵐᵒᵖ ≃+* _).symm.map_pow (op M) n,
+end
+
+lemma comap_unop_pow (n : ℕ) :
+  comap (↑(op_linear_equiv R : A ≃ₗ[R] Aᵐᵒᵖ).symm : Aᵐᵒᵖ →ₗ[R] A) (M ^ n) =
+    comap (↑(op_linear_equiv R : A ≃ₗ[R] Aᵐᵒᵖ).symm : Aᵐᵒᵖ →ₗ[R] A) M ^ n :=
+(equiv_opposite : submodule R Aᵐᵒᵖ ≃+* _).symm.map_pow (op M) n
+
 /-- `span` is a semiring homomorphism (recall multiplication is pointwise multiplication of subsets
 on either side). -/
 def span.ring_hom : set_semiring A →+* submodule R A :=
@@ -454,7 +535,7 @@ begin
   exact hn m hm,
 end
 
-@[simp] lemma map_div {B : Type*} [comm_ring B] [algebra R B]
+@[simp] protected lemma map_div {B : Type*} [comm_ring B] [algebra R B]
   (I J : submodule R A) (h : A ≃ₐ[R] B) :
   (I / J).map h.to_linear_map = I.map h.to_linear_map / J.map h.to_linear_map :=
 begin