Mathlib.Algebra.Group.Subgroup.MulOpposite

Subgroup.op definition

(H : Subgroup G) : Subgroup Gᵐᵒᵖ

Full source

/-- Pull a subgroup back to an opposite subgroup along `MulOpposite.unop` -/
@[to_additive (attr := simps)
"Pull an additive subgroup back to an opposite additive subgroup along `AddOpposite.unop`"]
protected def op (H : Subgroup G) : Subgroup Gᵐᵒᵖ where
  carrier := MulOpposite.unopMulOpposite.unop ⁻¹' (H : Set G)
  one_mem' := H.one_mem
  mul_mem' ha hb := H.mul_mem hb ha
  inv_mem' := H.inv_mem

Multiplicative opposite subgroup

Informal description

Given a subgroup $H$ of a group $G$, the multiplicative opposite subgroup $H^\text{op}$ is the subgroup of $G^\text{op}$ consisting of all elements $x$ in $G^\text{op}$ such that their projection back to $G$ (via `MulOpposite.unop`) lies in $H$. The subgroup $H^\text{op}$ inherits the group structure from $G^\text{op}$, with multiplication defined in the opposite order and inverses preserved.

Subgroup.mem_op theorem

{x : Gᵐᵒᵖ} {S : Subgroup G} : x ∈ S.op ↔ x.unop ∈ S

Full source

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

Membership Criterion for Multiplicative Opposite Subgroup

Informal description

For any element $x$ in the multiplicative opposite group $G^\text{op}$ and any subgroup $S$ of $G$, the element $x$ belongs to the opposite subgroup $S^\text{op}$ if and only if its projection back to $G$ (via `MulOpposite.unop`) belongs to $S$. In other words, $x \in S^\text{op} \leftrightarrow x^\text{unop} \in S$.

Subgroup.op_toSubmonoid theorem

(H : Subgroup G) : H.op.toSubmonoid = H.toSubmonoid.op

Full source

@[to_additive (attr := simp)] lemma op_toSubmonoid (H : Subgroup G) :
    H.op.toSubmonoid = H.toSubmonoid.op :=
  rfl

Submonoid Correspondence in Opposite Subgroup: $(H^\text{op}).\text{toSubmonoid} = (H.\text{toSubmonoid})^\text{op}$

Informal description

For any subgroup $H$ of a group $G$, the underlying submonoid of the opposite subgroup $H^\text{op}$ is equal to the opposite of the underlying submonoid of $H$. That is, $(H^\text{op}).\text{toSubmonoid} = (H.\text{toSubmonoid})^\text{op}$.

Subgroup.unop definition

(H : Subgroup Gᵐᵒᵖ) : Subgroup G

Full source

/-- 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`"]
protected def unop (H : Subgroup Gᵐᵒᵖ) : Subgroup G where
  carrier := MulOpposite.opMulOpposite.op ⁻¹' (H : Set Gᵐᵒᵖ)
  one_mem' := H.one_mem
  mul_mem' := fun ha hb => H.mul_mem hb ha
  inv_mem' := H.inv_mem

Subgroup of original group from opposite subgroup

Informal description

Given a subgroup $H$ of the multiplicative opposite group $G^\text{op}$, the function returns the corresponding subgroup of $G$ obtained by taking the preimage of $H$ under the canonical embedding $\text{op} : G \to G^\text{op}$. The subgroup consists of all elements $x \in G$ such that $\text{op}(x) \in H$, and it inherits the group structure from $G$.

Subgroup.mem_unop theorem

{x : G} {S : Subgroup Gᵐᵒᵖ} : x ∈ S.unop ↔ MulOpposite.op x ∈ S

Full source

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

Membership Criterion for Subgroup of Original Group via Opposite Subgroup

Informal description

For any element $x$ in a group $G$ and any subgroup $S$ of the multiplicative opposite group $G^\text{op}$, $x$ belongs to the subgroup $S.\text{unop}$ if and only if the canonical embedding $\text{op}(x)$ belongs to $S$.

Subgroup.unop_toSubmonoid theorem

(H : Subgroup Gᵐᵒᵖ) : H.unop.toSubmonoid = H.toSubmonoid.unop

Full source

@[to_additive (attr := simp)] lemma unop_toSubmonoid (H : Subgroup Gᵐᵒᵖ) :
    H.unop.toSubmonoid = H.toSubmonoid.unop :=
  rfl

Compatibility of Subgroup and Submonoid Unop Operations

Informal description

For any subgroup $H$ of the multiplicative opposite group $G^\text{op}$, the underlying submonoid of the corresponding subgroup $H^\text{unop}$ in $G$ is equal to the submonoid obtained by applying the $\text{unop}$ operation to the underlying submonoid of $H$.

Subgroup.unop_op theorem

(S : Subgroup G) : S.op.unop = S

Full source

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

Opposite and Unopposite Subgroup Identity: $(S^\text{op})^\text{unop} = S$

Informal description

For any subgroup $S$ of a group $G$, the unopposite of the opposite subgroup $S^\text{op}$ is equal to $S$ itself, i.e., $(S^\text{op})^\text{unop} = S$.

Subgroup.op_unop theorem

(S : Subgroup Gᵐᵒᵖ) : S.unop.op = S

Full source

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

Opposite Subgroup Involution: $(S^\text{unop})^\text{op} = S$

Informal description

For any subgroup $S$ of the multiplicative opposite group $G^\text{op}$, the operation of first taking the corresponding subgroup in $G$ via `unop` and then taking its opposite subgroup via `op` returns the original subgroup $S$, i.e., $(S^\text{unop})^\text{op} = S$.

Subgroup.op_le_iff theorem

{S₁ : Subgroup G} {S₂ : Subgroup Gᵐᵒᵖ} : S₁.op ≤ S₂ ↔ S₁ ≤ S₂.unop

Full source

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

Subgroup Order Relation Between Opposite and Original Groups

Informal description

For any subgroup $S_1$ of a group $G$ and any subgroup $S_2$ of the multiplicative opposite group $G^\text{op}$, the following are equivalent: 1. The opposite subgroup $S_1^\text{op}$ is contained in $S_2$. 2. The subgroup $S_1$ is contained in the unopposite subgroup $S_2^\text{unop}$. In symbols: $S_1^\text{op} \leq S_2 \leftrightarrow S_1 \leq S_2^\text{unop}$.

Subgroup.le_op_iff theorem

{S₁ : Subgroup Gᵐᵒᵖ} {S₂ : Subgroup G} : S₁ ≤ S₂.op ↔ S₁.unop ≤ S₂

Full source

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

Subgroup Order Relation Between Opposite and Original Groups: $S_1 \leq S_2^\text{op} \leftrightarrow S_1^\text{unop} \leq S_2$

Informal description

For any subgroup $S_1$ of the multiplicative opposite group $G^\text{op}$ and any subgroup $S_2$ of $G$, the following are equivalent: 1. The subgroup $S_1$ is contained in the opposite subgroup $S_2^\text{op}$. 2. The unopposite subgroup $S_1^\text{unop}$ is contained in $S_2$. In symbols: $S_1 \leq S_2^\text{op} \leftrightarrow S_1^\text{unop} \leq S_2$.

Subgroup.op_le_op_iff theorem

{S₁ S₂ : Subgroup G} : S₁.op ≤ S₂.op ↔ S₁ ≤ S₂

Full source

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

Order Relation Between Opposite Subgroups

Informal description

For any two subgroups $S_1$ and $S_2$ of a group $G$, the opposite subgroup $S_1^\text{op}$ is contained in $S_2^\text{op}$ if and only if $S_1$ is contained in $S_2$. In symbols: $$ S_1^\text{op} \leq S_2^\text{op} \leftrightarrow S_1 \leq S_2 $$

Subgroup.unop_le_unop_iff theorem

{S₁ S₂ : Subgroup Gᵐᵒᵖ} : S₁.unop ≤ S₂.unop ↔ S₁ ≤ S₂

Full source

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

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

Informal description

For any two subgroups $S_1$ and $S_2$ of the multiplicative opposite group $G^\text{op}$, the subgroup $S_1^\text{unop}$ is contained in $S_2^\text{unop}$ if and only if $S_1$ is contained in $S_2$ as subgroups of $G^\text{op}$.

Subgroup.opEquiv definition

: Subgroup G ≃o Subgroup Gᵐᵒᵖ

Full source

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

Order isomorphism between subgroups and opposite subgroups

Informal description

The order isomorphism $\text{Subgroup}(G) \simeq_o \text{Subgroup}(G^\text{op})$ between the lattice of subgroups of a group $G$ and the lattice of subgroups of its multiplicative opposite $G^\text{op}$. The isomorphism is given by mapping a subgroup $H$ of $G$ to its opposite subgroup $H^\text{op}$ in $G^\text{op}$, and vice versa via the inverse operation. This correspondence preserves the subgroup order relation: for any subgroups $H_1, H_2$ of $G$, we have $H_1 \leq H_2$ if and only if $H_1^\text{op} \leq H_2^\text{op}$.

Subgroup.op_injective theorem

: (@Subgroup.op G _).Injective

Full source

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

Injectivity of the Subgroup Opposite Map

Informal description

The map $\text{op} : \text{Subgroup}(G) \to \text{Subgroup}(G^\text{op})$, which sends a subgroup $H$ of $G$ to its multiplicative opposite subgroup $H^\text{op}$, is injective. That is, for any subgroups $H_1, H_2$ of $G$, if $H_1^\text{op} = H_2^\text{op}$, then $H_1 = H_2$.

Subgroup.unop_injective theorem

: (@Subgroup.unop G _).Injective

Full source

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

Injectivity of the Subgroup Unopposite Function

Informal description

The function $\text{unop} : \text{Subgroup}(G^\text{op}) \to \text{Subgroup}(G)$, which maps a subgroup of the multiplicative opposite group $G^\text{op}$ to the corresponding subgroup of $G$, is injective. That is, for any subgroups $H_1, H_2$ of $G^\text{op}$, if $\text{unop}(H_1) = \text{unop}(H_2)$, then $H_1 = H_2$.

Subgroup.op_inj theorem

{S T : Subgroup G} : S.op = T.op ↔ S = T

Full source

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

Injectivity of the Opposite Subgroup Construction

Informal description

For any two subgroups $S$ and $T$ of a group $G$, the multiplicative opposite subgroups $S^\text{op}$ and $T^\text{op}$ are equal if and only if $S = T$.

Subgroup.unop_inj theorem

{S T : Subgroup Gᵐᵒᵖ} : S.unop = T.unop ↔ S = T

Full source

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

Inverse Subgroup Correspondence is Injective: $S^\text{unop} = T^\text{unop} \leftrightarrow S = T$

Informal description

For any two subgroups $S$ and $T$ of the multiplicative opposite group $G^\text{op}$, the corresponding subgroups $S^\text{unop}$ and $T^\text{unop}$ in $G$ are equal if and only if $S = T$.

Subgroup.equivOp definition

(H : Subgroup G) : H ≃ H.op

Full source

/-- 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 :=
  MulOpposite.opEquiv.subtypeEquiv fun _ => Iff.rfl

Bijection between a subgroup and its multiplicative opposite

Informal description

Given a subgroup $ H $ of a group $ G $, there is a bijection between $ H $ and its multiplicative opposite subgroup $ H^\text{op} $. The bijection is given by the canonical embedding $ \text{op} : G \to G^\text{op} $ restricted to $ H $, with its inverse being the projection $ \text{unop} : G^\text{op} \to G $ restricted to $ H^\text{op} $.

Subgroup.op_normalizer theorem

(H : Subgroup G) : H.normalizer.op = H.op.normalizer

Full source

@[to_additive]
theorem op_normalizer (H : Subgroup G) : H.normalizer.op = H.op.normalizer := by
  ext x
  simp [mem_normalizer_iff', MulOpposite.op_surjective.forall, iff_comm]

Normalizer Commutes with Multiplicative Opposite: $(N_G(H))^\text{op} = N_{G^\text{op}}(H^\text{op})$

Informal description

For any subgroup $H$ of a group $G$, the multiplicative opposite of the normalizer of $H$ is equal to the normalizer of the multiplicative opposite of $H$. That is, $(N_G(H))^\text{op} = N_{G^\text{op}}(H^\text{op})$.

Subgroup.unop_normalizer theorem

(H : Subgroup Gᵐᵒᵖ) : H.normalizer.unop = H.unop.normalizer

Full source

@[to_additive]
theorem unop_normalizer (H : Subgroup Gᵐᵒᵖ) : H.normalizer.unop = H.unop.normalizer := by
  rw [← op_inj, op_unop, op_normalizer, op_unop]

Normalizer Commutes with Unopposite: $(N_{G^\text{op}}(H))^\text{unop} = N_G(H^\text{unop})$

Informal description

For any subgroup $H$ of the multiplicative opposite group $G^\text{op}$, the unopposite of the normalizer of $H$ is equal to the normalizer of the unopposite of $H$. That is, $(N_{G^\text{op}}(H))^\text{unop} = N_G(H^\text{unop})$.

Tags