feat: Add lattice lemmas about Sub{group,monoid}.{op,unop} (#9860)

In fact I only need the `closure` lemma, but the others are easy enough.

This changes the `opEquiv`s to be order isomorphisms rather than just `Equiv`s.

Mathlib/GroupTheory/SchurZassenhaus.lean

@@ -86,8 +86,8 @@ theorem smul_diff' (h : H) :
   rw [diff, diff, index_eq_card, ← Finset.card_univ, ← Finset.prod_const, ← Finset.prod_mul_distrib]
   refine' Finset.prod_congr rfl fun q _ => _
   simp_rw [Subtype.ext_iff, MonoidHom.id_apply, coe_mul, mul_assoc, mul_right_inj]
-  rw [smul_apply_eq_smul_apply_inv_smul, smul_eq_mul_unop, unop_op, mul_left_inj, ← Subtype.ext_iff,
-    Equiv.apply_eq_iff_eq, inv_smul_eq_iff]
+  rw [smul_apply_eq_smul_apply_inv_smul, smul_eq_mul_unop, MulOpposite.unop_op, mul_left_inj,
+    ← Subtype.ext_iff, Equiv.apply_eq_iff_eq, inv_smul_eq_iff]
   exact self_eq_mul_right.mpr ((QuotientGroup.eq_one_iff _).mpr h.2)
 #align subgroup.smul_diff' Subgroup.smul_diff'
 

Mathlib/GroupTheory/Subgroup/MulOpposite.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2022 Alex Kontorovich. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Alex Kontorovich
+Authors: Alex Kontorovich, Eric Wieser
 -/
 import Mathlib.Logic.Encodable.Basic
 import Mathlib.GroupTheory.Subgroup.Basic
@@ -18,7 +18,7 @@ subgroup, subgroups
 -/
 
 
-variable {G : Type*} [Group G]
+variable {ι : Sort*} {G : Type*} [Group G]
 
 namespace Subgroup
 
@@ -31,6 +31,13 @@ protected def op (H : Subgroup G) : Subgroup Gᵐᵒᵖ where
   mul_mem' ha hb := H.mul_mem hb ha
   inv_mem' := H.inv_mem
 
+@[to_additive (attr := simp)]
+theorem mem_op {x : Gᵐᵒᵖ} {S : Subgroup G} : x ∈ S.op ↔ x.unop ∈ S := Iff.rfl
+
+@[to_additive (attr := simp)] lemma op_toSubmonoid (H : Subgroup G) :
+    H.op.toSubmonoid = H.toSubmonoid.op :=
+  rfl
+
 /-- Pull an opposite subgroup back to a subgroup along `MulOpposite.op`-/
 @[to_additive (attr := simps)
 "Pull an opposite additive subgroup back to an additive subgroup along `AddOpposite.op`"]
@@ -40,25 +47,118 @@ protected def unop (H : Subgroup Gᵐᵒᵖ) : Subgroup G where
   mul_mem' := fun ha hb => H.mul_mem hb ha
   inv_mem' := H.inv_mem
 
-@[to_additive (attr := simp, nolint simpNF)] lemma op_toSubmonoid (H : Subgroup G) :
-    H.op.toSubmonoid = H.toSubmonoid.op :=
-  rfl
+@[to_additive (attr := simp)]
+theorem mem_unop {x : G} {S : Subgroup Gᵐᵒᵖ} : x ∈ S.unop ↔ MulOpposite.op x ∈ S := Iff.rfl
 
-@[to_additive (attr := simp, nolint simpNF)] lemma unop_toSubmonoid (H : Subgroup Gᵐᵒᵖ) :
+@[to_additive (attr := simp)] lemma unop_toSubmonoid (H : Subgroup Gᵐᵒᵖ) :
     H.unop.toSubmonoid = H.toSubmonoid.unop :=
   rfl
 
+@[to_additive (attr := simp)]
+theorem unop_op (S : Subgroup G) : S.op.unop = S := rfl
+
+@[to_additive (attr := simp)]
+theorem op_unop (S : Subgroup Gᵐᵒᵖ) : S.unop.op = S := rfl
+
+/-! ### Lattice results -/
+
+@[to_additive]
+theorem op_le_iff {S₁ : Subgroup G} {S₂ : Subgroup Gᵐᵒᵖ} : S₁.op ≤ S₂ ↔ S₁ ≤ S₂.unop :=
+  MulOpposite.op_surjective.forall
+
+@[to_additive]
+theorem le_op_iff {S₁ : Subgroup Gᵐᵒᵖ} {S₂ : Subgroup G} : S₁ ≤ S₂.op ↔ S₁.unop ≤ S₂ :=
+  MulOpposite.op_surjective.forall
+
+@[to_additive (attr := simp)]
+theorem op_le_op_iff {S₁ S₂ : Subgroup G} : S₁.op ≤ S₂.op ↔ S₁ ≤ S₂ :=
+  MulOpposite.op_surjective.forall
+
+@[to_additive (attr := simp)]
+theorem unop_le_unop_iff {S₁ S₂ : Subgroup Gᵐᵒᵖ} : S₁.unop ≤ S₂.unop ↔ S₁ ≤ S₂ :=
+  MulOpposite.unop_surjective.forall
+
 /-- A subgroup `H` of `G` determines a subgroup `H.op` of the opposite group `Gᵐᵒᵖ`. -/
 @[to_additive (attr := simps) "An additive subgroup `H` of `G` determines an additive subgroup
 `H.op` of the opposite additive group `Gᵃᵒᵖ`."]
-def opEquiv : Subgroup G ≃ Subgroup Gᵐᵒᵖ where
+def opEquiv : Subgroup G ≃o Subgroup Gᵐᵒᵖ where
   toFun := Subgroup.op
   invFun := Subgroup.unop
-  left_inv _ := SetLike.coe_injective rfl
-  right_inv _ := SetLike.coe_injective rfl
+  left_inv := unop_op
+  right_inv := op_unop
+  map_rel_iff' := op_le_op_iff
 #align subgroup.opposite Subgroup.opEquiv
 #align add_subgroup.opposite AddSubgroup.opEquiv
 
+@[to_additive (attr := simp)]
+theorem op_bot : (⊥ : Subgroup G).op = ⊥ := opEquiv.map_bot
+
+@[to_additive (attr := simp)]
+theorem unop_bot : (⊥ : Subgroup Gᵐᵒᵖ).unop = ⊥ := opEquiv.symm.map_bot
+
+@[to_additive (attr := simp)]
+theorem op_top : (⊤ : Subgroup G).op = ⊤ := opEquiv.map_top
+
+@[to_additive (attr := simp)]
+theorem unop_top : (⊤ : Subgroup Gᵐᵒᵖ).unop = ⊤ := opEquiv.symm.map_top
+
+@[to_additive]
+theorem op_sup (S₁ S₂ : Subgroup G) : (S₁ ⊔ S₂).op = S₁.op ⊔ S₂.op :=
+  opEquiv.map_sup _ _
+
+@[to_additive]
+theorem unop_sup (S₁ S₂ : Subgroup Gᵐᵒᵖ) : (S₁ ⊔ S₂).unop = S₁.unop ⊔ S₂.unop :=
+  opEquiv.symm.map_sup _ _
+
+@[to_additive]
+theorem op_inf (S₁ S₂ : Subgroup G) : (S₁ ⊓ S₂).op = S₁.op ⊓ S₂.op := opEquiv.map_inf _ _
+
+@[to_additive]
+theorem unop_inf (S₁ S₂ : Subgroup Gᵐᵒᵖ) : (S₁ ⊓ S₂).unop = S₁.unop ⊓ S₂.unop :=
+  opEquiv.symm.map_inf _ _
+
+@[to_additive]
+theorem op_sSup (S : Set (Subgroup G)) : (sSup S).op = sSup (.unop ⁻¹' S) :=
+  opEquiv.map_sSup_eq_sSup_symm_preimage _
+
+@[to_additive]
+theorem unop_sSup (S : Set (Subgroup Gᵐᵒᵖ)) : (sSup S).unop = sSup (.op ⁻¹' S) :=
+  opEquiv.symm.map_sSup_eq_sSup_symm_preimage _
+
+@[to_additive]
+theorem op_sInf (S : Set (Subgroup G)) : (sInf S).op = sInf (.unop ⁻¹' S) :=
+  opEquiv.map_sInf_eq_sInf_symm_preimage _
+
+@[to_additive]
+theorem unop_sInf (S : Set (Subgroup Gᵐᵒᵖ)) : (sInf S).unop = sInf (.op ⁻¹' S) :=
+  opEquiv.symm.map_sInf_eq_sInf_symm_preimage _
+
+@[to_additive]
+theorem op_iSup (S : ι → Subgroup G) : (iSup S).op = ⨆ i, (S i).op := opEquiv.map_iSup _
+
+@[to_additive]
+theorem unop_iSup (S : ι → Subgroup Gᵐᵒᵖ) : (iSup S).unop = ⨆ i, (S i).unop :=
+  opEquiv.symm.map_iSup _
+
+@[to_additive]
+theorem op_iInf (S : ι → Subgroup G) : (iInf S).op = ⨅ i, (S i).op := opEquiv.map_iInf _
+
+@[to_additive]
+theorem unop_iInf (S : ι → Subgroup Gᵐᵒᵖ) : (iInf S).unop = ⨅ i, (S i).unop :=
+  opEquiv.symm.map_iInf _
+
+@[to_additive]
+theorem op_closure (s : Set G) : (closure s).op = closure (MulOpposite.unop ⁻¹' s) := by
+  simp_rw [closure, op_sInf, Set.preimage_setOf_eq, Subgroup.unop_coe]
+  congr with a
+  exact MulOpposite.unop_surjective.forall
+
+@[to_additive]
+theorem unop_closure (s : Set Gᵐᵒᵖ) : (closure s).unop = closure (MulOpposite.op ⁻¹' s) := by
+  simp_rw [closure, unop_sInf, Set.preimage_setOf_eq, Subgroup.op_coe]
+  congr with a
+  exact MulOpposite.op_surjective.forall
+
 /-- Bijection between a subgroup `H` and its opposite. -/
 @[to_additive (attr := simps!) "Bijection between an additive subgroup `H` and its opposite."]
 def equivOp (H : Subgroup G) : H ≃ H.op :=

Mathlib/GroupTheory/Submonoid/MulOpposite.lean

@@ -13,34 +13,134 @@ For every monoid `M`, we construct an equivalence between submonoids of `M` and
 
 -/
 
-variable {M : Type*} [MulOneClass M]
+variable {ι : Sort*} {M : Type*} [MulOneClass M]
 
 namespace Submonoid
 
 /-- Pull a submonoid back to an opposite submonoid along `MulOpposite.unop`-/
 @[to_additive (attr := simps) "Pull an additive submonoid back to an opposite submonoid along
 `AddOpposite.unop`"]
-protected def op {M : Type*} [MulOneClass M] (x : Submonoid M) : Submonoid (MulOpposite M) where
-  carrier := MulOpposite.unop ⁻¹' x.1
+protected def op (x : Submonoid M) : Submonoid Mᵐᵒᵖ where
+  carrier := MulOpposite.unop ⁻¹' x
   mul_mem' ha hb := x.mul_mem hb ha
   one_mem' := Submonoid.one_mem' _
 
+@[to_additive (attr := simp)]
+theorem mem_op {x : Mᵐᵒᵖ} {S : Submonoid M} : x ∈ S.op ↔ x.unop ∈ S := Iff.rfl
+
 /-- Pull an opposite submonoid back to a submonoid along `MulOpposite.op`-/
 @[to_additive (attr := simps) "Pull an opposite additive submonoid back to a submonoid along
 `AddOpposite.op`"]
-protected def unop {M : Type*} [MulOneClass M] (x : Submonoid (MulOpposite M)) : Submonoid M where
-  carrier := MulOpposite.op ⁻¹' x.1
+protected def unop (x : Submonoid Mᵐᵒᵖ) : Submonoid M where
+  carrier := MulOpposite.op ⁻¹' x
   mul_mem' ha hb := x.mul_mem hb ha
   one_mem' := Submonoid.one_mem' _
 
+@[to_additive (attr := simp)]
+theorem mem_unop {x : M} {S : Submonoid Mᵐᵒᵖ} : x ∈ S.unop ↔ MulOpposite.op x ∈ S := Iff.rfl
+
+@[to_additive (attr := simp)]
+theorem unop_op (S : Submonoid M) : S.op.unop = S := rfl
+
+@[to_additive (attr := simp)]
+theorem op_unop (S : Submonoid Mᵐᵒᵖ) : S.unop.op = S := rfl
+
+/-! ### Lattice results -/
+
+@[to_additive]
+theorem op_le_iff {S₁ : Submonoid M} {S₂ : Submonoid Mᵐᵒᵖ} : S₁.op ≤ S₂ ↔ S₁ ≤ S₂.unop :=
+  MulOpposite.op_surjective.forall
+
+@[to_additive]
+theorem le_op_iff {S₁ : Submonoid Mᵐᵒᵖ} {S₂ : Submonoid M} : S₁ ≤ S₂.op ↔ S₁.unop ≤ S₂ :=
+  MulOpposite.op_surjective.forall
+
+@[to_additive (attr := simp)]
+theorem op_le_op_iff {S₁ S₂ : Submonoid M} : S₁.op ≤ S₂.op ↔ S₁ ≤ S₂ :=
+  MulOpposite.op_surjective.forall
+
+@[to_additive (attr := simp)]
+theorem unop_le_unop_iff {S₁ S₂ : Submonoid Mᵐᵒᵖ} : S₁.unop ≤ S₂.unop ↔ S₁ ≤ S₂ :=
+  MulOpposite.unop_surjective.forall
+
 /-- A submonoid `H` of `G` determines a submonoid `H.op` of the opposite group `Gᵐᵒᵖ`. -/
 @[to_additive (attr := simps) "A additive submonoid `H` of `G` determines an additive submonoid
 `H.op` of the opposite group `Gᵐᵒᵖ`."]
-def opEquiv : Submonoid M ≃ Submonoid Mᵐᵒᵖ where
+def opEquiv : Submonoid M ≃o Submonoid Mᵐᵒᵖ where
   toFun := Submonoid.op
   invFun := Submonoid.unop
-  left_inv _ := SetLike.coe_injective rfl
-  right_inv _ := SetLike.coe_injective rfl
+  left_inv := unop_op
+  right_inv := op_unop
+  map_rel_iff' := op_le_op_iff
+
+@[to_additive (attr := simp)]
+theorem op_bot : (⊥ : Submonoid M).op = ⊥ := opEquiv.map_bot
+
+@[to_additive (attr := simp)]
+theorem unop_bot : (⊥ : Submonoid Mᵐᵒᵖ).unop = ⊥ := opEquiv.symm.map_bot
+
+@[to_additive (attr := simp)]
+theorem op_top : (⊤ : Submonoid M).op = ⊤ := opEquiv.map_top
+
+@[to_additive (attr := simp)]
+theorem unop_top : (⊤ : Submonoid Mᵐᵒᵖ).unop = ⊤ := opEquiv.symm.map_top
+
+@[to_additive]
+theorem op_sup (S₁ S₂ : Submonoid M) : (S₁ ⊔ S₂).op = S₁.op ⊔ S₂.op :=
+  opEquiv.map_sup _ _
+
+@[to_additive]
+theorem unop_sup (S₁ S₂ : Submonoid Mᵐᵒᵖ) : (S₁ ⊔ S₂).unop = S₁.unop ⊔ S₂.unop :=
+  opEquiv.symm.map_sup _ _
+
+@[to_additive]
+theorem op_inf (S₁ S₂ : Submonoid M) : (S₁ ⊓ S₂).op = S₁.op ⊓ S₂.op := opEquiv.map_inf _ _
+
+@[to_additive]
+theorem unop_inf (S₁ S₂ : Submonoid Mᵐᵒᵖ) : (S₁ ⊓ S₂).unop = S₁.unop ⊓ S₂.unop :=
+  opEquiv.symm.map_inf _ _
+
+@[to_additive]
+theorem op_sSup (S : Set (Submonoid M)) : (sSup S).op = sSup (.unop ⁻¹' S) :=
+  opEquiv.map_sSup_eq_sSup_symm_preimage _
+
+@[to_additive]
+theorem unop_sSup (S : Set (Submonoid Mᵐᵒᵖ)) : (sSup S).unop = sSup (.op ⁻¹' S) :=
+  opEquiv.symm.map_sSup_eq_sSup_symm_preimage _
+
+@[to_additive]
+theorem op_sInf (S : Set (Submonoid M)) : (sInf S).op = sInf (.unop ⁻¹' S) :=
+  opEquiv.map_sInf_eq_sInf_symm_preimage _
+
+@[to_additive]
+theorem unop_sInf (S : Set (Submonoid Mᵐᵒᵖ)) : (sInf S).unop = sInf (.op ⁻¹' S) :=
+  opEquiv.symm.map_sInf_eq_sInf_symm_preimage _
+
+@[to_additive]
+theorem op_iSup (S : ι → Submonoid M) : (iSup S).op = ⨆ i, (S i).op := opEquiv.map_iSup _
+
+@[to_additive]
+theorem unop_iSup (S : ι → Submonoid Mᵐᵒᵖ) : (iSup S).unop = ⨆ i, (S i).unop :=
+  opEquiv.symm.map_iSup _
+
+@[to_additive]
+theorem op_iInf (S : ι → Submonoid M) : (iInf S).op = ⨅ i, (S i).op := opEquiv.map_iInf _
+
+@[to_additive]
+theorem unop_iInf (S : ι → Submonoid Mᵐᵒᵖ) : (iInf S).unop = ⨅ i, (S i).unop :=
+  opEquiv.symm.map_iInf _
+
+@[to_additive]
+theorem op_closure (s : Set M) : (closure s).op = closure (MulOpposite.unop ⁻¹' s) := by
+  simp_rw [closure, op_sInf, Set.preimage_setOf_eq, Submonoid.unop_coe]
+  congr with a
+  exact MulOpposite.unop_surjective.forall
+
+@[to_additive]
+theorem unop_closure (s : Set Mᵐᵒᵖ) : (closure s).unop = closure (MulOpposite.op ⁻¹' s) := by
+  simp_rw [closure, unop_sInf, Set.preimage_setOf_eq, Submonoid.op_coe]
+  congr with a
+  exact MulOpposite.op_surjective.forall
 
 /-- Bijection between a submonoid `H` and its opposite. -/
 @[to_additive (attr := simps!) "Bijection between an additive submonoid `H` and its opposite."]

Mathlib/Order/CompleteLattice.lean

@@ -8,7 +8,7 @@ import Mathlib.Data.Nat.Set
 import Mathlib.Data.Set.Prod
 import Mathlib.Data.ULift
 import Mathlib.Order.Bounds.Basic
-import Mathlib.Order.Hom.Basic
+import Mathlib.Order.Hom.Set
 import Mathlib.Mathport.Notation
 
 #align_import order.complete_lattice from "leanprover-community/mathlib"@"5709b0d8725255e76f47debca6400c07b5c2d8e6"
@@ -1463,6 +1463,14 @@ theorem sInf_image {s : Set β} {f : β → α} : sInf (f '' s) = ⨅ a ∈ s, f
   @sSup_image αᵒᵈ _ _ _ _
 #align Inf_image sInf_image
 
+theorem OrderIso.map_sSup_eq_sSup_symm_preimage [CompleteLattice β] (f : α ≃o β) (s : Set α) :
+    f (sSup s) = sSup (f.symm ⁻¹' s) := by
+  rw [map_sSup, ← sSup_image, f.image_eq_preimage]
+
+theorem OrderIso.map_sInf_eq_sInf_symm_preimage [CompleteLattice β] (f : α ≃o β) (s : Set α) :
+    f (sInf s) = sInf (f.symm ⁻¹' s) := by
+  rw [map_sInf, ← sInf_image, f.image_eq_preimage]
+
 /-
 ### iSup and iInf under set constructions
 -/