Mathlib.Algebra.Group.Submonoid.MulOpposite

Submonoid.op definition

(x : Submonoid M) : Submonoid Mᵐᵒᵖ

Full source

/-- 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 (x : Submonoid M) : Submonoid Mᵐᵒᵖ where
  carrier := MulOpposite.unopMulOpposite.unop ⁻¹' x
  mul_mem' ha hb := x.mul_mem hb ha
  one_mem' := Submonoid.one_mem' _

Opposite submonoid

Informal description

Given a submonoid $S$ of a monoid $M$, the opposite submonoid $S^{\text{op}}$ is defined as the preimage of $S$ under the unary operation $\text{unop} : M^{\text{op}} \to M$, where $M^{\text{op}}$ is the opposite monoid of $M$. The opposite submonoid consists of all elements $x \in M^{\text{op}}$ such that $\text{unop}(x) \in S$, and it inherits the submonoid structure from $S$ with the multiplication order reversed.

Submonoid.mem_op theorem

{x : Mᵐᵒᵖ} {S : Submonoid M} : x ∈ S.op ↔ x.unop ∈ S

Full source

@[to_additive (attr := simp)]
theorem mem_op {x : Mᵐᵒᵖ} {S : Submonoid M} : x ∈ S.opx ∈ S.op ↔ x.unop ∈ S := Iff.rfl

Membership in Opposite Submonoid via Unopposite

Informal description

For any element $x$ in the opposite monoid $M^{\text{op}}$ and any submonoid $S$ of $M$, the element $x$ belongs to the opposite submonoid $S^{\text{op}}$ if and only if its unopposite $x^{\text{unop}}$ belongs to $S$.

Submonoid.unop definition

(x : Submonoid Mᵐᵒᵖ) : Submonoid M

Full source

/-- 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 (x : Submonoid Mᵐᵒᵖ) : Submonoid M where
  carrier := MulOpposite.opMulOpposite.op ⁻¹' x
  mul_mem' ha hb := x.mul_mem hb ha
  one_mem' := Submonoid.one_mem' _

Submonoid of the original monoid from an opposite submonoid

Informal description

Given a submonoid $S$ of the opposite monoid $M^{\text{op}}$, the submonoid $\text{unop}(S)$ is defined as the preimage of $S$ under the operation $\text{op} : M \to M^{\text{op}}$. It consists of all elements $x \in M$ such that $\text{op}(x) \in S$, and it inherits the submonoid structure from $S$ with the multiplication order reversed.

Submonoid.mem_unop theorem

{x : M} {S : Submonoid Mᵐᵒᵖ} : x ∈ S.unop ↔ MulOpposite.op x ∈ S

Full source

@[to_additive (attr := simp)]
theorem mem_unop {x : M} {S : Submonoid Mᵐᵒᵖ} : x ∈ S.unopx ∈ S.unop ↔ MulOpposite.op x ∈ S := Iff.rfl

Membership Criterion for Submonoid of Opposite Monoid

Informal description

For any element $x$ in a monoid $M$ and any submonoid $S$ of the opposite monoid $M^{\text{op}}$, the element $x$ belongs to the submonoid $\text{unop}(S)$ if and only if the opposite element $\text{op}(x)$ belongs to $S$.

Submonoid.unop_op theorem

(S : Submonoid M) : S.op.unop = S

Full source

@[to_additive (attr := simp)]
theorem unop_op (S : Submonoid M) : S.op.unop = S := rfl

Opposite-Unop Submonoid Identity: $(S^{\text{op}})^{\text{unop}} = S$

Informal description

For any submonoid $S$ of a monoid $M$, the submonoid obtained by first taking the opposite submonoid $S^{\text{op}}$ and then applying the unop operation is equal to the original submonoid $S$, i.e., $(S^{\text{op}})^{\text{unop}} = S$.

Submonoid.op_unop theorem

(S : Submonoid Mᵐᵒᵖ) : S.unop.op = S

Full source

@[to_additive (attr := simp)]
theorem op_unop (S : Submonoid Mᵐᵒᵖ) : S.unop.op = S := rfl

Opposite-Unop Submonoid Identity: $(S^{\text{unop}})^{\text{op}} = S$

Informal description

For any submonoid $S$ of the opposite monoid $M^{\text{op}}$, the opposite of the submonoid obtained by applying the $\text{unop}$ operation to $S$ is equal to $S$ itself, i.e., $(S^{\text{unop}})^{\text{op}} = S$.

Submonoid.op_le_iff theorem

{S₁ : Submonoid M} {S₂ : Submonoid Mᵐᵒᵖ} : S₁.op ≤ S₂ ↔ S₁ ≤ S₂.unop

Full source

@[to_additive]
theorem op_le_iff {S₁ : Submonoid M} {S₂ : Submonoid Mᵐᵒᵖ} : S₁.op ≤ S₂ ↔ S₁ ≤ S₂.unop :=
  MulOpposite.op_surjective.forall

Order Reversal in Opposite Submonoids: $S_1^{\text{op}} \leq S_2 \leftrightarrow S_1 \leq S_2^{\text{unop}}$

Informal description

For any submonoid $S_1$ of a monoid $M$ and any submonoid $S_2$ of the opposite monoid $M^{\text{op}}$, the opposite submonoid $S_1^{\text{op}}$ is contained in $S_2$ if and only if $S_1$ is contained in the unopposite submonoid $S_2^{\text{unop}}$. In other words, $S_1^{\text{op}} \leq S_2 \leftrightarrow S_1 \leq S_2^{\text{unop}}$.

Submonoid.le_op_iff theorem

{S₁ : Submonoid Mᵐᵒᵖ} {S₂ : Submonoid M} : S₁ ≤ S₂.op ↔ S₁.unop ≤ S₂

Full source

@[to_additive]
theorem le_op_iff {S₁ : Submonoid Mᵐᵒᵖ} {S₂ : Submonoid M} : S₁ ≤ S₂.op ↔ S₁.unop ≤ S₂ :=
  MulOpposite.op_surjective.forall

Inclusion of Opposite Submonoids is Equivalent to Inclusion of Unopposed Submonoids

Informal description

For any submonoid $S_1$ of the opposite monoid $M^{\text{op}}$ and any submonoid $S_2$ of $M$, the inclusion $S_1 \leq S_2^{\text{op}}$ holds if and only if $S_1^{\text{unop}} \leq S_2$.

Submonoid.op_le_op_iff theorem

{S₁ S₂ : Submonoid M} : S₁.op ≤ S₂.op ↔ S₁ ≤ S₂

Full source

@[to_additive (attr := simp)]
theorem op_le_op_iff {S₁ S₂ : Submonoid M} : S₁.op ≤ S₂.op ↔ S₁ ≤ S₂ :=
  MulOpposite.op_surjective.forall

Order Reversal in Opposite Submonoids: $S_1^{\text{op}} \leq S_2^{\text{op}} \leftrightarrow S_1 \leq S_2$

Informal description

For any two submonoids $S_1$ and $S_2$ of a monoid $M$, the opposite submonoid $S_1^{\text{op}}$ is contained in $S_2^{\text{op}}$ if and only if $S_1$ is contained in $S_2$. In other words, $S_1^{\text{op}} \leq S_2^{\text{op}} \leftrightarrow S_1 \leq S_2$.

Submonoid.unop_le_unop_iff theorem

{S₁ S₂ : Submonoid Mᵐᵒᵖ} : S₁.unop ≤ S₂.unop ↔ S₁ ≤ S₂

Full source

@[to_additive (attr := simp)]
theorem unop_le_unop_iff {S₁ S₂ : Submonoid Mᵐᵒᵖ} : S₁.unop ≤ S₂.unop ↔ S₁ ≤ S₂ :=
  MulOpposite.unop_surjective.forall

Order Reversal in Opposite Submonoids: $S₁.\text{unop} \leq S₂.\text{unop} \leftrightarrow S₁ \leq S₂$

Informal description

For any two submonoids $S₁$ and $S₂$ of the opposite monoid $M^{\text{op}}$, the inequality $S₁.\text{unop} \leq S₂.\text{unop}$ holds if and only if $S₁ \leq S₂$ in $M^{\text{op}}$.

Submonoid.opEquiv definition

: Submonoid M ≃o Submonoid Mᵐᵒᵖ

Full source

/-- 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 : SubmonoidSubmonoid M ≃o Submonoid Mᵐᵒᵖ where
  toFun := Submonoid.op
  invFun := Submonoid.unop
  left_inv := unop_op
  right_inv := op_unop
  map_rel_iff' := op_le_op_iff

Order isomorphism between submonoids of a monoid and its opposite

Informal description

The order isomorphism $\text{Submonoid}\, M \simeq_o \text{Submonoid}\, M^{\text{op}}$ between the lattice of submonoids of a monoid $M$ and the lattice of submonoids of its opposite monoid $M^{\text{op}}$. The isomorphism is given by the maps $\text{op}$ and $\text{unop}$, which preserve the order structure and satisfy $\text{unop} \circ \text{op} = \text{id}$ and $\text{op} \circ \text{unop} = \text{id}$.

Submonoid.op_injective theorem

: (@Submonoid.op M _).Injective

Full source

@[to_additive]
theorem op_injective : (@Submonoid.op M _).Injective := opEquiv.injective

Injectivity of the Opposite Submonoid Map

Informal description

The map $\text{op} : \text{Submonoid}\, M \to \text{Submonoid}\, M^{\text{op}}$ is injective. That is, for any two submonoids $S, T$ of $M$, if $S^{\text{op}} = T^{\text{op}}$, then $S = T$.

Submonoid.unop_injective theorem

: (@Submonoid.unop M _).Injective

Full source

@[to_additive]
theorem unop_injective : (@Submonoid.unop M _).Injective := opEquiv.symm.injective

Injectivity of the Unop Operation on Submonoids of Opposite Monoids

Informal description

The function $\text{unop} : \text{Submonoid}\, M^{\text{op}} \to \text{Submonoid}\, M$ is injective. That is, for any submonoids $S, T$ of $M^{\text{op}}$, if $\text{unop}(S) = \text{unop}(T)$, then $S = T$.

Submonoid.op_inj theorem

{S T : Submonoid M} : S.op = T.op ↔ S = T

Full source

@[to_additive (attr := simp)]
theorem op_inj {S T : Submonoid M} : S.op = T.op ↔ S = T := opEquiv.eq_iff_eq

Equality of Opposite Submonoids is Equivalent to Equality of Original Submonoids

Informal description

For any two submonoids $S$ and $T$ of a monoid $M$, the opposite submonoids $S^{\text{op}}$ and $T^{\text{op}}$ are equal if and only if $S$ and $T$ are equal.

Submonoid.unop_inj theorem

{S T : Submonoid Mᵐᵒᵖ} : S.unop = T.unop ↔ S = T

Full source

@[to_additive (attr := simp)]
theorem unop_inj {S T : Submonoid Mᵐᵒᵖ} : S.unop = T.unop ↔ S = T := opEquiv.symm.eq_iff_eq

Injectivity of the Unop Operation on Submonoids of the Opposite Monoid

Informal description

For any two submonoids $S$ and $T$ of the opposite monoid $M^{\text{op}}$, the equality $S.\text{unop} = T.\text{unop}$ holds if and only if $S = T$.

Submonoid.op_bot theorem

: (⊥ : Submonoid M).op = ⊥

Full source

@[to_additive (attr := simp)]
theorem op_bot : (⊥ : Submonoid M).op = ⊥ := opEquiv.map_bot

Opposite of Trivial Submonoid is Trivial: $(\bot)^{\text{op}} = \bot$

Informal description

The opposite of the trivial submonoid $\{1\}$ of a monoid $M$ is equal to the trivial submonoid of the opposite monoid $M^{\text{op}}$, i.e., $(\bot : \text{Submonoid}\, M)^{\text{op}} = \bot$.

Submonoid.op_eq_bot theorem

{S : Submonoid M} : S.op = ⊥ ↔ S = ⊥

Full source

@[to_additive (attr := simp)]
theorem op_eq_bot {S : Submonoid M} : S.op = ⊥ ↔ S = ⊥ := op_injective.eq_iff' op_bot

Opposite Submonoid is Trivial if and only if Original Submonoid is Trivial: $S^{\text{op}} = \bot \leftrightarrow S = \bot$

Informal description

For any submonoid $S$ of a monoid $M$, the opposite submonoid $S^{\text{op}}$ is equal to the trivial submonoid $\{1\}$ of $M^{\text{op}}$ if and only if $S$ is the trivial submonoid of $M$.

Submonoid.unop_bot theorem

: (⊥ : Submonoid Mᵐᵒᵖ).unop = ⊥

Full source

@[to_additive (attr := simp)]
theorem unop_bot : (⊥ : Submonoid Mᵐᵒᵖ).unop = ⊥ := opEquiv.symm.map_bot

Unopposite of Bottom Submonoid is Bottom Submonoid

Informal description

The unopposite of the bottom submonoid of the opposite monoid $M^{\text{op}}$ is equal to the bottom submonoid of $M$, i.e., $\text{unop}(\bot) = \bot$.

Submonoid.unop_eq_bot theorem

{S : Submonoid Mᵐᵒᵖ} : S.unop = ⊥ ↔ S = ⊥

Full source

@[to_additive (attr := simp)]
theorem unop_eq_bot {S : Submonoid Mᵐᵒᵖ} : S.unop = ⊥ ↔ S = ⊥ := unop_injective.eq_iff' unop_bot

Triviality Criterion for Unopposite Submonoids

Informal description

For any submonoid $S$ of the opposite monoid $M^{\text{op}}$, the unopposite submonoid $\text{unop}(S)$ is equal to the trivial submonoid $\bot$ if and only if $S$ itself is the trivial submonoid $\bot$. That is, $\text{unop}(S) = \bot \leftrightarrow S = \bot$.

Submonoid.op_top theorem

: (⊤ : Submonoid M).op = ⊤

Full source

@[to_additive (attr := simp)]
theorem op_top : (⊤ : Submonoid M).op = ⊤ := rfl

Opposite of Top Submonoid is Top Submonoid of Opposite Monoid

Informal description

The opposite of the top submonoid of a monoid $M$ is equal to the top submonoid of the opposite monoid $M^{\text{op}}$, i.e., $(\top : \text{Submonoid } M)^{\text{op}} = \top$.

Submonoid.op_eq_top theorem

{S : Submonoid M} : S.op = ⊤ ↔ S = ⊤

Full source

@[to_additive (attr := simp)]
theorem op_eq_top {S : Submonoid M} : S.op = ⊤ ↔ S = ⊤ := op_injective.eq_iff' op_top

Opposite Submonoid is Top if and only if Original Submonoid is Top

Informal description

For any submonoid $S$ of a monoid $M$, the opposite submonoid $S^{\text{op}}$ is equal to the top submonoid of $M^{\text{op}}$ if and only if $S$ is the top submonoid of $M$.

Submonoid.unop_top theorem

: (⊤ : Submonoid Mᵐᵒᵖ).unop = ⊤

Full source

@[to_additive (attr := simp)]
theorem unop_top : (⊤ : Submonoid Mᵐᵒᵖ).unop = ⊤ := rfl

Unopposite of Top Submonoid is Top

Informal description

The unopposite of the top submonoid of the opposite monoid $M^{\text{op}}$ is equal to the top submonoid of $M$.

Submonoid.unop_eq_top theorem

{S : Submonoid Mᵐᵒᵖ} : S.unop = ⊤ ↔ S = ⊤

Full source

@[to_additive (attr := simp)]
theorem unop_eq_top {S : Submonoid Mᵐᵒᵖ} : S.unop = ⊤ ↔ S = ⊤ := unop_injective.eq_iff' unop_top

Characterization of Top Submonoid via Unopposite Operation

Informal description

For any submonoid $S$ of the opposite monoid $M^{\text{op}}$, the unopposite submonoid $\text{unop}(S)$ is equal to the top submonoid of $M$ if and only if $S$ is the top submonoid of $M^{\text{op}}$.

Submonoid.op_sup theorem

(S₁ S₂ : Submonoid M) : (S₁ ⊔ S₂).op = S₁.op ⊔ S₂.op

Full source

@[to_additive]
theorem op_sup (S₁ S₂ : Submonoid M) : (S₁ ⊔ S₂).op = S₁.op ⊔ S₂.op :=
  opEquiv.map_sup _ _

Opposite Submonoid Preserves Supremum: $(S_1 \sqcup S_2)^{\text{op}} = S_1^{\text{op}} \sqcup S_2^{\text{op}}$

Informal description

For any two submonoids $S_1$ and $S_2$ of a monoid $M$, the opposite of their supremum $(S_1 \sqcup S_2)^{\text{op}}$ is equal to the supremum of their opposites $S_1^{\text{op}} \sqcup S_2^{\text{op}}$ in the opposite monoid $M^{\text{op}}$.

Submonoid.unop_sup theorem

(S₁ S₂ : Submonoid Mᵐᵒᵖ) : (S₁ ⊔ S₂).unop = S₁.unop ⊔ S₂.unop

Full source

@[to_additive]
theorem unop_sup (S₁ S₂ : Submonoid Mᵐᵒᵖ) : (S₁ ⊔ S₂).unop = S₁.unop ⊔ S₂.unop :=
  opEquiv.symm.map_sup _ _

Unop Preserves Supremum of Submonoids in Opposite Monoid

Informal description

For any two submonoids $S_1$ and $S_2$ of the opposite monoid $M^{\text{op}}$, the operation $\text{unop}$ preserves their supremum, i.e., $\text{unop}(S_1 \sqcup S_2) = \text{unop}(S_1) \sqcup \text{unop}(S_2)$.

Submonoid.op_inf theorem

(S₁ S₂ : Submonoid M) : (S₁ ⊓ S₂).op = S₁.op ⊓ S₂.op

Full source

@[to_additive]
theorem op_inf (S₁ S₂ : Submonoid M) : (S₁ ⊓ S₂).op = S₁.op ⊓ S₂.op := rfl

Opposite of Submonoid Intersection Equals Intersection of Opposites

Informal description

For any two submonoids $S_1$ and $S_2$ of a monoid $M$, the opposite of their intersection $(S_1 \cap S_2)^{\text{op}}$ is equal to the intersection of their opposites $S_1^{\text{op}} \cap S_2^{\text{op}}$.

Submonoid.unop_inf theorem

(S₁ S₂ : Submonoid Mᵐᵒᵖ) : (S₁ ⊓ S₂).unop = S₁.unop ⊓ S₂.unop

Full source

@[to_additive]
theorem unop_inf (S₁ S₂ : Submonoid Mᵐᵒᵖ) : (S₁ ⊓ S₂).unop = S₁.unop ⊓ S₂.unop := rfl

Unop Preserves Infimum of Submonoids in Opposite Monoid

Informal description

For any two submonoids $S_1$ and $S_2$ of the opposite monoid $M^{\text{op}}$, the unop operation preserves their infimum, i.e., $(S_1 \sqcap S_2)^{\text{unop}} = S_1^{\text{unop}} \sqcap S_2^{\text{unop}}$.

Submonoid.op_sSup theorem

(S : Set (Submonoid M)) : (sSup S).op = sSup (.unop ⁻¹' S)

Full source

@[to_additive]
theorem op_sSup (S : Set (Submonoid M)) : (sSup S).op = sSup (.unop.unop ⁻¹' S) :=
  opEquiv.map_sSup_eq_sSup_symm_preimage _

Opposite of Supremum of Submonoids Equals Supremum of Preimage under Unop

Informal description

For any collection $S$ of submonoids of a monoid $M$, the opposite of their supremum $\bigvee S$ is equal to the supremum of the preimage of $S$ under the `unop` operation, i.e., $(\bigvee S)^{\text{op}} = \bigvee \text{unop}^{-1}(S)$.

Submonoid.unop_sSup theorem

(S : Set (Submonoid Mᵐᵒᵖ)) : (sSup S).unop = sSup (.op ⁻¹' S)

Full source

@[to_additive]
theorem unop_sSup (S : Set (Submonoid Mᵐᵒᵖ)) : (sSup S).unop = sSup (.op.op ⁻¹' S) :=
  opEquiv.symm.map_sSup_eq_sSup_symm_preimage _

Unop Preserves Supremum of Submonoids in Opposite Monoid

Informal description

For any family of submonoids $\{S_i\}_{i \in I}$ of the opposite monoid $M^{\text{op}}$, the unop operation preserves the supremum, i.e., \[ \left(\bigvee_{i \in I} S_i\right)^{\text{unop}} = \bigvee_{i \in I} S_i^{\text{unop}}, \] where the suprema are taken in the lattice of submonoids of $M$ and $M^{\text{op}}$ respectively.

Submonoid.op_sInf theorem

(S : Set (Submonoid M)) : (sInf S).op = sInf (.unop ⁻¹' S)

Full source

@[to_additive]
theorem op_sInf (S : Set (Submonoid M)) : (sInf S).op = sInf (.unop.unop ⁻¹' S) :=
  opEquiv.map_sInf_eq_sInf_symm_preimage _

Opposite of Infimum of Submonoids Equals Infimum of Opposite Preimage

Informal description

For any family of submonoids $S$ of a monoid $M$, the opposite of their infimum $\bigwedge S$ is equal to the infimum of the preimage of $S$ under the operation $\text{unop} : M^{\text{op}} \to M$. That is, $(\bigwedge S)^{\text{op}} = \bigwedge (\text{unop}^{-1}(S))$.

Submonoid.unop_sInf theorem

(S : Set (Submonoid Mᵐᵒᵖ)) : (sInf S).unop = sInf (.op ⁻¹' S)

Full source

@[to_additive]
theorem unop_sInf (S : Set (Submonoid Mᵐᵒᵖ)) : (sInf S).unop = sInf (.op.op ⁻¹' S) :=
  opEquiv.symm.map_sInf_eq_sInf_symm_preimage _

Infimum Preservation under Unop Operation for Submonoids of Opposite Monoid

Informal description

For any family of submonoids $S$ of the opposite monoid $M^{\text{op}}$, the unop operation applied to the infimum of $S$ equals the infimum of the preimage of $S$ under the op operation. In other words, $$(\inf S)^{\text{unop}} = \inf \{T \subseteq M \mid T^{\text{op}} \in S\}.$$

Submonoid.op_iSup theorem

(S : ι → Submonoid M) : (iSup S).op = ⨆ i, (S i).op

Full source

@[to_additive]
theorem op_iSup (S : ι → Submonoid M) : (iSup S).op = ⨆ i, (S i).op := opEquiv.map_iSup _

Opposite of Supremum of Submonoids Equals Supremum of Opposites

Informal description

For any family of submonoids $(S_i)_{i \in \iota}$ of a monoid $M$, the opposite of their supremum equals the supremum of their opposites. That is, $(\bigsqcup_i S_i)^{\text{op}} = \bigsqcup_i (S_i^{\text{op}})$.

Submonoid.unop_iSup theorem

(S : ι → Submonoid Mᵐᵒᵖ) : (iSup S).unop = ⨆ i, (S i).unop

Full source

@[to_additive]
theorem unop_iSup (S : ι → Submonoid Mᵐᵒᵖ) : (iSup S).unop = ⨆ i, (S i).unop :=
  opEquiv.symm.map_iSup _

Unopposite of Supremum of Submonoids Equals Supremum of Unopposites

Informal description

For any family of submonoids $(S_i)_{i \in \iota}$ of the opposite monoid $M^{\text{op}}$, the unopposite of their supremum equals the supremum of their unopposites. That is, $$(\bigsqcup_{i \in \iota} S_i)^{\text{unop}} = \bigsqcup_{i \in \iota} S_i^{\text{unop}}.$$

Submonoid.op_iInf theorem

(S : ι → Submonoid M) : (iInf S).op = ⨅ i, (S i).op

Full source

@[to_additive]
theorem op_iInf (S : ι → Submonoid M) : (iInf S).op = ⨅ i, (S i).op := opEquiv.map_iInf _

Opposite of Infimum of Submonoids Equals Infimum of Opposites

Informal description

For any family of submonoids $(S_i)_{i \in \iota}$ of a monoid $M$, the opposite of their infimum is equal to the infimum of their opposites, i.e., $$(\bigsqcap_i S_i)^{\text{op}} = \bigsqcap_i S_i^{\text{op}}.$$

Submonoid.unop_iInf theorem

(S : ι → Submonoid Mᵐᵒᵖ) : (iInf S).unop = ⨅ i, (S i).unop

Full source

@[to_additive]
theorem unop_iInf (S : ι → Submonoid Mᵐᵒᵖ) : (iInf S).unop = ⨅ i, (S i).unop :=
  opEquiv.symm.map_iInf _

Unop Preserves Infima of Submonoids in Opposite Monoid

Informal description

For any family of submonoids $(S_i)_{i \in \iota}$ of the opposite monoid $M^{\text{op}}$, the unop operation commutes with infima. That is, the unop of the infimum of the family is equal to the infimum of the unops of each submonoid in the family: $$(\bigsqcap_i S_i)^{\text{unop}} = \bigsqcap_i S_i^{\text{unop}}.$$

Submonoid.op_closure theorem

(s : Set M) : (closure s).op = closure (MulOpposite.unop ⁻¹' s)

Full source

@[to_additive]
theorem op_closure (s : Set M) : (closure s).op = closure (MulOpposite.unopMulOpposite.unop ⁻¹' s) := by
  simp_rw [closure, op_sInf, Set.preimage_setOf_eq, Submonoid.coe_unop]
  congr with a
  exact MulOpposite.unop_surjective.forall

Opposite of Generated Submonoid Equals Generated Opposite Preimage

Informal description

For any subset $s$ of a monoid $M$, the opposite submonoid of the submonoid generated by $s$ is equal to the submonoid generated by the preimage of $s$ under the unary operation $\text{unop} : M^{\text{op}} \to M$. That is, $$(\text{closure}(s))^{\text{op}} = \text{closure}(\text{unop}^{-1}(s)).$$

Submonoid.unop_closure theorem

(s : Set Mᵐᵒᵖ) : (closure s).unop = closure (MulOpposite.op ⁻¹' s)

Full source

@[to_additive]
theorem unop_closure (s : Set Mᵐᵒᵖ) : (closure s).unop = closure (MulOpposite.opMulOpposite.op ⁻¹' s) := by
  rw [← op_inj, op_unop, op_closure]
  simp_rw [Set.preimage_preimage, MulOpposite.op_unop, Set.preimage_id']

Unop of Generated Submonoid in Opposite Monoid Equals Generated Preimage under Op

Informal description

For any subset $s$ of the opposite monoid $M^{\text{op}}$, the submonoid $\text{unop}(\text{closure}(s))$ of $M$ is equal to the submonoid generated by the preimage of $s$ under the operation $\text{op} : M \to M^{\text{op}}$. That is, $$(\text{closure}(s))^{\text{unop}} = \text{closure}(\text{op}^{-1}(s)).$$

Submonoid.equivOp definition

(H : Submonoid M) : H ≃ H.op

Full source

/-- Bijection between a submonoid `H` and its opposite. -/
@[to_additive (attr := simps!) "Bijection between an additive submonoid `H` and its opposite."]
def equivOp (H : Submonoid M) : H ≃ H.op :=
  MulOpposite.opEquiv.subtypeEquiv fun _ => Iff.rfl

Bijection between a submonoid and its opposite

Informal description

For any submonoid $H$ of a monoid $M$, there is a bijection between $H$ and its opposite submonoid $H^{\text{op}}$, where $H^{\text{op}}$ consists of all elements $x \in M^{\text{op}}$ such that $\text{unop}(x) \in H$.