From 3882aaf68845e0859785eaeb100bf2841606cb11 Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Mon, 24 Oct 2022 07:29:28 +0000
Subject: [PATCH] feat(group_theory/index): criterion for subgroups of index
 two (#16629)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

* A subgroup has index two if and only if there exists `a` such that for all `b`, `b * a ∈ H` is equivalent to `b ∉ H`.
* For a subgroup of index two, `a * b ∈ H ↔ (a ∈ H ↔ b ∈ H)`.
---
 src/group_theory/coset.lean |  9 +++++----
 src/group_theory/index.lean | 34 ++++++++++++++++++++++++++++++++++
 src/logic/basic.lean        | 14 +++++++++-----
 3 files changed, 48 insertions(+), 9 deletions(-)

diff --git a/src/group_theory/coset.lean b/src/group_theory/coset.lean
index 639d5237d5555..115d06f715d9e 100644
--- a/src/group_theory/coset.lean
+++ b/src/group_theory/coset.lean
@@ -344,10 +344,11 @@ quotient.induction_on' x H
 lemma quotient_lift_on_coe {β} (f : α → β) (h) (x : α) :
   quotient.lift_on' (x : α ⧸ s) f h = f x := rfl
 
-@[to_additive]
-lemma forall_coe {C : α ⧸ s → Prop} :
-  (∀ x : α ⧸ s, C x) ↔ ∀ x : α, C x :=
-⟨λ hx x, hx _, quot.ind⟩
+@[to_additive] lemma forall_coe {C : α ⧸ s → Prop} : (∀ x : α ⧸ s, C x) ↔ ∀ x : α, C x :=
+mk_surjective.forall
+
+@[to_additive] lemma exists_coe {C : α ⧸ s → Prop} : (∃ x : α ⧸ s, C x) ↔ ∃ x : α, C x :=
+mk_surjective.exists
 
 @[to_additive]
 instance (s : subgroup α) : inhabited (α ⧸ s) :=
diff --git a/src/group_theory/index.lean b/src/group_theory/index.lean
index 76d67442cef44..e0a7622984973 100644
--- a/src/group_theory/index.lean
+++ b/src/group_theory/index.lean
@@ -132,6 +132,40 @@ begin
   exact relindex_mul_relindex (H ⊓ L) (K ⊓ L) L (inf_le_inf_right L hHK) inf_le_right,
 end
 
+/-- A subgroup has index two if and only if there exists `a` such that for all `b`, exactly one
+of `b * a` and `b` belong to `H`. -/
+@[to_additive "/-- An additive subgroup has index two if and only if there exists `a` such that for
+all `b`, exactly one of `b + a` and `b` belong to `H`. -/"]
+lemma index_eq_two_iff : H.index = 2 ↔ ∃ a, ∀ b, xor (b * a ∈ H) (b ∈ H) :=
+begin
+  simp only [index, nat.card_eq_two_iff' ((1 : G) : G ⧸ H), exists_unique, inv_mem_iff,
+    quotient_group.exists_coe, quotient_group.forall_coe, ne.def, quotient_group.eq, mul_one,
+    xor_iff_iff_not],
+  refine exists_congr (λ a, ⟨λ ha b, ⟨λ hba hb, _, λ hb, _⟩, λ ha, ⟨_, λ b hb, _⟩⟩),
+  { exact ha.1 ((mul_mem_cancel_left hb).1 hba) },
+  { exact inv_inv b ▸ ha.2 _ (mt inv_mem_iff.1 hb) },
+  { rw [← inv_mem_iff, ← ha, inv_mul_self], exact one_mem _ },
+  { rwa [ha, inv_mem_iff] }
+end
+
+@[to_additive] lemma mul_mem_iff_of_index_two (h : H.index = 2) {a b : G} :
+  a * b ∈ H ↔ (a ∈ H ↔ b ∈ H) :=
+begin
+  by_cases ha : a ∈ H, { simp only [ha, true_iff, mul_mem_cancel_left ha] },
+  by_cases hb : b ∈ H, { simp only [hb, iff_true, mul_mem_cancel_right hb] },
+  simp only [ha, hb, iff_self, iff_true],
+  rcases index_eq_two_iff.1 h with ⟨c, hc⟩,
+  refine (hc _).or.resolve_left _,
+  rwa [mul_assoc, mul_mem_cancel_right ((hc _).or.resolve_right hb)]
+end
+
+@[to_additive] lemma mul_self_mem_of_index_two (h : H.index = 2) (a : G) : a * a ∈ H :=
+by rw [mul_mem_iff_of_index_two h]
+
+@[to_additive two_smul_mem_of_index_two]
+lemma sq_mem_of_index_two (h : H.index = 2) (a : G) : a ^ 2 ∈ H :=
+(pow_two a).symm ▸ mul_self_mem_of_index_two h a
+
 variables (H K)
 
 @[simp, to_additive] lemma index_top : (⊤ : subgroup G).index = 1 :=
diff --git a/src/logic/basic.lean b/src/logic/basic.lean
index 0107c651c530a..3314867fd2287 100644
--- a/src/logic/basic.lean
+++ b/src/logic/basic.lean
@@ -426,11 +426,15 @@ lemma iff.not_right (h : ¬ a ↔ b) : a ↔ ¬ b := not_not.symm.trans h.not
 
 @[simp] theorem xor_false : xor false = id := funext $ λ a, by simp [xor]
 
-theorem xor_comm (a b) : xor a b = xor b a := by simp [xor, and_comm, or_comm]
+theorem xor_comm (a b) : xor a b ↔ xor b a := or_comm _ _
 
-instance : is_commutative Prop xor := ⟨xor_comm⟩
+instance : is_commutative Prop xor := ⟨λ a b, propext $ xor_comm a b⟩
 
 @[simp] theorem xor_self (a : Prop) : xor a a = false := by simp [xor]
+@[simp] theorem xor_not_left : xor (¬a) b ↔ (a ↔ b) := by by_cases a; simp *
+@[simp] theorem xor_not_right : xor a (¬b) ↔ (a ↔ b) := by by_cases a; simp *
+theorem xor_not_not : xor (¬a) (¬b) ↔ xor a b := by simp [xor, or_comm, and_comm]
+protected theorem xor.or (h : xor a b) : a ∨ b := h.imp and.left and.left
 
 /-! ### Declarations about `and` -/
 
@@ -810,9 +814,9 @@ theorem and_iff_not_or_not : a ∧ b ↔ ¬ (¬ a ∨ ¬ b) := decidable.and_iff
 @[simp] theorem not_xor (P Q : Prop) : ¬ xor P Q ↔ (P ↔ Q) :=
 by simp only [not_and, xor, not_or_distrib, not_not, ← iff_iff_implies_and_implies]
 
-theorem xor_iff_not_iff (P Q : Prop) : xor P Q ↔ ¬ (P ↔ Q) :=
-by rw [iff_not_comm, not_xor]
-
+theorem xor_iff_not_iff (P Q : Prop) : xor P Q ↔ ¬ (P ↔ Q) := (not_xor P Q).not_right
+theorem xor_iff_iff_not : xor a b ↔ (a ↔ ¬b) := by simp only [← @xor_not_right a, not_not]
+theorem xor_iff_not_iff' : xor a b ↔ (¬a ↔ b) := by simp only [← @xor_not_left _ b, not_not]
 
 end propositional