feat(measure_theory/group/arithmetic): add a section about opposite (…

…#10026)
leanprover-community · Oct 29, 2021 · 4f3443a · 4f3443a
1 parent 3f6174b
commit 4f3443a
Showing 1 changed file with 35 additions and 2 deletions.
diff --git a/src/measure_theory/group/arithmetic.lean b/src/measure_theory/group/arithmetic.lean
@@ -423,13 +423,13 @@ export has_measurable_vadd (measurable_const_vadd measurable_vadd_const)
   has_measurable_vadd₂ (measurable_vadd)
 
 @[to_additive]
-instance has_measurable_smul_of_mul (M : Type*) [monoid M] [measurable_space M]
+instance has_measurable_smul_of_mul (M : Type*) [has_mul M] [measurable_space M]
   [has_measurable_mul M] :
   has_measurable_smul M M :=
 ⟨measurable_id.const_mul, measurable_id.mul_const⟩
 
 @[to_additive]
-instance has_measurable_smul₂_of_mul (M : Type*) [monoid M] [measurable_space M]
+instance has_measurable_smul₂_of_mul (M : Type*) [has_mul M] [measurable_space M]
   [has_measurable_mul₂ M] :
   has_measurable_smul₂ M M :=
 ⟨measurable_mul⟩
@@ -539,6 +539,39 @@ lemma ae_measurable_const_smul_iff₀ {c : G₀} (hc : c ≠ 0) :
 
 end mul_action
 
+/-!
+### Opposite monoid
+-/
+
+section opposite
+open opposite
+
+instance {α : Type*} [h : measurable_space α] : measurable_space αᵒᵖ := measurable_space.map op h
+
+lemma measurable_op {α : Type*} [measurable_space α] : measurable (op : α → αᵒᵖ) := λ s, id
+
+lemma measurable_unop {α : Type*} [measurable_space α] : measurable (unop : αᵒᵖ → α) := λ s, id
+
+instance {M : Type*} [has_mul M] [measurable_space M] [has_measurable_mul M] :
+  has_measurable_mul Mᵒᵖ :=
+⟨λ c, measurable_op.comp (measurable_unop.mul_const _),
+  λ c, measurable_op.comp (measurable_unop.const_mul _)⟩
+
+instance {M : Type*} [has_mul M] [measurable_space M] [has_measurable_mul₂ M] :
+  has_measurable_mul₂ Mᵒᵖ :=
+⟨measurable_op.comp ((measurable_unop.comp measurable_snd).mul
+  (measurable_unop.comp measurable_fst))⟩
+
+instance has_measurable_smul_opposite_of_mul {M : Type*} [has_mul M] [measurable_space M]
+  [has_measurable_mul M] : has_measurable_smul Mᵒᵖ M :=
+⟨λ c, measurable_mul_const (unop c), λ x, measurable_unop.const_mul x⟩
+
+instance has_measurable_smul₂_opposite_of_mul {M : Type*} [has_mul M] [measurable_space M]
+  [has_measurable_mul₂ M] : has_measurable_smul₂ Mᵒᵖ M :=
+⟨measurable_snd.mul (measurable_unop.comp measurable_fst)⟩
+
+end opposite
+
 /-!
 ### Big operators: `∏` and `∑`
 -/