Documentation

Mathlib.GroupTheory.Subgroup.MulOpposite

Mul-opposite subgroups #

Tags #

subgroup, subgroups

theorem AddSubgroup.opposite.proof_1 {G : Type u_1} [AddGroup G] (H : AddSubgroup G) :
∀ {a b : Gᵃᵒᵖ}, a AddOpposite.unop ⁻¹' Hb AddOpposite.unop ⁻¹' HAddOpposite.unop b + AddOpposite.unop a H

An additive subgroup H of G determines an additive subgroup H.opposite of the opposite additive group Gᵃᵒᵖ.

Instances For
    theorem AddSubgroup.opposite.proof_6 {G : Type u_1} [AddGroup G] :
    ∀ (x : AddSubgroup G), (fun H => { toAddSubmonoid := { toAddSubsemigroup := { carrier := AddOpposite.op ⁻¹' H, add_mem' := (_ : ∀ {a b : G}, a AddOpposite.op ⁻¹' Hb AddOpposite.op ⁻¹' H{ unop' := b } + { unop' := a } H) }, zero_mem' := (_ : 0 H) }, neg_mem' := (_ : ∀ {x : G}, AddOpposite.op x H-AddOpposite.op x H) }) ((fun H => { toAddSubmonoid := { toAddSubsemigroup := { carrier := AddOpposite.unop ⁻¹' H, add_mem' := (_ : ∀ {a b : Gᵃᵒᵖ}, a AddOpposite.unop ⁻¹' Hb AddOpposite.unop ⁻¹' HAddOpposite.unop b + AddOpposite.unop a H) }, zero_mem' := (_ : 0 H) }, neg_mem' := (_ : ∀ {x : Gᵃᵒᵖ}, AddOpposite.unop x H-AddOpposite.unop x H) }) x) = x
    theorem AddSubgroup.opposite.proof_7 {G : Type u_1} [AddGroup G] :
    ∀ (x : AddSubgroup Gᵃᵒᵖ), (fun H => { toAddSubmonoid := { toAddSubsemigroup := { carrier := AddOpposite.unop ⁻¹' H, add_mem' := (_ : ∀ {a b : Gᵃᵒᵖ}, a AddOpposite.unop ⁻¹' Hb AddOpposite.unop ⁻¹' HAddOpposite.unop b + AddOpposite.unop a H) }, zero_mem' := (_ : 0 H) }, neg_mem' := (_ : ∀ {x : Gᵃᵒᵖ}, AddOpposite.unop x H-AddOpposite.unop x H) }) ((fun H => { toAddSubmonoid := { toAddSubsemigroup := { carrier := AddOpposite.op ⁻¹' H, add_mem' := (_ : ∀ {a b : G}, a AddOpposite.op ⁻¹' Hb AddOpposite.op ⁻¹' H{ unop' := b } + { unop' := a } H) }, zero_mem' := (_ : 0 H) }, neg_mem' := (_ : ∀ {x : G}, AddOpposite.op x H-AddOpposite.op x H) }) x) = x
    theorem AddSubgroup.opposite.proof_3 {G : Type u_1} [AddGroup G] (H : AddSubgroup Gᵃᵒᵖ) :
    ∀ {a b : G}, a AddOpposite.op ⁻¹' Hb AddOpposite.op ⁻¹' H{ unop' := b } + { unop' := a } H

    A subgroup H of G determines a subgroup H.opposite of the opposite group Gᵐᵒᵖ.

    Instances For
      theorem AddSubgroup.oppositeEquiv.proof_1 {G : Type u_1} [AddGroup G] (H : AddSubgroup G) :
      ∀ (x : G), x H x H
      def AddSubgroup.oppositeEquiv {G : Type u_1} [AddGroup G] (H : AddSubgroup G) :
      { x // x H } { x // x AddSubgroup.opposite H }

      Bijection between an additive subgroup H and its opposite.

      Instances For
        @[simp]
        theorem Subgroup.oppositeEquiv_symm_apply_coe {G : Type u_1} [Group G] (H : Subgroup G) (b : { b // (fun x => x Subgroup.opposite H) b }) :
        ↑((Subgroup.oppositeEquiv H).symm b) = MulOpposite.unop b
        @[simp]
        theorem AddSubgroup.oppositeEquiv_symm_apply_coe {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (b : { b // (fun x => x AddSubgroup.opposite H) b }) :
        @[simp]
        theorem AddSubgroup.oppositeEquiv_apply_coe {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (a : { a // (fun x => x H) a }) :
        @[simp]
        theorem Subgroup.oppositeEquiv_apply_coe {G : Type u_1} [Group G] (H : Subgroup G) (a : { a // (fun x => x H) a }) :
        def Subgroup.oppositeEquiv {G : Type u_1} [Group G] (H : Subgroup G) :
        { x // x H } { x // x Subgroup.opposite H }

        Bijection between a subgroup H and its opposite.

        Instances For
          theorem AddSubgroup.vadd_opposite_add {G : Type u_1} [AddGroup G] {H : AddSubgroup G} (x : G) (g : G) (h : { x // x AddSubgroup.opposite H }) :
          h +ᵥ (g + x) = g + (h +ᵥ x)
          theorem Subgroup.smul_opposite_mul {G : Type u_1} [Group G] {H : Subgroup G} (x : G) (g : G) (h : { x // x Subgroup.opposite H }) :
          h (g * x) = g * h x