Documentation

Mathlib.GroupTheory.Coset.Basic

Cosets #

This file develops the basic theory of left and right cosets.

When G is a group and a : G, s : Set G, with open scoped Pointwise we can write:

If instead G is an additive group, we can write (with open scoped Pointwise still)

Main definitions #

Notation #

TODO #

Properly merge with pointwise actions on sets, by renaming and deduplicating lemmas as appropriate.

theorem mem_leftAddCoset {α : Type u_1} [Add α] {s : Set α} {x : α} (a : α) (hxS : x s) :
a + x a +ᵥ s
theorem mem_leftCoset {α : Type u_1} [Mul α] {s : Set α} {x : α} (a : α) (hxS : x s) :
a * x a s
theorem mem_rightAddCoset {α : Type u_1} [Add α] {s : Set α} {x : α} (a : α) (hxS : x s) :
theorem mem_rightCoset {α : Type u_1} [Mul α] {s : Set α} {x : α} (a : α) (hxS : x s) :
def LeftAddCosetEquivalence {α : Type u_1} [Add α] (s : Set α) (a : α) (b : α) :

Equality of two left cosets a + s and b + s.

Equations
def LeftCosetEquivalence {α : Type u_1} [Mul α] (s : Set α) (a : α) (b : α) :

Equality of two left cosets a * s and b * s.

Equations
def RightAddCosetEquivalence {α : Type u_1} [Add α] (s : Set α) (a : α) (b : α) :

Equality of two right cosets s + a and s + b.

Equations
def RightCosetEquivalence {α : Type u_1} [Mul α] (s : Set α) (a : α) (b : α) :

Equality of two right cosets s * a and s * b.

Equations
theorem leftAddCoset_assoc {α : Type u_1} [AddSemigroup α] (s : Set α) (a : α) (b : α) :
a +ᵥ (b +ᵥ s) = a + b +ᵥ s
theorem leftCoset_assoc {α : Type u_1} [Semigroup α] (s : Set α) (a : α) (b : α) :
a b s = (a * b) s
theorem rightAddCoset_assoc {α : Type u_1} [AddSemigroup α] (s : Set α) (a : α) (b : α) :
theorem rightCoset_assoc {α : Type u_1} [Semigroup α] (s : Set α) (a : α) (b : α) :
theorem leftAddCoset_rightAddCoset {α : Type u_1} [AddSemigroup α] (s : Set α) (a : α) (b : α) :
theorem leftCoset_rightCoset {α : Type u_1} [Semigroup α] (s : Set α) (a : α) (b : α) :
theorem zero_leftAddCoset {α : Type u_1} [AddMonoid α] (s : Set α) :
0 +ᵥ s = s
theorem one_leftCoset {α : Type u_1} [Monoid α] (s : Set α) :
1 s = s
theorem rightAddCoset_zero {α : Type u_1} [AddMonoid α] (s : Set α) :
theorem rightCoset_one {α : Type u_1} [Monoid α] (s : Set α) :
theorem mem_own_leftAddCoset {α : Type u_1} [AddMonoid α] (s : AddSubmonoid α) (a : α) :
a a +ᵥ s
theorem mem_own_leftCoset {α : Type u_1} [Monoid α] (s : Submonoid α) (a : α) :
a a s
theorem mem_own_rightAddCoset {α : Type u_1} [AddMonoid α] (s : AddSubmonoid α) (a : α) :
theorem mem_own_rightCoset {α : Type u_1} [Monoid α] (s : Submonoid α) (a : α) :
theorem mem_leftAddCoset_leftAddCoset {α : Type u_1} [AddMonoid α] (s : AddSubmonoid α) {a : α} (ha : a +ᵥ s = s) :
a s
theorem mem_leftCoset_leftCoset {α : Type u_1} [Monoid α] (s : Submonoid α) {a : α} (ha : a s = s) :
a s
theorem mem_rightAddCoset_rightAddCoset {α : Type u_1} [AddMonoid α] (s : AddSubmonoid α) {a : α} (ha : AddOpposite.op a +ᵥ s = s) :
a s
theorem mem_rightCoset_rightCoset {α : Type u_1} [Monoid α] (s : Submonoid α) {a : α} (ha : MulOpposite.op a s = s) :
a s
theorem mem_leftAddCoset_iff {α : Type u_1} [AddGroup α] {s : Set α} {x : α} (a : α) :
x a +ᵥ s -a + x s
theorem mem_leftCoset_iff {α : Type u_1} [Group α] {s : Set α} {x : α} (a : α) :
x a s a⁻¹ * x s
theorem mem_rightAddCoset_iff {α : Type u_1} [AddGroup α] {s : Set α} {x : α} (a : α) :
theorem mem_rightCoset_iff {α : Type u_1} [Group α] {s : Set α} {x : α} (a : α) :
theorem leftAddCoset_mem_leftAddCoset {α : Type u_1} [AddGroup α] (s : AddSubgroup α) {a : α} (ha : a s) :
a +ᵥ s = s
theorem leftCoset_mem_leftCoset {α : Type u_1} [Group α] (s : Subgroup α) {a : α} (ha : a s) :
a s = s
theorem rightAddCoset_mem_rightAddCoset {α : Type u_1} [AddGroup α] (s : AddSubgroup α) {a : α} (ha : a s) :
AddOpposite.op a +ᵥ s = s
theorem rightCoset_mem_rightCoset {α : Type u_1} [Group α] (s : Subgroup α) {a : α} (ha : a s) :
MulOpposite.op a s = s
theorem orbit_addSubgroup_eq_rightCoset {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (a : α) :
theorem orbit_subgroup_eq_rightCoset {α : Type u_1} [Group α] (s : Subgroup α) (a : α) :
theorem orbit_addSubgroup_eq_self_of_mem {α : Type u_1} [AddGroup α] (s : AddSubgroup α) {a : α} (ha : a s) :
AddAction.orbit (↥s) a = s
theorem orbit_subgroup_eq_self_of_mem {α : Type u_1} [Group α] (s : Subgroup α) {a : α} (ha : a s) :
MulAction.orbit (↥s) a = s
theorem orbit_addSubgroup_zero_eq_self {α : Type u_1} [AddGroup α] (s : AddSubgroup α) :
AddAction.orbit (↥s) 0 = s
theorem orbit_subgroup_one_eq_self {α : Type u_1} [Group α] (s : Subgroup α) :
MulAction.orbit (↥s) 1 = s
theorem eq_addCosets_of_normal {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (N : s.Normal) (g : α) :
g +ᵥ s = AddOpposite.op g +ᵥ s
theorem eq_cosets_of_normal {α : Type u_1} [Group α] (s : Subgroup α) (N : s.Normal) (g : α) :
g s = MulOpposite.op g s
theorem normal_of_eq_addCosets {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (h : ∀ (g : α), g +ᵥ s = AddOpposite.op g +ᵥ s) :
s.Normal
theorem normal_of_eq_cosets {α : Type u_1} [Group α] (s : Subgroup α) (h : ∀ (g : α), g s = MulOpposite.op g s) :
s.Normal
theorem normal_iff_eq_addCosets {α : Type u_1} [AddGroup α] (s : AddSubgroup α) :
s.Normal ∀ (g : α), g +ᵥ s = AddOpposite.op g +ᵥ s
theorem normal_iff_eq_cosets {α : Type u_1} [Group α] (s : Subgroup α) :
s.Normal ∀ (g : α), g s = MulOpposite.op g s
theorem leftAddCoset_eq_iff {α : Type u_1} [AddGroup α] (s : AddSubgroup α) {x : α} {y : α} :
x +ᵥ s = y +ᵥ s -x + y s
theorem leftCoset_eq_iff {α : Type u_1} [Group α] (s : Subgroup α) {x : α} {y : α} :
x s = y s x⁻¹ * y s
theorem rightAddCoset_eq_iff {α : Type u_1} [AddGroup α] (s : AddSubgroup α) {x : α} {y : α} :
theorem rightCoset_eq_iff {α : Type u_1} [Group α] (s : Subgroup α) {x : α} {y : α} :
def QuotientAddGroup.leftRel {α : Type u_1} [AddGroup α] (s : AddSubgroup α) :

The equivalence relation corresponding to the partition of a group by left cosets of a subgroup.

Equations
def QuotientGroup.leftRel {α : Type u_1} [Group α] (s : Subgroup α) :

The equivalence relation corresponding to the partition of a group by left cosets of a subgroup.

Equations
theorem QuotientAddGroup.leftRel_apply {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {x : α} {y : α} :
theorem QuotientGroup.leftRel_apply {α : Type u_1} [Group α] {s : Subgroup α} {x : α} {y : α} :
theorem QuotientAddGroup.leftRel_eq {α : Type u_1} [AddGroup α] (s : AddSubgroup α) :
(QuotientAddGroup.leftRel s) = fun (x y : α) => -x + y s
theorem QuotientGroup.leftRel_eq {α : Type u_1} [Group α] (s : Subgroup α) :
(QuotientGroup.leftRel s) = fun (x y : α) => x⁻¹ * y s
theorem QuotientAddGroup.leftRelDecidable.proof_1 {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (x : α) (y : α) :
Decidable ((QuotientAddGroup.leftRel s) x y) = Decidable ((fun (x y : α) => -x + y s) x y)
Equations
instance QuotientGroup.leftRelDecidable {α : Type u_1} [Group α] (s : Subgroup α) [DecidablePred fun (x : α) => x s] :
Equations

α ⧸ s is the quotient type representing the left cosets of s. If s is a normal subgroup, α ⧸ s is a group

Equations

α ⧸ s is the quotient type representing the left cosets of s. If s is a normal subgroup, α ⧸ s is a group

Equations
def QuotientAddGroup.rightRel {α : Type u_1} [AddGroup α] (s : AddSubgroup α) :

The equivalence relation corresponding to the partition of a group by right cosets of a subgroup.

Equations
def QuotientGroup.rightRel {α : Type u_1} [Group α] (s : Subgroup α) :

The equivalence relation corresponding to the partition of a group by right cosets of a subgroup.

Equations
theorem QuotientAddGroup.rightRel_apply {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {x : α} {y : α} :
theorem QuotientGroup.rightRel_apply {α : Type u_1} [Group α] {s : Subgroup α} {x : α} {y : α} :
theorem QuotientAddGroup.rightRel_eq {α : Type u_1} [AddGroup α] (s : AddSubgroup α) :
(QuotientAddGroup.rightRel s) = fun (x y : α) => y + -x s
theorem QuotientGroup.rightRel_eq {α : Type u_1} [Group α] (s : Subgroup α) :
(QuotientGroup.rightRel s) = fun (x y : α) => y * x⁻¹ s
Equations
theorem QuotientAddGroup.rightRelDecidable.proof_1 {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (x : α) (y : α) :
Decidable ((QuotientAddGroup.rightRel s) x y) = Decidable ((fun (x y : α) => y + -x s) x y)
instance QuotientGroup.rightRelDecidable {α : Type u_1} [Group α] (s : Subgroup α) [DecidablePred fun (x : α) => x s] :
Equations
theorem QuotientAddGroup.quotientRightRelEquivQuotientLeftRel.proof_2 {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (a : α) (b : α) :
(QuotientAddGroup.leftRel s) a b(QuotientAddGroup.rightRel s) ((fun (g : α) => -g) a) ((fun (g : α) => -g) b)
theorem QuotientAddGroup.quotientRightRelEquivQuotientLeftRel.proof_4 {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (g : α s) :
Quotient.map' (fun (g : α) => -g) (Quotient.map' (fun (g : α) => -g) g) = g
theorem QuotientAddGroup.quotientRightRelEquivQuotientLeftRel.proof_1 {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (a : α) (b : α) :
(QuotientAddGroup.rightRel s) a b(QuotientAddGroup.leftRel s) ((fun (g : α) => -g) a) ((fun (g : α) => -g) b)
theorem QuotientAddGroup.quotientRightRelEquivQuotientLeftRel.proof_3 {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (g : Quotient (QuotientAddGroup.rightRel s)) :
Quotient.map' (fun (g : α) => -g) (Quotient.map' (fun (g : α) => -g) g) = g

Right cosets are in bijection with left cosets.

Equations

Right cosets are in bijection with left cosets.

Equations
@[reducible, inline]
abbrev QuotientAddGroup.mk {α : Type u_1} [AddGroup α] {s : AddSubgroup α} (a : α) :
α s

The canonical map from an AddGroup α to the quotient α ⧸ s.

Equations
@[reducible, inline]
abbrev QuotientGroup.mk {α : Type u_1} [Group α] {s : Subgroup α} (a : α) :
α s

The canonical map from a group α to the quotient α ⧸ s.

Equations
theorem QuotientAddGroup.mk_surjective {α : Type u_1} [AddGroup α] {s : AddSubgroup α} :
Function.Surjective QuotientAddGroup.mk
theorem QuotientGroup.mk_surjective {α : Type u_1} [Group α] {s : Subgroup α} :
Function.Surjective QuotientGroup.mk
@[simp]
theorem QuotientAddGroup.range_mk {α : Type u_1} [AddGroup α] {s : AddSubgroup α} :
Set.range QuotientAddGroup.mk = Set.univ
@[simp]
theorem QuotientGroup.range_mk {α : Type u_1} [Group α] {s : Subgroup α} :
Set.range QuotientGroup.mk = Set.univ
theorem QuotientAddGroup.induction_on {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {C : α sProp} (x : α s) (H : ∀ (z : α), C z) :
C x
theorem QuotientGroup.induction_on {α : Type u_1} [Group α] {s : Subgroup α} {C : α sProp} (x : α s) (H : ∀ (z : α), C z) :
C x
instance QuotientAddGroup.instCoeQuotientAddSubgroup {α : Type u_1} [AddGroup α] {s : AddSubgroup α} :
Coe α (α s)
Equations
  • QuotientAddGroup.instCoeQuotientAddSubgroup = { coe := QuotientAddGroup.mk }
instance QuotientGroup.instCoeQuotientSubgroup {α : Type u_1} [Group α] {s : Subgroup α} :
Coe α (α s)
Equations
  • QuotientGroup.instCoeQuotientSubgroup = { coe := QuotientGroup.mk }
@[deprecated]
theorem QuotientGroup.induction_on' {α : Type u_1} [Group α] {s : Subgroup α} {C : α sProp} (x : α s) (H : ∀ (z : α), C z) :
C x

Alias of QuotientGroup.induction_on.

@[deprecated]
theorem QuotientAddGroup.induction_on' {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {C : α sProp} (x : α s) (H : ∀ (z : α), C z) :
C x
@[simp]
theorem QuotientAddGroup.quotient_liftOn_mk {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {β : Sort u_2} (f : αβ) (h : ∀ (a b : α), (QuotientAddGroup.leftRel s) a bf a = f b) (x : α) :
Quotient.liftOn' (↑x) f h = f x
@[simp]
theorem QuotientGroup.quotient_liftOn_mk {α : Type u_1} [Group α] {s : Subgroup α} {β : Sort u_2} (f : αβ) (h : ∀ (a b : α), (QuotientGroup.leftRel s) a bf a = f b) (x : α) :
Quotient.liftOn' (↑x) f h = f x
theorem QuotientAddGroup.forall_mk {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {C : α sProp} :
(∀ (x : α s), C x) ∀ (x : α), C x
theorem QuotientGroup.forall_mk {α : Type u_1} [Group α] {s : Subgroup α} {C : α sProp} :
(∀ (x : α s), C x) ∀ (x : α), C x
theorem QuotientAddGroup.exists_mk {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {C : α sProp} :
(∃ (x : α s), C x) ∃ (x : α), C x
theorem QuotientGroup.exists_mk {α : Type u_1} [Group α] {s : Subgroup α} {C : α sProp} :
(∃ (x : α s), C x) ∃ (x : α), C x
theorem QuotientAddGroup.eq {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {a : α} {b : α} :
a = b -a + b s
theorem QuotientGroup.eq {α : Type u_1} [Group α] {s : Subgroup α} {a : α} {b : α} :
a = b a⁻¹ * b s
@[deprecated]
theorem QuotientGroup.eq' {α : Type u_1} [Group α] {s : Subgroup α} {a : α} {b : α} :
a = b a⁻¹ * b s

Alias of QuotientGroup.eq.

@[deprecated]
theorem QuotientAddGroup.eq' {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {a : α} {b : α} :
a = b -a + b s
theorem QuotientAddGroup.out_eq' {α : Type u_1} [AddGroup α] {s : AddSubgroup α} (a : α s) :
(Quotient.out' a) = a
theorem QuotientGroup.out_eq' {α : Type u_1} [Group α] {s : Subgroup α} (a : α s) :
(Quotient.out' a) = a
theorem QuotientAddGroup.strictMono_comap_prod_image {α : Type u_1} [AddGroup α] (s : AddSubgroup α) :
StrictMono fun (t : AddSubgroup α) => (AddSubgroup.comap s.subtype t, QuotientAddGroup.mk '' t)

Given an additive subgroup s, the function that sends an additive subgroup t to the pair consisting of its intersection with s and its image in the quotient α ⧸ s is strictly monotone, even though it is not injective in general.

theorem QuotientGroup.strictMono_comap_prod_image {α : Type u_1} [Group α] (s : Subgroup α) :
StrictMono fun (t : Subgroup α) => (Subgroup.comap s.subtype t, QuotientGroup.mk '' t)

Given a subgroup s, the function that sends a subgroup t to the pair consisting of its intersection with s and its image in the quotient α ⧸ s is strictly monotone, even though it is not injective in general.

theorem QuotientAddGroup.mk_out'_eq_mul {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (g : α) :
∃ (h : s), Quotient.out' g = g + h
theorem QuotientGroup.mk_out'_eq_mul {α : Type u_1} [Group α] (s : Subgroup α) (g : α) :
∃ (h : s), Quotient.out' g = g * h
@[simp]
theorem QuotientAddGroup.mk_add_of_mem {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {b : α} (a : α) (hb : b s) :
(a + b) = a
@[simp]
theorem QuotientGroup.mk_mul_of_mem {α : Type u_1} [Group α] {s : Subgroup α} {b : α} (a : α) (hb : b s) :
(a * b) = a
theorem QuotientAddGroup.eq_class_eq_leftCoset {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (g : α) :
{x : α | x = g} = g +ᵥ s
theorem QuotientGroup.eq_class_eq_leftCoset {α : Type u_1} [Group α] (s : Subgroup α) (g : α) :
{x : α | x = g} = g s
theorem QuotientAddGroup.preimage_image_mk {α : Type u_1} [AddGroup α] (N : AddSubgroup α) (s : Set α) :
QuotientAddGroup.mk ⁻¹' (QuotientAddGroup.mk '' s) = ⋃ (x : N), (fun (x_1 : α) => x_1 + x) ⁻¹' s
theorem QuotientGroup.preimage_image_mk {α : Type u_1} [Group α] (N : Subgroup α) (s : Set α) :
QuotientGroup.mk ⁻¹' (QuotientGroup.mk '' s) = ⋃ (x : N), (fun (x_1 : α) => x_1 * x) ⁻¹' s
theorem QuotientAddGroup.preimage_image_mk_eq_iUnion_image {α : Type u_1} [AddGroup α] (N : AddSubgroup α) (s : Set α) :
QuotientAddGroup.mk ⁻¹' (QuotientAddGroup.mk '' s) = ⋃ (x : N), (fun (x_1 : α) => x_1 + x) '' s
theorem QuotientGroup.preimage_image_mk_eq_iUnion_image {α : Type u_1} [Group α] (N : Subgroup α) (s : Set α) :
QuotientGroup.mk ⁻¹' (QuotientGroup.mk '' s) = ⋃ (x : N), (fun (x_1 : α) => x_1 * x) '' s
theorem QuotientAddGroup.preimage_image_mk_eq_add {α : Type u_1} [AddGroup α] (N : AddSubgroup α) (s : Set α) :
QuotientAddGroup.mk ⁻¹' (QuotientAddGroup.mk '' s) = s + N
theorem QuotientGroup.preimage_image_mk_eq_mul {α : Type u_1} [Group α] (N : Subgroup α) (s : Set α) :
QuotientGroup.mk ⁻¹' (QuotientGroup.mk '' s) = s * N
theorem AddSubgroup.leftCosetEquivAddSubgroup.proof_4 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} (g : α) :
∀ (x : s), (fun (x : (g +ᵥ s)) => -g + x, ) ((fun (x : s) => g + x, ) x) = x
theorem AddSubgroup.leftCosetEquivAddSubgroup.proof_1 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} (g : α) (x : (g +ᵥ s)) :
-g + x s
def AddSubgroup.leftCosetEquivAddSubgroup {α : Type u_1} [AddGroup α] {s : AddSubgroup α} (g : α) :
(g +ᵥ s) s

The natural bijection between the cosets g + s and s.

Equations
theorem AddSubgroup.leftCosetEquivAddSubgroup.proof_2 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} (g : α) (x : s) :
as, (fun (x : α) => g +ᵥ x) a = g + x
theorem AddSubgroup.leftCosetEquivAddSubgroup.proof_3 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} (g : α) :
∀ (x : (g +ᵥ s)), (fun (x : s) => g + x, ) ((fun (x : (g +ᵥ s)) => -g + x, ) x) = x
def Subgroup.leftCosetEquivSubgroup {α : Type u_1} [Group α] {s : Subgroup α} (g : α) :
(g s) s

The natural bijection between a left coset g * s and s.

Equations
def AddSubgroup.rightCosetEquivAddSubgroup {α : Type u_1} [AddGroup α] {s : AddSubgroup α} (g : α) :
(AddOpposite.op g +ᵥ s) s

The natural bijection between the cosets s + g and s.

Equations
theorem AddSubgroup.rightCosetEquivAddSubgroup.proof_4 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} (g : α) :
∀ (x : s), (fun (x : (AddOpposite.op g +ᵥ s)) => x + -g, ) ((fun (x : s) => x + g, ) x) = x
theorem AddSubgroup.rightCosetEquivAddSubgroup.proof_1 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} (g : α) (x : (AddOpposite.op g +ᵥ s)) :
x + -g s
theorem AddSubgroup.rightCosetEquivAddSubgroup.proof_3 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} (g : α) :
∀ (x : (AddOpposite.op g +ᵥ s)), (fun (x : s) => x + g, ) ((fun (x : (AddOpposite.op g +ᵥ s)) => x + -g, ) x) = x
theorem AddSubgroup.rightCosetEquivAddSubgroup.proof_2 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} (g : α) (x : s) :
as, (fun (x : α) => AddOpposite.op g +ᵥ x) a = x + g
def Subgroup.rightCosetEquivSubgroup {α : Type u_1} [Group α] {s : Subgroup α} (g : α) :
(MulOpposite.op g s) s

The natural bijection between a right coset s * g and s.

Equations
theorem AddSubgroup.addGroupEquivQuotientProdAddSubgroup.proof_1 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} (L : α s) :
({ x : α // x = L } (Quotient.out' L +ᵥ s)) = ({ x : α // x = L } {x : α | x = (Quotient.out' L)})
theorem AddSubgroup.addGroupEquivQuotientProdAddSubgroup.proof_2 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} (L : α s) :
({ x : α // Quotient.mk'' x = L } { x : α // Quotient.mk'' x = Quotient.mk'' (Quotient.out' L) }) = ({ x : α // Quotient.mk'' x = L } { x : α // Quotient.mk'' x = L })
noncomputable def AddSubgroup.addGroupEquivQuotientProdAddSubgroup {α : Type u_1} [AddGroup α] {s : AddSubgroup α} :
α (α s) × s

A (non-canonical) bijection between an add_group α and the product (α/s) × s

Equations
  • One or more equations did not get rendered due to their size.
noncomputable def Subgroup.groupEquivQuotientProdSubgroup {α : Type u_1} [Group α] {s : Subgroup α} :
α (α s) × s

A (non-canonical) bijection between a group α and the product (α/s) × s

Equations
  • One or more equations did not get rendered due to their size.
theorem AddSubgroup.quotientEquivOfEq.proof_1 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h : s = t) (_a : α) (_b : α) (h' : (QuotientAddGroup.leftRel s) _a _b) :
def AddSubgroup.quotientEquivOfEq {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h : s = t) :
α s α t

If two subgroups M and N of G are equal, their quotients are in bijection.

Equations
theorem AddSubgroup.quotientEquivOfEq.proof_2 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h : s = t) (_a : α) (_b : α) (h' : (QuotientAddGroup.leftRel t) _a _b) :
theorem AddSubgroup.quotientEquivOfEq.proof_4 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h : s = t) (q : α t) :
Quotient.map' id (Quotient.map' id q) = q
theorem AddSubgroup.quotientEquivOfEq.proof_3 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h : s = t) (q : α s) :
Quotient.map' id (Quotient.map' id q) = q
def Subgroup.quotientEquivOfEq {α : Type u_1} [Group α] {s : Subgroup α} {t : Subgroup α} (h : s = t) :
α s α t

If two subgroups M and N of G are equal, their quotients are in bijection.

Equations
theorem Subgroup.quotientEquivOfEq_mk {α : Type u_1} [Group α] {s : Subgroup α} {t : Subgroup α} (h : s = t) (a : α) :
theorem AddSubgroup.quotientEquivSumOfLE'.proof_5 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h_le : s t) (f : α tα) (hf : Function.RightInverse f QuotientAddGroup.mk) (q : Quotient (QuotientAddGroup.leftRel s)) :
(fun (a : (α t) × t s.addSubgroupOf t) => Quotient.map' (fun (b : t) => f a.1 + b) a.2) ((fun (a : α s) => (Quotient.map' id a, Quotient.map' (fun (g : α) => -f (Quotient.mk'' g) + g, ) a)) q) = q
theorem AddSubgroup.quotientEquivSumOfLE'.proof_4 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (f : α tα) (a : (α t) × t s.addSubgroupOf t) (b : t) (c : t) (h : (QuotientAddGroup.leftRel (s.addSubgroupOf t)) b c) :
(QuotientAddGroup.leftRel s) ((fun (b : t) => f a.1 + b) b) ((fun (b : t) => f a.1 + b) c)
theorem AddSubgroup.quotientEquivSumOfLE'.proof_1 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h_le : s t) :
∀ (x x_1 : α), (QuotientAddGroup.leftRel s) x x_1(QuotientAddGroup.leftRel t) (id x) (id x_1)
def AddSubgroup.quotientEquivSumOfLE' {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h_le : s t) (f : α tα) (hf : Function.RightInverse f QuotientAddGroup.mk) :
α s (α t) × t s.addSubgroupOf t

If H ≤ K, then G/H ≃ G/K × K/H constructively, using the provided right inverse of the quotient map G → G/K. The classical version is AddSubgroup.quotientEquivSumOfLE.

Equations
  • One or more equations did not get rendered due to their size.
theorem AddSubgroup.quotientEquivSumOfLE'.proof_3 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h_le : s t) (f : α tα) (hf : Function.RightInverse f QuotientAddGroup.mk) (b : α) (c : α) (h : (QuotientAddGroup.leftRel s) b c) :
(QuotientAddGroup.leftRel (s.addSubgroupOf t)) ((fun (g : α) => -f (Quotient.mk'' g) + g, ) b) ((fun (g : α) => -f (Quotient.mk'' g) + g, ) c)
theorem AddSubgroup.quotientEquivSumOfLE'.proof_6 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h_le : s t✝) (f : α t✝α) (hf : Function.RightInverse f QuotientAddGroup.mk) (t : (α t✝) × t✝ s.addSubgroupOf t✝) :
(fun (a : α s) => (Quotient.map' id a, Quotient.map' (fun (g : α) => -f (Quotient.mk'' g) + g, ) a)) ((fun (a : (α t✝) × t✝ s.addSubgroupOf t✝) => Quotient.map' (fun (b : t✝) => f a.1 + b) a.2) t) = t
theorem AddSubgroup.quotientEquivSumOfLE'.proof_2 {α : Type u_1} [AddGroup α] {t : AddSubgroup α} (f : α tα) (hf : Function.RightInverse f QuotientAddGroup.mk) (g : α) :
-f (Quotient.mk'' g) + g t
@[simp]
theorem Subgroup.quotientEquivProdOfLE'_symm_apply {α : Type u_1} [Group α] {s : Subgroup α} {t : Subgroup α} (h_le : s t) (f : α tα) (hf : Function.RightInverse f QuotientGroup.mk) (a : (α t) × t s.subgroupOf t) :
(Subgroup.quotientEquivProdOfLE' h_le f hf).symm a = Quotient.map' (fun (b : t) => f a.1 * b) a.2
@[simp]
theorem AddSubgroup.quotientEquivSumOfLE'_symm_apply {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h_le : s t) (f : α tα) (hf : Function.RightInverse f QuotientAddGroup.mk) (a : (α t) × t s.addSubgroupOf t) :
(AddSubgroup.quotientEquivSumOfLE' h_le f hf).symm a = Quotient.map' (fun (b : t) => f a.1 + b) a.2
@[simp]
theorem Subgroup.quotientEquivProdOfLE'_apply {α : Type u_1} [Group α] {s : Subgroup α} {t : Subgroup α} (h_le : s t) (f : α tα) (hf : Function.RightInverse f QuotientGroup.mk) (a : α s) :
(Subgroup.quotientEquivProdOfLE' h_le f hf) a = (Quotient.map' id a, Quotient.map' (fun (g : α) => (f (Quotient.mk'' g))⁻¹ * g, ) a)
@[simp]
theorem AddSubgroup.quotientEquivSumOfLE'_apply {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h_le : s t) (f : α tα) (hf : Function.RightInverse f QuotientAddGroup.mk) (a : α s) :
(AddSubgroup.quotientEquivSumOfLE' h_le f hf) a = (Quotient.map' id a, Quotient.map' (fun (g : α) => -f (Quotient.mk'' g) + g, ) a)
def Subgroup.quotientEquivProdOfLE' {α : Type u_1} [Group α] {s : Subgroup α} {t : Subgroup α} (h_le : s t) (f : α tα) (hf : Function.RightInverse f QuotientGroup.mk) :
α s (α t) × t s.subgroupOf t

If H ≤ K, then G/H ≃ G/K × K/H constructively, using the provided right inverse of the quotient map G → G/K. The classical version is Subgroup.quotientEquivProdOfLE.

Equations
  • One or more equations did not get rendered due to their size.
noncomputable def AddSubgroup.quotientEquivSumOfLE {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h_le : s t) :
α s (α t) × t s.addSubgroupOf t

If H ≤ K, then G/H ≃ G/K × K/H nonconstructively. The constructive version is quotientEquivProdOfLE'.

Equations
@[simp]
theorem AddSubgroup.quotientEquivSumOfLE_apply {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h_le : s t) (a : α s) :
(AddSubgroup.quotientEquivSumOfLE h_le) a = (Quotient.map' id a, Quotient.map' (fun (g : α) => -(Quotient.mk'' g).out' + g, ) a)
@[simp]
theorem Subgroup.quotientEquivProdOfLE_symm_apply {α : Type u_1} [Group α] {s : Subgroup α} {t : Subgroup α} (h_le : s t) (a : (α t) × t s.subgroupOf t) :
(Subgroup.quotientEquivProdOfLE h_le).symm a = Quotient.map' (fun (b : t) => Quotient.out' a.1 * b) a.2
@[simp]
theorem AddSubgroup.quotientEquivSumOfLE_symm_apply {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h_le : s t) (a : (α t) × t s.addSubgroupOf t) :
(AddSubgroup.quotientEquivSumOfLE h_le).symm a = Quotient.map' (fun (b : t) => Quotient.out' a.1 + b) a.2
@[simp]
theorem Subgroup.quotientEquivProdOfLE_apply {α : Type u_1} [Group α] {s : Subgroup α} {t : Subgroup α} (h_le : s t) (a : α s) :
(Subgroup.quotientEquivProdOfLE h_le) a = (Quotient.map' id a, Quotient.map' (fun (g : α) => (Quotient.mk'' g).out'⁻¹ * g, ) a)
noncomputable def Subgroup.quotientEquivProdOfLE {α : Type u_1} [Group α] {s : Subgroup α} {t : Subgroup α} (h_le : s t) :
α s (α t) × t s.subgroupOf t

If H ≤ K, then G/H ≃ G/K × K/H nonconstructively. The constructive version is quotientEquivProdOfLE'.

Equations
def AddSubgroup.quotientAddSubgroupOfEmbeddingOfLE {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (H : AddSubgroup α) (h : s t) :
s H.addSubgroupOf s t H.addSubgroupOf t

If s ≤ t, then there is an embedding s ⧸ H.addSubgroupOf s ↪ t ⧸ H.addSubgroupOf t.

Equations
theorem AddSubgroup.quotientAddSubgroupOfEmbeddingOfLE.proof_2 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (H : AddSubgroup α) (h : s t) (q₁ : Quotient (QuotientAddGroup.leftRel (H.addSubgroupOf s))) (q₂ : Quotient (QuotientAddGroup.leftRel (H.addSubgroupOf s))) :
Quotient.map' (AddSubgroup.inclusion h) q₁ = Quotient.map' (AddSubgroup.inclusion h) q₂q₁ = q₂
theorem AddSubgroup.quotientAddSubgroupOfEmbeddingOfLE.proof_1 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (H : AddSubgroup α) (h : s t) (a : s) (b : s) :
(QuotientAddGroup.leftRel (H.addSubgroupOf s)) a b(QuotientAddGroup.leftRel (H.addSubgroupOf t)) ((AddSubgroup.inclusion h) a) ((AddSubgroup.inclusion h) b)
def Subgroup.quotientSubgroupOfEmbeddingOfLE {α : Type u_1} [Group α] {s : Subgroup α} {t : Subgroup α} (H : Subgroup α) (h : s t) :
s H.subgroupOf s t H.subgroupOf t

If s ≤ t, then there is an embedding s ⧸ H.subgroupOf s ↪ t ⧸ H.subgroupOf t.

Equations
@[simp]
theorem Subgroup.quotientSubgroupOfEmbeddingOfLE_apply_mk {α : Type u_1} [Group α] {s : Subgroup α} {t : Subgroup α} (H : Subgroup α) (h : s t) (g : s) :
def AddSubgroup.quotientAddSubgroupOfMapOfLE {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (H : AddSubgroup α) (h : s t) :
H s.addSubgroupOf HH t.addSubgroupOf H

If s ≤ t, then there is a map H ⧸ s.addSubgroupOf H → H ⧸ t.addSubgroupOf H.

Equations
theorem AddSubgroup.quotientAddSubgroupOfMapOfLE.proof_1 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (H : AddSubgroup α) (h : s t) (a : H) (b : H) :
(QuotientAddGroup.leftRel (s.addSubgroupOf H)) a b(QuotientAddGroup.leftRel (t.addSubgroupOf H)) (id a) (id b)
def Subgroup.quotientSubgroupOfMapOfLE {α : Type u_1} [Group α] {s : Subgroup α} {t : Subgroup α} (H : Subgroup α) (h : s t) :
H s.subgroupOf HH t.subgroupOf H

If s ≤ t, then there is a map H ⧸ s.subgroupOf H → H ⧸ t.subgroupOf H.

Equations
@[simp]
theorem AddSubgroup.quotientAddSubgroupOfMapOfLE_apply_mk {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (H : AddSubgroup α) (h : s t) (g : H) :
@[simp]
theorem Subgroup.quotientSubgroupOfMapOfLE_apply_mk {α : Type u_1} [Group α] {s : Subgroup α} {t : Subgroup α} (H : Subgroup α) (h : s t) (g : H) :
theorem AddSubgroup.quotientMapOfLE.proof_1 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h : s t) (a : α) (b : α) :
def AddSubgroup.quotientMapOfLE {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h : s t) :
α sα t

If s ≤ t, then there is a map α ⧸ s → α ⧸ t.

Equations
def Subgroup.quotientMapOfLE {α : Type u_1} [Group α] {s : Subgroup α} {t : Subgroup α} (h : s t) :
α sα t

If s ≤ t, then there is a map α ⧸ s → α ⧸ t.

Equations
@[simp]
theorem AddSubgroup.quotientMapOfLE_apply_mk {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h : s t) (g : α) :
@[simp]
theorem Subgroup.quotientMapOfLE_apply_mk {α : Type u_1} [Group α] {s : Subgroup α} {t : Subgroup α} (h : s t) (g : α) :
theorem AddSubgroup.quotientiInfAddSubgroupOfEmbedding.proof_1 {α : Type u_1} [AddGroup α] {ι : Type u_2} (f : ιAddSubgroup α) (i : ι) :
iInf f f i
theorem AddSubgroup.quotientiInfAddSubgroupOfEmbedding.proof_2 {α : Type u_1} [AddGroup α] {ι : Type u_2} (f : ιAddSubgroup α) (H : AddSubgroup α) (q₁ : Quotient (QuotientAddGroup.leftRel ((⨅ (i : ι), f i).addSubgroupOf H))) (q₂ : Quotient (QuotientAddGroup.leftRel ((⨅ (i : ι), f i).addSubgroupOf H))) :
(fun (q : H (⨅ (i : ι), f i).addSubgroupOf H) (i : ι) => AddSubgroup.quotientAddSubgroupOfMapOfLE H q) q₁ = (fun (q : H (⨅ (i : ι), f i).addSubgroupOf H) (i : ι) => AddSubgroup.quotientAddSubgroupOfMapOfLE H q) q₂q₁ = q₂
def AddSubgroup.quotientiInfAddSubgroupOfEmbedding {α : Type u_1} [AddGroup α] {ι : Type u_2} (f : ιAddSubgroup α) (H : AddSubgroup α) :
H (⨅ (i : ι), f i).addSubgroupOf H (i : ι) → H (f i).addSubgroupOf H

The natural embedding H ⧸ (⨅ i, f i).addSubgroupOf H) ↪ Π i, H ⧸ (f i).addSubgroupOf H.

Equations
@[simp]
theorem AddSubgroup.quotientiInfAddSubgroupOfEmbedding_apply {α : Type u_1} [AddGroup α] {ι : Type u_2} (f : ιAddSubgroup α) (H : AddSubgroup α) (q : H (⨅ (i : ι), f i).addSubgroupOf H) (i : ι) :
@[simp]
theorem Subgroup.quotientiInfSubgroupOfEmbedding_apply {α : Type u_1} [Group α] {ι : Type u_2} (f : ιSubgroup α) (H : Subgroup α) (q : H (⨅ (i : ι), f i).subgroupOf H) (i : ι) :
def Subgroup.quotientiInfSubgroupOfEmbedding {α : Type u_1} [Group α] {ι : Type u_2} (f : ιSubgroup α) (H : Subgroup α) :
H (⨅ (i : ι), f i).subgroupOf H (i : ι) → H (f i).subgroupOf H

The natural embedding H ⧸ (⨅ i, f i).subgroupOf H ↪ Π i, H ⧸ (f i).subgroupOf H.

Equations
@[simp]
theorem AddSubgroup.quotientiInfAddSubgroupOfEmbedding_apply_mk {α : Type u_1} [AddGroup α] {ι : Type u_2} (f : ιAddSubgroup α) (H : AddSubgroup α) (g : H) (i : ι) :
@[simp]
theorem Subgroup.quotientiInfSubgroupOfEmbedding_apply_mk {α : Type u_1} [Group α] {ι : Type u_2} (f : ιSubgroup α) (H : Subgroup α) (g : H) (i : ι) :
theorem AddSubgroup.quotientiInfEmbedding.proof_1 {α : Type u_1} [AddGroup α] {ι : Type u_2} (f : ιAddSubgroup α) (i : ι) :
iInf f f i
theorem AddSubgroup.quotientiInfEmbedding.proof_2 {α : Type u_1} [AddGroup α] {ι : Type u_2} (f : ιAddSubgroup α) (q₁ : Quotient (QuotientAddGroup.leftRel (⨅ (i : ι), f i))) (q₂ : Quotient (QuotientAddGroup.leftRel (⨅ (i : ι), f i))) :
(fun (q : α ⨅ (i : ι), f i) (i : ι) => AddSubgroup.quotientMapOfLE q) q₁ = (fun (q : α ⨅ (i : ι), f i) (i : ι) => AddSubgroup.quotientMapOfLE q) q₂q₁ = q₂
def AddSubgroup.quotientiInfEmbedding {α : Type u_1} [AddGroup α] {ι : Type u_2} (f : ιAddSubgroup α) :
α ⨅ (i : ι), f i (i : ι) → α f i

The natural embedding α ⧸ (⨅ i, f i) ↪ Π i, α ⧸ f i.

Equations
@[simp]
theorem AddSubgroup.quotientiInfEmbedding_apply {α : Type u_1} [AddGroup α] {ι : Type u_2} (f : ιAddSubgroup α) (q : α ⨅ (i : ι), f i) (i : ι) :
@[simp]
theorem Subgroup.quotientiInfEmbedding_apply {α : Type u_1} [Group α] {ι : Type u_2} (f : ιSubgroup α) (q : α ⨅ (i : ι), f i) (i : ι) :
def Subgroup.quotientiInfEmbedding {α : Type u_1} [Group α] {ι : Type u_2} (f : ιSubgroup α) :
α ⨅ (i : ι), f i (i : ι) → α f i

The natural embedding α ⧸ (⨅ i, f i) ↪ Π i, α ⧸ f i.

Equations
@[simp]
theorem AddSubgroup.quotientiInfEmbedding_apply_mk {α : Type u_1} [AddGroup α] {ι : Type u_2} (f : ιAddSubgroup α) (g : α) (i : ι) :
@[simp]
theorem Subgroup.quotientiInfEmbedding_apply_mk {α : Type u_1} [Group α] {ι : Type u_2} (f : ιSubgroup α) (g : α) (i : ι) :
def AddMonoidHom.fiberEquivKer {α : Type u_1} [AddGroup α] {H : Type u_2} [AddGroup H] (f : α →+ H) (a : α) :
(f ⁻¹' {f a}) f.ker

An equivalence between any non-empty fiber of an AddMonoidHom and its kernel.

Equations
theorem AddMonoidHom.fiberEquivKer.proof_1 {α : Type u_1} [AddGroup α] {H : Type u_2} [AddGroup H] (f : α →+ H) (a : α) :
f ⁻¹' {f a} = a +ᵥ f.ker
def MonoidHom.fiberEquivKer {α : Type u_1} [Group α] {H : Type u_2} [Group H] (f : α →* H) (a : α) :
(f ⁻¹' {f a}) f.ker

An equivalence between any non-empty fiber of a MonoidHom and its kernel.

Equations
@[simp]
theorem AddMonoidHom.fiberEquivKer_apply {α : Type u_1} [AddGroup α] {H : Type u_2} [AddGroup H] (f : α →+ H) (a : α) (g : (f ⁻¹' {f a})) :
((f.fiberEquivKer a) g) = -a + g
@[simp]
theorem MonoidHom.fiberEquivKer_apply {α : Type u_1} [Group α] {H : Type u_2} [Group H] (f : α →* H) (a : α) (g : (f ⁻¹' {f a})) :
((f.fiberEquivKer a) g) = a⁻¹ * g
@[simp]
theorem AddMonoidHom.fiberEquivKer_symm_apply {α : Type u_1} [AddGroup α] {H : Type u_2} [AddGroup H] (f : α →+ H) (a : α) (g : f.ker) :
((f.fiberEquivKer a).symm g) = a + g
@[simp]
theorem MonoidHom.fiberEquivKer_symm_apply {α : Type u_1} [Group α] {H : Type u_2} [Group H] (f : α →* H) (a : α) (g : f.ker) :
((f.fiberEquivKer a).symm g) = a * g
noncomputable def AddMonoidHom.fiberEquivKerOfSurjective {α : Type u_1} [AddGroup α] {H : Type u_2} [AddGroup H] {f : α →+ H} (hf : Function.Surjective f) (h : H) :
(f ⁻¹' {h}) f.ker

An equivalence between any fiber of a surjective AddMonoidHom and its kernel.

Equations
theorem AddMonoidHom.fiberEquivKerOfSurjective.proof_1 {α : Type u_2} [AddGroup α] {H : Type u_1} [AddGroup H] {f : α →+ H} (hf : Function.Surjective f) (h : H) :
f .choose = h
noncomputable def MonoidHom.fiberEquivKerOfSurjective {α : Type u_1} [Group α] {H : Type u_2} [Group H] {f : α →* H} (hf : Function.Surjective f) (h : H) :
(f ⁻¹' {h}) f.ker

An equivalence between any fiber of a surjective MonoidHom and its kernel.

Equations
def AddMonoidHom.fiberEquiv {α : Type u_1} [AddGroup α] {H : Type u_2} [AddGroup H] (f : α →+ H) (a : α) (b : α) :
(f ⁻¹' {f a}) (f ⁻¹' {f b})

An equivalence between any two non-empty fibers of an AddMonoidHom.

Equations
  • f.fiberEquiv a b = (f.fiberEquivKer a).trans (f.fiberEquivKer b).symm
def MonoidHom.fiberEquiv {α : Type u_1} [Group α] {H : Type u_2} [Group H] (f : α →* H) (a : α) (b : α) :
(f ⁻¹' {f a}) (f ⁻¹' {f b})

An equivalence between any two non-empty fibers of a MonoidHom.

Equations
  • f.fiberEquiv a b = (f.fiberEquivKer a).trans (f.fiberEquivKer b).symm
@[simp]
theorem AddMonoidHom.fiberEquiv_apply {α : Type u_1} [AddGroup α] {H : Type u_2} [AddGroup H] (f : α →+ H) (a : α) (b : α) (g : (f ⁻¹' {f a})) :
((f.fiberEquiv a b) g) = b + (-a + g)
@[simp]
theorem MonoidHom.fiberEquiv_apply {α : Type u_1} [Group α] {H : Type u_2} [Group H] (f : α →* H) (a : α) (b : α) (g : (f ⁻¹' {f a})) :
((f.fiberEquiv a b) g) = b * (a⁻¹ * g)
@[simp]
theorem AddMonoidHom.fiberEquiv_symm_apply {α : Type u_1} [AddGroup α] {H : Type u_2} [AddGroup H] (f : α →+ H) (a : α) (b : α) (g : (f ⁻¹' {f b})) :
((f.fiberEquiv a b).symm g) = a + (-b + g)
@[simp]
theorem MonoidHom.fiberEquiv_symm_apply {α : Type u_1} [Group α] {H : Type u_2} [Group H] (f : α →* H) (a : α) (b : α) (g : (f ⁻¹' {f b})) :
((f.fiberEquiv a b).symm g) = a * (b⁻¹ * g)
noncomputable def AddMonoidHom.fiberEquivOfSurjective {α : Type u_1} [AddGroup α] {H : Type u_2} [AddGroup H] {f : α →+ H} (hf : Function.Surjective f) (h : H) (h' : H) :
(f ⁻¹' {h}) (f ⁻¹' {h'})

An equivalence between any two fibers of a surjective AddMonoidHom.

Equations
noncomputable def MonoidHom.fiberEquivOfSurjective {α : Type u_1} [Group α] {H : Type u_2} [Group H] {f : α →* H} (hf : Function.Surjective f) (h : H) (h' : H) :
(f ⁻¹' {h}) (f ⁻¹' {h'})

An equivalence between any two fibers of a surjective MonoidHom.

Equations
noncomputable def QuotientAddGroup.preimageMkEquivAddSubgroupProdSet {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (t : Set (α s)) :
(QuotientAddGroup.mk ⁻¹' t) s × t

If s is a subgroup of the additive group α, and t is a subset of α ⧸ s, then there is a (typically non-canonical) bijection between the preimage of t in α and the product s × t.

Equations
  • One or more equations did not get rendered due to their size.
theorem QuotientAddGroup.preimageMkEquivAddSubgroupProdSet.proof_3 {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (t : Set (α s)) (a : s × t) :
(Quotient.out' a.2 + a.1) t
theorem QuotientAddGroup.preimageMkEquivAddSubgroupProdSet.proof_2 {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (t : Set (α s)) (a : (QuotientAddGroup.mk ⁻¹' t)) :
a QuotientAddGroup.mk ⁻¹' t
theorem QuotientAddGroup.preimageMkEquivAddSubgroupProdSet.proof_1 {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (t : Set (α s)) (a : (QuotientAddGroup.mk ⁻¹' t)) :
-Quotient.out' a + a s
theorem QuotientAddGroup.preimageMkEquivAddSubgroupProdSet.proof_5 {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (t : Set (α s)) :
∀ (x : s × t), (fun (a : (QuotientAddGroup.mk ⁻¹' t)) => (-Quotient.out' a + a, , a, )) ((fun (a : s × t) => Quotient.out' a.2 + a.1, ) x) = x
theorem QuotientAddGroup.preimageMkEquivAddSubgroupProdSet.proof_4 {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (t : Set (α s)) :
∀ (x : (QuotientAddGroup.mk ⁻¹' t)), (fun (a : s × t) => Quotient.out' a.2 + a.1, ) ((fun (a : (QuotientAddGroup.mk ⁻¹' t)) => (-Quotient.out' a + a, , a, )) x) = x
noncomputable def QuotientGroup.preimageMkEquivSubgroupProdSet {α : Type u_1} [Group α] (s : Subgroup α) (t : Set (α s)) :
(QuotientGroup.mk ⁻¹' t) s × t

If s is a subgroup of the group α, and t is a subset of α ⧸ s, then there is a (typically non-canonical) bijection between the preimage of t in α and the product s × t.

Equations
  • One or more equations did not get rendered due to their size.