Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas

Subgroup.instSMul instance

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

Full source

@[to_additive] instance instSMul (H : Subgroup G) : SMul H.op G := Submonoid.smul ..

Scalar Multiplication Action of Opposite Subgroup on Group

Informal description

For any subgroup $H$ of a group $G$, the multiplicative opposite subgroup $H^\text{op}$ has a canonical scalar multiplication action on $G$ defined by $h^\text{op} \bullet g = g * h$ for $h^\text{op} \in H^\text{op}$ and $g \in G$.

Subgroup.op_bot theorem

: (⊥ : Subgroup G).op = ⊥

Full source

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

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

Informal description

The multiplicative opposite of the trivial subgroup $\bot$ of a group $G$ is equal to the trivial subgroup $\bot$ of the opposite group $G^\text{op}$.

Subgroup.op_eq_bot theorem

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

Full source

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

Opposite Subgroup is Trivial if and only if Original Subgroup is Trivial

Informal description

For any subgroup $S$ of a group $G$, the multiplicative opposite subgroup $S^\text{op}$ is equal to the trivial subgroup $\bot$ of $G^\text{op}$ if and only if $S$ is equal to the trivial subgroup $\bot$ of $G$.

Subgroup.unop_bot theorem

: (⊥ : Subgroup Gᵐᵒᵖ).unop = ⊥

Full source

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

Unopposite of Bottom Subgroup is Bottom Subgroup

Informal description

The unopposite of the bottom subgroup of the multiplicative opposite group $G^\text{op}$ is equal to the bottom subgroup of $G$. In other words, $(\bot : \text{Subgroup } G^\text{op})^\text{unop} = \bot$.

Subgroup.unop_eq_bot theorem

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

Full source

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

Triviality Criterion for Subgroups via Unopposite Operation

Informal description

For any subgroup $S$ of the multiplicative opposite group $G^\text{op}$, the corresponding subgroup $S^\text{unop}$ in $G$ is the trivial subgroup if and only if $S$ is the trivial subgroup in $G^\text{op}$. In other words, $S^\text{unop} = \bot \leftrightarrow S = \bot$.

Subgroup.op_top theorem

: (⊤ : Subgroup G).op = ⊤

Full source

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

Opposite of Top Subgroup is Top Subgroup in Opposite Group

Informal description

The multiplicative opposite of the top subgroup of a group $G$ is equal to the top subgroup of the multiplicative opposite group $G^\text{op}$. In other words, $(\top : \text{Subgroup } G)^\text{op} = \top$.

Subgroup.op_eq_top theorem

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

Full source

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

Characterization of Top Subgroup via Multiplicative Opposite: $S^\text{op} = \top \leftrightarrow S = \top$

Informal description

For any subgroup $S$ of a group $G$, the multiplicative opposite subgroup $S^\text{op}$ is equal to the top subgroup of $G^\text{op}$ if and only if $S$ is the top subgroup of $G$. In other words, $S^\text{op} = \top$ holds precisely when $S = \top$.

Subgroup.unop_top theorem

: (⊤ : Subgroup Gᵐᵒᵖ).unop = ⊤

Full source

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

Preimage of Top Subgroup in Opposite Group is Top Subgroup

Informal description

The preimage of the top subgroup of the multiplicative opposite group $G^\text{op}$ under the canonical embedding $\text{op} : G \to G^\text{op}$ is the top subgroup of $G$. In other words, $(\top : \text{Subgroup } G^\text{op}).\text{unop} = \top$.

Subgroup.unop_eq_top theorem

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

Full source

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

Unop of Subgroup is Top if and only if Subgroup is Top in Opposite Group

Informal description

For any subgroup $S$ of the multiplicative opposite group $G^\text{op}$, the corresponding subgroup $S.\text{unop}$ of $G$ is equal to the top subgroup $\top$ if and only if $S$ is the top subgroup of $G^\text{op}$.

Subgroup.op_sup theorem

(S₁ S₂ : Subgroup G) : (S₁ ⊔ S₂).op = S₁.op ⊔ S₂.op

Full source

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

Join of Subgroups Commutes with Multiplicative Opposite: $(S_1 \sqcup S_2)^\text{op} = S_1^\text{op} \sqcup S_2^\text{op}$

Informal description

For any two subgroups $S_1$ and $S_2$ of a group $G$, the multiplicative opposite of their join $(S_1 \sqcup S_2)^\text{op}$ is equal to the join of their multiplicative opposites $S_1^\text{op} \sqcup S_2^\text{op}$ in the opposite group $G^\text{op}$.

Subgroup.unop_sup theorem

(S₁ S₂ : Subgroup Gᵐᵒᵖ) : (S₁ ⊔ S₂).unop = S₁.unop ⊔ S₂.unop

Full source

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

Supremum of Opposite Subgroups Preserved by Unop

Informal description

For any two subgroups $S_1$ and $S_2$ of the multiplicative opposite group $G^\text{op}$, the unop operation (which maps a subgroup of $G^\text{op}$ back to a subgroup of $G$) commutes with the supremum operation. That is, $(S_1 \sqcup S_2).\text{unop} = S_1.\text{unop} \sqcup S_2.\text{unop}$.

Subgroup.op_inf theorem

(S₁ S₂ : Subgroup G) : (S₁ ⊓ S₂).op = S₁.op ⊓ S₂.op

Full source

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

Intersection of Subgroups Commutes with Multiplicative Opposite

Informal description

For any two subgroups $S₁$ and $S₂$ of a group $G$, the multiplicative opposite of their intersection $(S₁ \cap S₂)^\text{op}$ is equal to the intersection of their multiplicative opposites $S₁^\text{op} \cap S₂^\text{op}$.

Subgroup.unop_inf theorem

(S₁ S₂ : Subgroup Gᵐᵒᵖ) : (S₁ ⊓ S₂).unop = S₁.unop ⊓ S₂.unop

Full source

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

Infimum of Opposite Subgroups Preserved by Unop

Informal description

For any two subgroups $S_1$ and $S_2$ of the multiplicative opposite group $G^\text{op}$, the unop operation (which maps a subgroup of $G^\text{op}$ back to a subgroup of $G$) commutes with the infimum operation. That is, $(S_1 \cap S_2).\text{unop} = S_1.\text{unop} \cap S_2.\text{unop}$.

Subgroup.op_sSup theorem

(S : Set (Subgroup G)) : (sSup S).op = sSup (.unop ⁻¹' S)

Full source

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

Supremum of Subgroups Commutes with Multiplicative Opposite

Informal description

Let $G$ be a group and $S$ be a set of subgroups of $G$. The multiplicative opposite of the supremum (join) of $S$ is equal to the supremum of the preimage of $S$ under the `unop` operation in the lattice of subgroups of $G^\text{op}$. In symbols: \[ (\bigvee S)^\text{op} = \bigvee \{H \in \text{Subgroup}(G^\text{op}) \mid H^\text{unop} \in S\} \]

Subgroup.unop_sSup theorem

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

Full source

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

Supremum of Opposite Subgroups Preserved by Unop

Informal description

For any set $S$ of subgroups of the multiplicative opposite group $G^\text{op}$, the unop operation (which maps a subgroup of $G^\text{op}$ back to a subgroup of $G$) commutes with the supremum operation. That is, the unop of the supremum of $S$ equals the supremum of the preimage of $S$ under the op operation: \[ (\bigvee S).\text{unop} = \bigvee \{H \mid H^\text{op} \in S\}. \]

Subgroup.op_sInf theorem

(S : Set (Subgroup G)) : (sInf S).op = sInf (.unop ⁻¹' S)

Full source

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

Infimum of Subgroups Commutes with Multiplicative Opposite

Informal description

Let $G$ be a group and $S$ a set of subgroups of $G$. The multiplicative opposite of the infimum (meet) of $S$ is equal to the infimum of the preimage of $S$ under the `unop` operation in the lattice of subgroups of $G^\text{op}$. In symbols: \[ (\bigwedge S)^\text{op} = \bigwedge \{H \in \text{Subgroup}(G^\text{op}) \mid H^\text{unop} \in S\}. \]

Subgroup.unop_sInf theorem

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

Full source

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

Infimum of Opposite Subgroups Preserved by Unop

Informal description

For any set $S$ of subgroups of the multiplicative opposite group $G^\text{op}$, the unop operation (which maps a subgroup of $G^\text{op}$ back to a subgroup of $G$) commutes with the infimum operation. That is, the unop of the infimum of $S$ equals the infimum of the preimage of $S$ under the op operation: \[ (\bigwedge S).\text{unop} = \bigwedge \{H \mid H^\text{op} \in S\}. \]

Subgroup.op_iSup theorem

(S : ι → Subgroup G) : (iSup S).op = ⨆ i, (S i).op

Full source

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

Opposite Subgroup Preserves Indexed Suprema: $(\bigsqcup_i H_i)^\text{op} = \bigsqcup_i H_i^\text{op}$

Informal description

Let $G$ be a group and $(H_i)_{i \in \iota}$ a family of subgroups of $G$. Then the multiplicative opposite of the supremum of the $H_i$ is equal to the supremum of the multiplicative opposites of the $H_i$: \[ \left(\bigsqcup_{i} H_i\right)^\text{op} = \bigsqcup_{i} H_i^\text{op}. \]

Subgroup.unop_iSup theorem

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

Full source

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

Unop Preserves Suprema of Subgroups in Opposite Group

Informal description

Let $G$ be a group and $G^\text{op}$ its multiplicative opposite group. For any family of subgroups $(S_i)_{i \in \iota}$ of $G^\text{op}$, the unop operation (which converts subgroups of $G^\text{op}$ back to subgroups of $G$) commutes with taking suprema. That is, the unop of the supremum of the $S_i$ equals the supremum of the unops of the $S_i$: \[ (\bigsqcup_{i} S_i).\text{unop} = \bigsqcup_{i} (S_i.\text{unop}) \]

Subgroup.op_iInf theorem

(S : ι → Subgroup G) : (iInf S).op = ⨅ i, (S i).op

Full source

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

Opposite Subgroup Preserves Indexed Infima: $(\bigsqcap_i H_i)^\text{op} = \bigsqcap_i H_i^\text{op}$

Informal description

Let $G$ be a group and $(H_i)_{i \in \iota}$ a family of subgroups of $G$. Then the multiplicative opposite of the infimum of the $H_i$ is equal to the infimum of the multiplicative opposites of the $H_i$: \[ \left(\bigsqcap_{i} H_i\right)^\text{op} = \bigsqcap_{i} H_i^\text{op}. \]

Subgroup.unop_iInf theorem

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

Full source

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

Unop Preserves Infima of Subgroups in Opposite Group

Informal description

Let $G$ be a group and $G^\text{op}$ its multiplicative opposite group. For any family of subgroups $(S_i)_{i \in \iota}$ of $G^\text{op}$, the unop operation (which converts subgroups of $G^\text{op}$ back to subgroups of $G$) commutes with taking infima. That is, the unop of the infimum of the $S_i$ equals the infimum of the unops of the $S_i$: \[ (\bigsqcap_{i} S_i).\text{unop} = \bigsqcap_{i} (S_i.\text{unop}) \]

Subgroup.op_closure theorem

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

Full source

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

Subgroup Closure Commutes with Multiplicative Opposite: $(\langle s \rangle)^\text{op} = \langle \text{unop}^{-1}(s) \rangle$

Informal description

Let $G$ be a group and $s$ a subset of $G$. The multiplicative opposite of the subgroup generated by $s$ is equal to the subgroup of $G^\text{op}$ generated by the preimage of $s$ under the canonical projection $\text{unop} : G^\text{op} \to G$. In symbols: \[ (\langle s \rangle)^\text{op} = \langle \text{unop}^{-1}(s) \rangle. \]

Subgroup.unop_closure theorem

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

Full source

@[to_additive]
theorem unop_closure (s : Set Gᵐᵒᵖ) : (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']

Subgroup Closure Commutes with Unop: $(\langle s \rangle).\text{unop} = \langle \text{op}^{-1}(s) \rangle$

Informal description

Let $G$ be a group and $s$ a subset of the multiplicative opposite group $G^\text{op}$. The subgroup of $G$ obtained by applying the `unop` operation to the subgroup generated by $s$ in $G^\text{op}$ is equal to the subgroup of $G$ generated by the preimage of $s$ under the canonical embedding $\text{op} : G \to G^\text{op}$. In symbols: \[ (\langle s \rangle).\text{unop} = \langle \text{op}^{-1}(s) \rangle. \]

Subgroup.instEncodableSubtypeMulOppositeMemOp instance

(H : Subgroup G) [Encodable H] : Encodable H.op

Full source

@[to_additive]
instance (H : Subgroup G) [Encodable H] : Encodable H.op :=
  Encodable.ofEquiv H H.equivOp.symm

Encodability of the Multiplicative Opposite Subgroup

Informal description

For any subgroup $H$ of a group $G$, if $H$ is encodable, then its multiplicative opposite subgroup $H^\text{op}$ is also encodable.

Subgroup.instCountableSubtypeMulOppositeMemOp instance

(H : Subgroup G) [Countable H] : Countable H.op

Full source

@[to_additive]
instance (H : Subgroup G) [Countable H] : Countable H.op :=
  Countable.of_equiv H H.equivOp

Countability of the Opposite Subgroup

Informal description

For any subgroup $H$ of a group $G$, if $H$ is countable, then its multiplicative opposite subgroup $H^\text{op}$ is also countable.

Subgroup.smul_opposite_mul theorem

{H : Subgroup G} (x g : G) (h : H.op) : h • (g * x) = g * h • x

Full source

@[to_additive]
theorem smul_opposite_mul {H : Subgroup G} (x g : G) (h : H.op) :
    h • (g * x) = g * h • x :=
  mul_assoc _ _ _

Compatibility of Opposite Subgroup Action with Group Multiplication: $h \bullet (g * x) = g * (h \bullet x)$

Informal description

Let $H$ be a subgroup of a group $G$. For any elements $x, g \in G$ and any $h \in H^\text{op}$ (the multiplicative opposite subgroup of $H$), the scalar multiplication action satisfies $h \bullet (g * x) = g * (h \bullet x)$.

Subgroup.normal_op theorem

{H : Subgroup G} : H.op.Normal ↔ H.Normal

Full source

@[to_additive (attr := simp)]
theorem normal_op {H : Subgroup G} : H.op.Normal ↔ H.Normal := by
  simp only [← normalizer_eq_top_iff, ← op_normalizer, op_eq_top]

Normality of Opposite Subgroup: $H^\text{op} \triangleleft G^\text{op} \leftrightarrow H \triangleleft G$

Informal description

For any subgroup $H$ of a group $G$, the multiplicative opposite subgroup $H^\text{op}$ is normal in $G^\text{op}$ if and only if $H$ is normal in $G$.

Subgroup.op.instNormal instance

{H : Subgroup G} [H.Normal] : H.op.Normal

Full source

@[to_additive]
instance op.instNormal {H : Subgroup G} [H.Normal] : H.op.Normal := .op ‹_›

Normality of the Opposite Subgroup

Informal description

For any normal subgroup $H$ of a group $G$, the multiplicative opposite subgroup $H^\text{op}$ is normal in $G^\text{op}$.

Subgroup.normal_unop theorem

{H : Subgroup Gᵐᵒᵖ} : H.unop.Normal ↔ H.Normal

Full source

@[to_additive (attr := simp)]
theorem normal_unop {H : Subgroup Gᵐᵒᵖ} : H.unop.Normal ↔ H.Normal := by
  rw [← normal_op, op_unop]

Normality of Unopposite Subgroup: $H^\text{unop} \triangleleft G \leftrightarrow H \triangleleft G^\text{op}$

Informal description

For any subgroup $H$ of the multiplicative opposite group $G^\text{op}$, the subgroup $H^\text{unop}$ is normal in $G$ if and only if $H$ is normal in $G^\text{op}$.

Subgroup.unop.instNormal instance

{H : Subgroup Gᵐᵒᵖ} [H.Normal] : H.unop.Normal

Full source

@[to_additive]
instance unop.instNormal {H : Subgroup Gᵐᵒᵖ} [H.Normal] : H.unop.Normal := .unop ‹_›

Normality of the Unopposite Subgroup

Informal description

For any normal subgroup $H$ of the multiplicative opposite group $G^\text{op}$, the corresponding subgroup $H^\text{unop}$ is normal in $G$.

Tags