Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+โ†‘Ctrl+โ†“to navigate, Ctrl+๐Ÿ–ฑ๏ธto focus. On Mac, use Cmdinstead of Ctrl. 
/-
Copyright (c) 2022 Alex Kontorovich. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Alex Kontorovich

! This file was ported from Lean 3 source module group_theory.subgroup.mul_opposite
! leanprover-community/mathlib commit f93c11933efbc3c2f0299e47b8ff83e9b539cbf6
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.GroupTheory.Subgroup.Actions

/-!
# Mul-opposite subgroups

## Tags
subgroup, subgroups

-/


variable {
G: Type ?u.3013
G : 
Type _: Type (?u.2122+1)
Type _} [
Group: Type ?u.3774 โ†’ Type ?u.3774
Group 
G: Type ?u.2
G]

namespace Subgroup

/-- A subgroup `H` of `G` determines a subgroup `H.opposite` of the opposite group `Gแตแต’แต–`. -/
@[
to_additive: {G : Type u_1} โ†’ [inst : AddGroup G] โ†’ AddSubgroup G โ‰ƒ AddSubgroup Gแตƒแต’แต–
to_additive "An additive subgroup `H` of `G` determines an additive subgroup `H.opposite` of the
 opposite additive group `Gแตƒแต’แต–`."]
def 
opposite: {G : Type u_1} โ†’ [inst : Group G] โ†’ Subgroup G โ‰ƒ Subgroup Gแตแต’แต–
opposite : 
Subgroup: (G : Type ?u.16) โ†’ [inst : Group G] โ†’ Type ?u.16
Subgroup 
G: Type ?u.8
G โ‰ƒ 
Subgroup: (G : Type ?u.22) โ†’ [inst : Group G] โ†’ Type ?u.22
Subgroup 
G: Type ?u.8
Gแตแต’แต–
    where
  toFun 
H: ?m.41
H :=
    { carrier := 
MulOpposite.unop: {ฮฑ : Type ?u.750} โ†’ ฮฑแตแต’แต– โ†’ ฮฑ
MulOpposite.unop โปยน' (
H: ?m.41
H : 
Set: Type ?u.757 โ†’ Type ?u.757
Set 
G: Type ?u.8
G)
      one_mem' := 
H: ?m.41
H.
one_mem: โˆ€ {G : Type ?u.905} [inst : Group G] (H : Subgroup G), 1 โˆˆ H
one_mem
      mul_mem' := fun 
ha: ?m.850
ha 
hb: ?m.853
hb => 
H: ?m.41
H.
mul_mem: โˆ€ {G : Type ?u.855} [inst : Group G] (H : Subgroup G) {x y : G}, x โˆˆ H โ†’ y โˆˆ H โ†’ x * y โˆˆ H
mul_mem 
hb: ?m.853
hb 
ha: ?m.850
ha
      inv_mem' := 
H: ?m.41
H.
inv_mem: โˆ€ {G : Type ?u.912} [inst : Group G] (H : Subgroup G) {x : G}, x โˆˆ H โ†’ xโปยน โˆˆ H
inv_mem }
  invFun 
H: ?m.932
H :=
    { carrier := 
MulOpposite.op: {ฮฑ : Type ?u.1510} โ†’ ฮฑ โ†’ ฮฑแตแต’แต–
MulOpposite.op โปยน' (
H: ?m.932
H : 
Set: Type ?u.1516 โ†’ Type ?u.1516
Set 
G: Type ?u.8
Gแตแต’แต–)
      one_mem' := 
H: ?m.932
H.
one_mem: โˆ€ {G : Type ?u.1614} [inst : Group G] (H : Subgroup G), 1 โˆˆ H
one_mem
      mul_mem' := fun 
ha: ?m.1584
ha 
hb: ?m.1587
hb => 
H: ?m.932
H.
mul_mem: โˆ€ {G : Type ?u.1589} [inst : Group G] (H : Subgroup G) {x y : G}, x โˆˆ H โ†’ y โˆˆ H โ†’ x * y โˆˆ H
mul_mem 
hb: ?m.1587
hb 
ha: ?m.1584
ha
      inv_mem' := 
H: ?m.932
H.
inv_mem: โˆ€ {G : Type ?u.1621} [inst : Group G] (H : Subgroup G) {x : G}, x โˆˆ H โ†’ xโปยน โˆˆ H
inv_mem }
  left_inv 
_: ?m.1639
_ := 
SetLike.coe_injective: โˆ€ {A : Type ?u.1641} {B : Type ?u.1642} [i : SetLike A B], Function.Injective SetLike.coe
SetLike.coe_injective 
rfl: โˆ€ {ฮฑ : Sort ?u.1664} {a : ฮฑ}, a = a
rfl
  right_inv 
_: ?m.1688
_ := 
SetLike.coe_injective: โˆ€ {A : Type ?u.1690} {B : Type ?u.1691} [i : SetLike A B], Function.Injective SetLike.coe
SetLike.coe_injective 
rfl: โˆ€ {ฮฑ : Sort ?u.1710} {a : ฮฑ}, a = a
rfl
#align subgroup.opposite 
Subgroup.opposite: {G : Type u_1} โ†’ [inst : Group G] โ†’ Subgroup G โ‰ƒ Subgroup Gแตแต’แต–
Subgroup.opposite
#align add_subgroup.opposite 
AddSubgroup.opposite: {G : Type u_1} โ†’ [inst : AddGroup G] โ†’ AddSubgroup G โ‰ƒ AddSubgroup Gแตƒแต’แต–
AddSubgroup.opposite

/-- Bijection between a subgroup `H` and its opposite. -/
@[
to_additive: {G : Type u_1} โ†’ [inst : AddGroup G] โ†’ (H : AddSubgroup G) โ†’ { x // x โˆˆ H } โ‰ƒ { x // x โˆˆ โ†‘AddSubgroup.opposite H }
to_additive (attr := simps!) "Bijection between an additive subgroup `H` and its opposite."]
def 
oppositeEquiv: (H : Subgroup G) โ†’ { x // x โˆˆ H } โ‰ƒ { x // x โˆˆ โ†‘opposite H }
oppositeEquiv (
H: Subgroup G
H : 
Subgroup: (G : Type ?u.2128) โ†’ [inst : Group G] โ†’ Type ?u.2128
Subgroup 
G: Type ?u.2122
G) : 
H: Subgroup G
H โ‰ƒ 
opposite: {G : Type ?u.2305} โ†’ [inst : Group G] โ†’ Subgroup G โ‰ƒ Subgroup Gแตแต’แต–
opposite 
H: Subgroup G
H :=
  
MulOpposite.opEquiv: {ฮฑ : Type ?u.2598} โ†’ ฮฑ โ‰ƒ ฮฑแตแต’แต–
MulOpposite.opEquiv.
subtypeEquiv: {ฮฑ : Sort ?u.2601} โ†’
  {ฮฒ : Sort ?u.2600} โ†’
    {p : ฮฑ โ†’ Prop} โ†’ {q : ฮฒ โ†’ Prop} โ†’ (e : ฮฑ โ‰ƒ ฮฒ) โ†’ (โˆ€ (a : ฮฑ), p a โ†” q (โ†‘e a)) โ†’ { a // p a } โ‰ƒ { b // q b }
subtypeEquiv fun 
_: ?m.2626
_ => 
Iff.rfl: โˆ€ {a : Prop}, a โ†” a
Iff.rfl
#align subgroup.opposite_equiv 
Subgroup.oppositeEquiv: {G : Type u_1} โ†’ [inst : Group G] โ†’ (H : Subgroup G) โ†’ { x // x โˆˆ H } โ‰ƒ { x // x โˆˆ โ†‘opposite H }
Subgroup.oppositeEquiv
#align add_subgroup.opposite_equiv 
AddSubgroup.oppositeEquiv: {G : Type u_1} โ†’ [inst : AddGroup G] โ†’ (H : AddSubgroup G) โ†’ { x // x โˆˆ H } โ‰ƒ { x // x โˆˆ โ†‘AddSubgroup.opposite H }
AddSubgroup.oppositeEquiv
#align subgroup.opposite_equiv_symm_apply_coe 
Subgroup.oppositeEquiv_symm_apply_coe: โˆ€ {G : Type u_1} [inst : Group G] (H : Subgroup G) (b : { b // (fun x => x โˆˆ โ†‘opposite H) b }),
  โ†‘(โ†‘(oppositeEquiv H).symm b) = MulOpposite.unop โ†‘b
Subgroup.oppositeEquiv_symm_apply_coe

@[
to_additive: {G : Type u_1} โ†’
  [inst : AddGroup G] โ†’
    (H : AddSubgroup G) โ†’ [inst_1 : Encodable { x // x โˆˆ H }] โ†’ Encodable { x // x โˆˆ โ†‘AddSubgroup.opposite H }
to_additive]

instance: {G : Type u_1} โ†’
  [inst : Group G] โ†’ (H : Subgroup G) โ†’ [inst_1 : Encodable { x // x โˆˆ H }] โ†’ Encodable { x // x โˆˆ โ†‘opposite H }
instance (
H: Subgroup G
H : 
Subgroup: (G : Type ?u.3019) โ†’ [inst : Group G] โ†’ Type ?u.3019
Subgroup 
G: Type ?u.3013
G) [
Encodable: Type ?u.3027 โ†’ Type ?u.3027
Encodable 
H: Subgroup G
H] : 
Encodable: Type ?u.3174 โ†’ Type ?u.3174
Encodable (
opposite: {G : Type ?u.3175} โ†’ [inst : Group G] โ†’ Subgroup G โ‰ƒ Subgroup Gแตแต’แต–
opposite 
H: Subgroup G
H) :=
  
Encodable.ofEquiv: {ฮฒ : Type ?u.3455} โ†’ (ฮฑ : Type ?u.3454) โ†’ [inst : Encodable ฮฑ] โ†’ ฮฒ โ‰ƒ ฮฑ โ†’ Encodable ฮฒ
Encodable.ofEquiv 
H: Subgroup G
H 
H: Subgroup G
H.
oppositeEquiv: {G : Type ?u.3592} โ†’ [inst : Group G] โ†’ (H : Subgroup G) โ†’ { x // x โˆˆ H } โ‰ƒ { x // x โˆˆ โ†‘opposite H }
oppositeEquiv.
symm: {ฮฑ : Sort ?u.3598} โ†’ {ฮฒ : Sort ?u.3597} โ†’ ฮฑ โ‰ƒ ฮฒ โ†’ ฮฒ โ‰ƒ ฮฑ
symm

@[
to_additive: โˆ€ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) [inst_1 : Countable { x // x โˆˆ H }],
  Countable { x // x โˆˆ โ†‘AddSubgroup.opposite H }
to_additive]

instance: โˆ€ {G : Type u_1} [inst : Group G] (H : Subgroup G) [inst_1 : Countable { x // x โˆˆ H }],
  Countable { x // x โˆˆ โ†‘opposite H }
instance (
H: Subgroup G
H : 
Subgroup: (G : Type ?u.3777) โ†’ [inst : Group G] โ†’ Type ?u.3777
Subgroup 
G: Type ?u.3771
G) [
Countable: Sort ?u.3785 โ†’ Prop
Countable 
H: Subgroup G
H] : 
Countable: Sort ?u.3955 โ†’ Prop
Countable (
opposite: {G : Type ?u.3956} โ†’ [inst : Group G] โ†’ Subgroup G โ‰ƒ Subgroup Gแตแต’แต–
opposite 
H: Subgroup G
H) :=
  
Countable.of_equiv: โˆ€ {ฮฒ : Sort ?u.4255} (ฮฑ : Sort ?u.4256) [inst : Countable ฮฑ], ฮฑ โ‰ƒ ฮฒ โ†’ Countable ฮฒ
Countable.of_equiv 
H: Subgroup G
H 
H: Subgroup G
H.
oppositeEquiv: {G : Type ?u.4410} โ†’ [inst : Group G] โ†’ (H : Subgroup G) โ†’ { x // x โˆˆ H } โ‰ƒ { x // x โˆˆ โ†‘opposite H }
oppositeEquiv

@[
to_additive: โˆ€ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} (x g : G) (h : { x // x โˆˆ โ†‘AddSubgroup.opposite H }),
  h +แตฅ (g + x) = g + (h +แตฅ x)
to_additive]
theorem 
smul_opposite_mul: โˆ€ {H : Subgroup G} (x g : G) (h : { x // x โˆˆ โ†‘opposite H }), h โ€ข (g * x) = g * h โ€ข x
smul_opposite_mul {
H: Subgroup G
H : 
Subgroup: (G : Type ?u.4517) โ†’ [inst : Group G] โ†’ Type ?u.4517
Subgroup 
G: Type ?u.4511
G} (
x: G
x 
g: G
g : 
G: Type ?u.4511
G) (
h: { x // x โˆˆ โ†‘opposite H }
h : 
opposite: {G : Type ?u.4529} โ†’ [inst : Group G] โ†’ Subgroup G โ‰ƒ Subgroup Gแตแต’แต–
opposite 
H: Subgroup G
H) :
    
h: { x // x โˆˆ โ†‘opposite H }
h โ€ข (
g: G
g * 
x: G
x) = 
g: G
g * 
h: { x // x โˆˆ โ†‘opposite H }
h โ€ข 
x: G
x :=
  
mul_assoc: โˆ€ {G : Type ?u.6585} [inst : Semigroup G] (a b c : G), a * b * c = a * (b * c)
mul_assoc 
_: ?m.6586
_ 
_: ?m.6586
_ 
_: ?m.6586
_
#align subgroup.smul_opposite_mul 
Subgroup.smul_opposite_mul: โˆ€ {G : Type u_1} [inst : Group G] {H : Subgroup G} (x g : G) (h : { x // x โˆˆ โ†‘opposite H }), h โ€ข (g * x) = g * h โ€ข x
Subgroup.smul_opposite_mul
#align add_subgroup.vadd_opposite_add 
AddSubgroup.vadd_opposite_add: โˆ€ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} (x g : G) (h : { x // x โˆˆ โ†‘AddSubgroup.opposite H }),
  h +แตฅ (g + x) = g + (h +แตฅ x)
AddSubgroup.vadd_opposite_add

end Subgroup