text:
/-
Copyright (c) 2020 Markus Himmel. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Markus Himmel
-/
import ring_theory.ideal.operations

/-!
# Ideals in product rings

For commutative rings `R` and `S` and ideals `I ≤ R`, `J ≤ S`, we define `ideal.prod I J` as the
product `I × J`, viewed as an ideal of `R × S`. In `ideal_prod_eq` we show that every ideal of
`R × S` is of this form.  Furthermore, we show that every prime ideal of `R × S` is of the form
`p × S` or `R × p`, where `p` is a prime ideal.
-/

universes u v
variables {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (I I' : ideal R) (J J' : ideal S)

namespace ideal

/-- `I × J` as an ideal of `R × S`. -/
def prod : ideal (R × S) :=
{ carrier := { x | x.fst ∈ I ∧ x.snd ∈ J },
  zero_mem' := by simp,
  add_mem' :=
  begin
    rintros ⟨a₁, a₂⟩ ⟨b₁, b₂⟩ ⟨ha₁, ha₂⟩ ⟨hb₁, hb₂⟩,
    exact ⟨I.add_mem ha₁ hb₁, J.add_mem ha₂ hb₂⟩
  end,
  smul_mem' :=
  begin
    rintros ⟨a₁, a₂⟩ ⟨b₁, b₂⟩ ⟨hb₁, hb₂⟩,
    exact ⟨I.mul_mem_left _ hb₁, J.mul_mem_left _ hb₂⟩,
  end }

@[simp] lemma mem_prod {r : R} {s : S} : (⟨r, s⟩ : R × S) ∈ prod I J ↔ r ∈ I ∧ s ∈ J := iff.rfl
@[simp] lemma prod_top_top : prod (⊤ : ideal R) (⊤ : ideal S) = ⊤ := ideal.ext $ by simp

/-- Every ideal of the product ring is of the form `I × J`, where `I` and `J` can be explicitly
    given as the image under the projection maps. -/
theorem ideal_prod_eq (I : ideal (R × S)) :
  I = ideal.prod (map (ring_hom.fst R S) I) (map (ring_hom.snd R S) I) :=
begin
  apply ideal.ext,
  rintro ⟨r, s⟩,
  rw [mem_prod, mem_map_iff_of_surjective (ring_hom.fst R S) prod.fst_surjective,
    mem_map_iff_of_surjective (ring_hom.snd R S) prod.snd_surjective],
  refine ⟨λ h, ⟨⟨_, ⟨h, rfl⟩⟩, ⟨_, ⟨h, rfl⟩⟩⟩, _⟩,
  rintro ⟨⟨⟨r, s'⟩, ⟨h₁, rfl⟩⟩, ⟨⟨r', s⟩, ⟨h₂, rfl⟩⟩⟩,
  simpa using I.add_mem (I.mul_mem_right (1, 0) h₁) (I.mul_mem_right (0, 1) h₂)
end

@[simp] lemma map_fst_prod (I : ideal R) (J : ideal S) : map (ring_hom.fst R S) (prod I J) = I :=
begin
  ext,
  rw mem_map_iff_of_surjective (ring_hom.fst R S) prod.fst_surjective,
  exact ⟨by { rintro ⟨x, ⟨h, rfl⟩⟩, exact h.1 }, λ h, ⟨⟨x, 0⟩, ⟨⟨h, ideal.zero_mem _⟩, rfl⟩⟩⟩
end

@[simp] lemma map_snd_prod (I : ideal R) (J : ideal S) : map (ring_hom.snd R S) (prod I J) = J :=
begin
  ext,
  rw mem_map_iff_of_surjective (ring_hom.snd R S) prod.snd_surjective,
  exact ⟨by { rintro ⟨x, ⟨h, rfl⟩⟩, exact h.2 }, λ h, ⟨⟨0, x⟩, ⟨⟨ideal.zero_mem _, h⟩, rfl⟩⟩⟩
end

@[simp] lemma map_prod_comm_prod :
  map ↑(ring_equiv.prod_comm : R × S ≃+* S × R) (prod I J) = prod J I :=
begin
  refine trans (ideal_prod_eq _) _,
  simp [map_map],
end

/-- Ideals of `R × S` are in one-to-one correspondence with pairs of ideals of `R` and ideals of
    `S`. -/
def ideal_prod_equiv : ideal (R × S) ≃ ideal R × ideal S :=
{ to_fun := λ I, ⟨map (ring_hom.fst R S) I, map (ring_hom.snd R S) I⟩,
  inv_fun := λ I, prod I.1 I.2,
  left_inv := λ I, (ideal_prod_eq I).symm,
  right_inv := λ ⟨I, J⟩, by simp }

@[simp] lemma ideal_prod_equiv_symm_apply (I : ideal R) (J : ideal S) :
  ideal_prod_equiv.symm ⟨I, J⟩ = prod I J := rfl

lemma prod.ext_iff {I I' : ideal R} {J J' : ideal S} : prod I J = prod I' J' ↔ I = I' ∧ J = J' :=
by simp only [←ideal_prod_equiv_symm_apply, ideal_prod_equiv.symm.injective.eq_iff, prod.mk.inj_iff]

lemma is_prime_of_is_prime_prod_top {I : ideal R} (h : (ideal.prod I (⊤ : ideal S)).is_prime) :
  I.is_prime :=
begin
  split,
  { unfreezingI { contrapose! h },
    simp [is_prime_iff, h] },
  { intros x y hxy,
    have : (⟨x, 1⟩ : R × S) * ⟨y, 1⟩ ∈ prod I ⊤,
    { rw [prod.mk_mul_mk, mul_one, mem_prod],
      exact ⟨hxy, trivial⟩ },
    simpa using h.mem_or_mem this }
end

lemma is_prime_of_is_prime_prod_top' {I : ideal S} (h : (ideal.prod (⊤ : ideal R) I).is_prime) :
  I.is_prime :=
begin
  apply @is_prime_of_is_prime_prod_top _ R,
  rw ←map_prod_comm_prod,
  exact map_is_prime_of_equiv _
end

lemma is_prime_ideal_prod_top' {I : ideal S} [h : I.is_prime] : (prod (⊤ : ideal R) I).is_prime :=
begin
  rw ←map_prod_comm_prod,
  apply map_is_prime_of_equiv _,
  exact is_prime_ideal_prod_top,
end

lemma ideal_prod_prime_aux {I : ideal R} {J : ideal S} : (ideal.prod I J).is_prime →
  I = ⊤ ∨ J = ⊤ :=
begin
  contrapose!,
  simp only [ne_top_iff_one, is_prime_iff, not_and, not_forall, not_or_distrib],
  exact λ ⟨hI, hJ⟩ hIJ, ⟨⟨0, 1⟩, ⟨1, 0⟩, by simp, by simp [hJ], by simp [hI]⟩
end

/-- Classification of prime ideals in product rings: the prime ideals of `R × S` are precisely the
    ideals of the form `p × S` or `R × p`, where `p` is a prime ideal of `R` or `S`. -/
theorem ideal_prod_prime (I : ideal (R × S)) : I.is_prime ↔
  ((∃ p : ideal R, p.is_prime ∧ I = ideal.prod p ⊤) ∨
   (∃ p : ideal S, p.is_prime ∧ I = ideal.prod ⊤ p)) :=
begin
  split,
  { rw ideal_prod_eq I,
    introsI hI,
    rcases ideal_prod_prime_aux hI with (h|h),
    { right,
      rw h at hI ⊢,
      exact ⟨_, ⟨is_prime_of_is_prime_prod_top' hI, rfl⟩⟩ },
    { left,
      rw h at hI ⊢,
      exact ⟨_, ⟨is_prime_of_is_prime_prod_top hI, rfl⟩⟩ } },
  { rintro (⟨p, ⟨h, rfl⟩⟩|⟨p, ⟨h, rfl⟩⟩),
    { exactI is_prime_ideal_prod_top },
    { exactI is_prime_ideal_prod_top' } }
end

@[simp] private def prime_ideals_equiv_impl :
  { I : ideal R // I.is_prime } ⊕ { J : ideal S // J.is_prime } →
    { K : ideal (R × S) // K.is_prime }
| (sum.inl ⟨I, hI⟩) := ⟨ideal.prod I ⊤, by exactI is_prime_ideal_prod_top⟩
| (sum.inr ⟨J, hJ⟩) := ⟨ideal.prod ⊤ J, by exactI is_prime_ideal_prod_top'⟩

section
variables (R S)

/-- The prime ideals of `R × S` are in bijection with the disjoint union of the prime ideals
    of `R` and the prime ideals of `S`. -/
noncomputable def prime_ideals_equiv : { K : ideal (R × S) // K.is_prime } ≃
  { I : ideal R // I.is_prime } ⊕ { J : ideal S // J.is_prime } :=
equiv.symm $ equiv.of_bijective prime_ideals_equiv_impl
begin
  split,
  { rintros (⟨I, hI⟩|⟨J, hJ⟩) (⟨I',  hI'⟩|⟨J', hJ'⟩) h;
    simp [prod.ext_iff] at h,
    { simp [h] },
    { exact false.elim (hI.ne_top h.1) },
    { exact false.elim (hJ.ne_top h.2) },
    { simp [h] } },
  { rintro ⟨I, hI⟩,
    rcases (ideal_prod_prime I).1 hI with (⟨p, ⟨hp, rfl⟩⟩|⟨p, ⟨hp, rfl⟩⟩),
    { exact ⟨sum.inl ⟨p, hp⟩, rfl⟩ },
    { exact ⟨sum.inr ⟨p, hp⟩, rfl⟩ } }
end

end

@[simp] lemma prime_ideals_equiv_symm_inl (h : I.is_prime) :
  (prime_ideals_equiv R S).symm (sum.inl ⟨I, h⟩) = ⟨prod I ⊤, by exactI is_prime_ideal_prod_top⟩ :=
rfl
@[simp] lemma prime_ideals_equiv_symm_inr (h : J.is_prime) :
  (prime_ideals_equiv R S).symm (sum.inr ⟨J, h⟩) = ⟨prod ⊤ J, by exactI is_prime_ideal_prod_top'⟩ :=
rfl

end ideal

author: JLimperg


text:
import algebra.group algebra.group_power

universe u
variables {A G: Type u}

-- Theorems & lemmas from the body text of chapter 2.3

-- Lemma 2.3.1: If G is a group, then
-- a. The identity element of G is unique.
-- b. Every a ∈ G has a unique inverse in G.
-- c. For every a ∈ G, (a⁻¹)⁻¹ = a.
-- d. For all a, b ∈ G, (a * b)⁻¹ = b⁻¹ * a ⁻¹

lemma L2_3_1a (e f: G) [group G]:
  (∀ a: G, a = a * e) ∧
  (∀ a: G, a = e * a) ∧
  (∀ a: G, a = a * f) ∧
  (∀ a: G, a = f * a) → e = f :=
λ ⟨h1, ⟨h2, ⟨h3, h4⟩⟩⟩, eq.trans (h3 e) (h2 f).symm

-- now justified: use of group.one G to extract unique identity of G,
-- and the notation 1 for group.one G.

lemma L2_3_1b (a g h: G) [group G]:
  a * g = 1 ∧ g * a = 1 ∧
  a * h = 1 ∧ h * a = 1 → g = h :=
λ ⟨h1, ⟨h2, ⟨h3, h4⟩⟩⟩, calc
  g = g * 1       : (mul_one g).symm
... = g * (a * h) : h3 ▸ ⟨g * (a * h)⟩
... = (g * a) * h : (mul_assoc g a h).symm
... = 1 * h       : h2 ▸ ⟨(g * a) * h⟩
... = h           : (one_mul h)

-- now justified: use of group.inv and notation a⁻¹ for the inverse of a.

lemma L2_3_1b₁ (a b c: G) [group G]:
  a * b = a * c → b = c := λ h, calc
  b   = 1 * b       : (one_mul b).symm
  ... = a⁻¹ * a * b : by rw inv_mul_self
  ... = a⁻¹ * a * c : by rw [mul_assoc, h, ←mul_assoc]
  ... = 1 * c       : by rw inv_mul_self
  ... = c           : one_mul c

lemma L2_3_1c (a: G) [group G]: (a⁻¹)⁻¹ = a :=
eq.symm $ calc a
    = 1 * a               : (one_mul _).symm
... = (a⁻¹)⁻¹ * a⁻¹ * a   : by rw ←inv_mul_self
... = (a⁻¹)⁻¹ * (a⁻¹ * a) : by rw mul_assoc
... = (a⁻¹)⁻¹ * 1         : by rw inv_mul_self
... = (a⁻¹)⁻¹             : mul_one _

-- now justified: use of group.mul_inv_rev

lemma L2_3_1d (a b : G) [group G] : (a * b)⁻¹ = b⁻¹ * a⁻¹ :=
inv_eq_of_mul_eq_one $ calc a * b * (b⁻¹ * a⁻¹)
    = a * (b * (b⁻¹ * a⁻¹))   : mul_assoc _ _ _
... = a * (b * b⁻¹ * a ⁻¹)    : by rw ←mul_assoc b b⁻¹ a⁻¹
... = a * (1 * a⁻¹)           : by rw mul_right_inv
... = a * a⁻¹                 : by rw one_mul
... = 1                       : by rw mul_right_inv

-- left cancellation
lemma L2_3_2₁ (a u w: G) [group G]:
  a * u = a * w → u = w :=
λ h, calc u
    = 1 * u         : (one_mul _).symm
... = a⁻¹ * a * u   : by rw ←inv_mul_self
... = a⁻¹ * (a * u) : mul_assoc _ _ _
... = a⁻¹ * (a * w) : by rw h
... = a⁻¹ * a * w   : (mul_assoc _ _ _).symm
... = 1 * w         : by rw inv_mul_self
... = w             : by rw one_mul

-- right cancellation: similarly
lemma L2_3_2₂ (a u w: G) [group G]:
  u * a = w * a → u = w :=
λ h, calc u
    = u * (a * a⁻¹) : (mul_right_inv a).symm ▸ (mul_one u).symm
... = w * (a * a⁻¹) : by rw [ ←mul_assoc, h, mul_assoc ]
... = w             : by rw [ mul_right_inv, mul_one ]

author: group-study-group

repo: herstein


text:
import data.real.basic
import game.Completeness.level04

noncomputable theory
open_locale classical

/-
# Chapter 6 : Completeness

## Level 6

Prove that a nonempty and upper bounded
set has a unique least upper bound.

-/

definition has_lub (S : set ℝ) := ∃ x, is_lub S x

definition is_upper_bound (S : set ℝ) (x : ℝ) := ∀ s ∈ S, s ≤ x

definition is_lub_plzwork (S : set ℝ) (x : ℝ) := is_upper_bound S x ∧
∀ y : ℝ, is_upper_bound S y → x ≤ y

/-
lemma unique_LUB (A : set ℝ) (x y : ℝ) (H : has_lub A) (hx : is_lub A x) (hy : is_lub A y) : x = y :=
begin
  cases hx with d hd,
  cases hy with f hf,

  specialize hd y,
  specialize hf x,
  specialize hf d,
  specialize hd f,
  linarith,
end
-/

theorem nonempty_and_bounded_has_unique_LUB (x y : ℝ) (S : set ℝ) (H : has_lub S) (hx : is_lub_plzwork S x) (hy : is_lub_plzwork S y) :
 (S ≠ ∅) ∧ (has_lub S) → x = y :=
begin
  intro h,
  cases h with t ht,
  cases ht with t ht,

  cases hx with d hd,
  cases hy with f hf,

  --specialize hd y,
  specialize hf x,
  specialize hd y,

  specialize hf d,
  specialize hd f,
  linarith,
end

author: DavidTalone

repo: Real-Number-Game


text:
/-
Copyright (c) 2018 Chris Hughes. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Chris Hughes, Thomas Browning

! This file was ported from Lean 3 source module group_theory.sylow
! leanprover-community/mathlib commit c55911f6166b348e1c72b08c8664e3af5f1ce334
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathbin.Data.Nat.Factorization.Basic
import Mathbin.Data.SetLike.Fintype
import Mathbin.GroupTheory.GroupAction.ConjAct
import Mathbin.GroupTheory.PGroup
import Mathbin.GroupTheory.NoncommPiCoprod
import Mathbin.Order.Atoms.Finite

/-!
# Sylow theorems

The Sylow theorems are the following results for every finite group `G` and every prime number `p`.

* There exists a Sylow `p`-subgroup of `G`.
* All Sylow `p`-subgroups of `G` are conjugate to each other.
* Let `nₚ` be the number of Sylow `p`-subgroups of `G`, then `nₚ` divides the index of the Sylow
  `p`-subgroup, `nₚ ≡ 1 [MOD p]`, and `nₚ` is equal to the index of the normalizer of the Sylow
  `p`-subgroup in `G`.

## Main definitions

* `sylow p G` : The type of Sylow `p`-subgroups of `G`.

## Main statements

* `exists_subgroup_card_pow_prime`: A generalization of Sylow's first theorem:
  For every prime power `pⁿ` dividing the cardinality of `G`,
  there exists a subgroup of `G` of order `pⁿ`.
* `is_p_group.exists_le_sylow`: A generalization of Sylow's first theorem:
  Every `p`-subgroup is contained in a Sylow `p`-subgroup.
* `sylow.card_eq_multiplicity`: The cardinality of a Sylow group is `p ^ n`
 where `n` is the multiplicity of `p` in the group order.
* `sylow_conjugate`: A generalization of Sylow's second theorem:
  If the number of Sylow `p`-subgroups is finite, then all Sylow `p`-subgroups are conjugate.
* `card_sylow_modeq_one`: A generalization of Sylow's third theorem:
  If the number of Sylow `p`-subgroups is finite, then it is congruent to `1` modulo `p`.
-/

open Fintype MulAction Subgroup

section InfiniteSylow

variable (p : ℕ) (G : Type _) [Group G]

/-- A Sylow `p`-subgroup is a maximal `p`-subgroup. -/
structure Sylow extends Subgroup G where
  is_p_group' : IsPGroup p to_subgroup
  is_maximal' : ∀ {Q : Subgroup G}, IsPGroup p Q → to_subgroup ≤ Q → Q = to_subgroup
#align sylow Sylow

variable {p} {G}

namespace Sylow

instance : Coe (Sylow p G) (Subgroup G) :=
  ⟨Sylow.toSubgroup⟩

@[simp]
theorem toSubgroup_eq_coe {P : Sylow p G} : P.toSubgroup = ↑P :=
  rfl
#align sylow.to_subgroup_eq_coe Sylow.toSubgroup_eq_coe

@[ext]
theorem ext {P Q : Sylow p G} (h : (P : Subgroup G) = Q) : P = Q := by cases P <;> cases Q <;> congr
#align sylow.ext Sylow.ext

theorem ext_iff {P Q : Sylow p G} : P = Q ↔ (P : Subgroup G) = Q :=
  ⟨congr_arg coe, ext⟩
#align sylow.ext_iff Sylow.ext_iff

instance : SetLike (Sylow p G) G where
  coe := coe
  coe_injective' P Q h := ext (SetLike.coe_injective h)

instance : SubgroupClass (Sylow p G) G
    where
  mul_mem s _ _ := s.mul_mem'
  one_mem s := s.one_mem'
  inv_mem s _ := s.inv_mem'

variable (P : Sylow p G)

/-- The action by a Sylow subgroup is the action by the underlying group. -/
instance mulActionLeft {α : Type _} [MulAction G α] : MulAction P α :=
  Subgroup.mulAction ↑P
#align sylow.mul_action_left Sylow.mulActionLeft

variable {K : Type _} [Group K] (ϕ : K →* G) {N : Subgroup G}

/-- The preimage of a Sylow subgroup under a p-group-kernel homomorphism is a Sylow subgroup. -/
def comapOfKerIsPGroup (hϕ : IsPGroup p ϕ.ker) (h : ↑P ≤ ϕ.range) : Sylow p K :=
  { P.1.comap ϕ with
    is_p_group' := P.2.comap_of_ker_isPGroup ϕ hϕ
    is_maximal' := fun Q hQ hle =>
      by
      rw [← P.3 (hQ.map ϕ) (le_trans (ge_of_eq (map_comap_eq_self h)) (map_mono hle))]
      exact (comap_map_eq_self ((P.1.ker_le_comap ϕ).trans hle)).symm }
#align sylow.comap_of_ker_is_p_group Sylow.comapOfKerIsPGroup

@[simp]
theorem coe_comapOfKerIsPGroup (hϕ : IsPGroup p ϕ.ker) (h : ↑P ≤ ϕ.range) :
    ↑(P.comap_of_ker_isPGroup ϕ hϕ h) = Subgroup.comap ϕ ↑P :=
  rfl
#align sylow.coe_comap_of_ker_is_p_group Sylow.coe_comapOfKerIsPGroup

/-- The preimage of a Sylow subgroup under an injective homomorphism is a Sylow subgroup. -/
def comapOfInjective (hϕ : Function.Injective ϕ) (h : ↑P ≤ ϕ.range) : Sylow p K :=
  P.comap_of_ker_isPGroup ϕ (IsPGroup.ker_isPGroup_of_injective hϕ) h
#align sylow.comap_of_injective Sylow.comapOfInjective

@[simp]
theorem coe_comapOfInjective (hϕ : Function.Injective ϕ) (h : ↑P ≤ ϕ.range) :
    ↑(P.comap_of_injective ϕ hϕ h) = Subgroup.comap ϕ ↑P :=
  rfl
#align sylow.coe_comap_of_injective Sylow.coe_comapOfInjective

/-- A sylow subgroup of G is also a sylow subgroup of a subgroup of G. -/
protected def subtype (h : ↑P ≤ N) : Sylow p N :=
  P.comap_of_injective N.Subtype Subtype.coe_injective (by rwa [subtype_range])
#align sylow.subtype Sylow.subtype

@[simp]
theorem coe_subtype (h : ↑P ≤ N) : ↑(P.Subtype h) = subgroupOf (↑P) N :=
  rfl
#align sylow.coe_subtype Sylow.coe_subtype

theorem subtype_injective {P Q : Sylow p G} {hP : ↑P ≤ N} {hQ : ↑Q ≤ N}
    (h : P.Subtype hP = Q.Subtype hQ) : P = Q :=
  by
  rw [SetLike.ext_iff] at h⊢
  exact fun g => ⟨fun hg => (h ⟨g, hP hg⟩).mp hg, fun hg => (h ⟨g, hQ hg⟩).mpr hg⟩
#align sylow.subtype_injective Sylow.subtype_injective

end Sylow

/-- A generalization of **Sylow's first theorem**.
  Every `p`-subgroup is contained in a Sylow `p`-subgroup. -/
theorem IsPGroup.exists_le_sylow {P : Subgroup G} (hP : IsPGroup p P) : ∃ Q : Sylow p G, P ≤ Q :=
  Exists.elim
    (zorn_nonempty_partialOrder₀ { Q : Subgroup G | IsPGroup p Q }
      (fun c hc1 hc2 Q hQ =>
        ⟨{  carrier := ⋃ R : c, R
            one_mem' := ⟨Q, ⟨⟨Q, hQ⟩, rfl⟩, Q.one_mem⟩
            inv_mem' := fun g ⟨_, ⟨R, rfl⟩, hg⟩ => ⟨R, ⟨R, rfl⟩, R.1.inv_mem hg⟩
            mul_mem' := fun g h ⟨_, ⟨R, rfl⟩, hg⟩ ⟨_, ⟨S, rfl⟩, hh⟩ =>
              (hc2.Total R.2 S.2).elim (fun T => ⟨S, ⟨S, rfl⟩, S.1.mul_mem (T hg) hh⟩) fun T =>
                ⟨R, ⟨R, rfl⟩, R.1.mul_mem hg (T hh)⟩ },
          fun ⟨g, _, ⟨S, rfl⟩, hg⟩ =>
          by
          refine' Exists.imp (fun k hk => _) (hc1 S.2 ⟨g, hg⟩)
          rwa [Subtype.ext_iff, coe_pow] at hk⊢, fun M hM g hg => ⟨M, ⟨⟨M, hM⟩, rfl⟩, hg⟩⟩)
      P hP)
    fun Q ⟨hQ1, hQ2, hQ3⟩ => ⟨⟨Q, hQ1, hQ3⟩, hQ2⟩
#align is_p_group.exists_le_sylow IsPGroup.exists_le_sylow

instance Sylow.nonempty : Nonempty (Sylow p G) :=
  nonempty_of_exists IsPGroup.of_bot.exists_le_sylow
#align sylow.nonempty Sylow.nonempty

noncomputable instance Sylow.inhabited : Inhabited (Sylow p G) :=
  Classical.inhabited_of_nonempty Sylow.nonempty
#align sylow.inhabited Sylow.inhabited

theorem Sylow.exists_comap_eq_of_ker_isPGroup {H : Type _} [Group H] (P : Sylow p H) {f : H →* G}
    (hf : IsPGroup p f.ker) : ∃ Q : Sylow p G, (Q : Subgroup G).comap f = P :=
  Exists.imp (fun Q hQ => P.3 (Q.2.comap_of_ker_isPGroup f hf) (map_le_iff_le_comap.mp hQ))
    (P.2.map f).exists_le_sylow
#align sylow.exists_comap_eq_of_ker_is_p_group Sylow.exists_comap_eq_of_ker_isPGroup

theorem Sylow.exists_comap_eq_of_injective {H : Type _} [Group H] (P : Sylow p H) {f : H →* G}
    (hf : Function.Injective f) : ∃ Q : Sylow p G, (Q : Subgroup G).comap f = P :=
  P.exists_comap_eq_of_ker_isPGroup (IsPGroup.ker_isPGroup_of_injective hf)
#align sylow.exists_comap_eq_of_injective Sylow.exists_comap_eq_of_injective

theorem Sylow.exists_comap_subtype_eq {H : Subgroup G} (P : Sylow p H) :
    ∃ Q : Sylow p G, (Q : Subgroup G).comap H.Subtype = P :=
  P.exists_comap_eq_of_injective Subtype.coe_injective
#align sylow.exists_comap_subtype_eq Sylow.exists_comap_subtype_eq

/-- If the kernel of `f : H →* G` is a `p`-group,
  then `fintype (sylow p G)` implies `fintype (sylow p H)`. -/
noncomputable def Sylow.fintypeOfKerIsPGroup {H : Type _} [Group H] {f : H →* G}
    (hf : IsPGroup p f.ker) [Fintype (Sylow p G)] : Fintype (Sylow p H) :=
  let h_exists := fun P : Sylow p H => P.exists_comap_eq_of_ker_isPGroup hf
  let g : Sylow p H → Sylow p G := fun P => Classical.choose (h_exists P)
  let hg : ∀ P : Sylow p H, (g P).1.comap f = P := fun P => Classical.choose_spec (h_exists P)
  Fintype.ofInjective g fun P Q h => Sylow.ext (by simp only [← hg, h])
#align sylow.fintype_of_ker_is_p_group Sylow.fintypeOfKerIsPGroup

/-- If `f : H →* G` is injective, then `fintype (sylow p G)` implies `fintype (sylow p H)`. -/
noncomputable def Sylow.fintypeOfInjective {H : Type _} [Group H] {f : H →* G}
    (hf : Function.Injective f) [Fintype (Sylow p G)] : Fintype (Sylow p H) :=
  Sylow.fintypeOfKerIsPGroup (IsPGroup.ker_isPGroup_of_injective hf)
#align sylow.fintype_of_injective Sylow.fintypeOfInjective

/-- If `H` is a subgroup of `G`, then `fintype (sylow p G)` implies `fintype (sylow p H)`. -/
noncomputable instance (H : Subgroup G) [Fintype (Sylow p G)] : Fintype (Sylow p H) :=
  Sylow.fintypeOfInjective H.subtype_injective

/-- If `H` is a subgroup of `G`, then `finite (sylow p G)` implies `finite (sylow p H)`. -/
instance (H : Subgroup G) [Finite (Sylow p G)] : Finite (Sylow p H) :=
  by
  cases nonempty_fintype (Sylow p G)
  infer_instance

open Pointwise

/-- `subgroup.pointwise_mul_action` preserves Sylow subgroups. -/
instance Sylow.pointwiseMulAction {α : Type _} [Group α] [MulDistribMulAction α G] :
    MulAction α (Sylow p G)
    where
  smul g P :=
    ⟨g • P, P.2.map _, fun Q hQ hS =>
      inv_smul_eq_iff.mp
        (P.3 (hQ.map _) fun s hs =>
          (congr_arg (· ∈ g⁻¹ • Q) (inv_smul_smul g s)).mp
            (smul_mem_pointwise_smul (g • s) g⁻¹ Q (hS (smul_mem_pointwise_smul s g P hs))))⟩
  one_smul P := Sylow.ext (one_smul α P)
  mul_smul g h P := Sylow.ext (mul_smul g h P)
#align sylow.pointwise_mul_action Sylow.pointwiseMulAction

theorem Sylow.pointwise_smul_def {α : Type _} [Group α] [MulDistribMulAction α G] {g : α}
    {P : Sylow p G} : ↑(g • P) = g • (P : Subgroup G) :=
  rfl
#align sylow.pointwise_smul_def Sylow.pointwise_smul_def

instance Sylow.mulAction : MulAction G (Sylow p G) :=
  compHom _ MulAut.conj
#align sylow.mul_action Sylow.mulAction

theorem Sylow.smul_def {g : G} {P : Sylow p G} : g • P = MulAut.conj g • P :=
  rfl
#align sylow.smul_def Sylow.smul_def

theorem Sylow.coe_subgroup_smul {g : G} {P : Sylow p G} :
    ↑(g • P) = MulAut.conj g • (P : Subgroup G) :=
  rfl
#align sylow.coe_subgroup_smul Sylow.coe_subgroup_smul

theorem Sylow.coe_smul {g : G} {P : Sylow p G} : ↑(g • P) = MulAut.conj g • (P : Set G) :=
  rfl
#align sylow.coe_smul Sylow.coe_smul

theorem Sylow.smul_le {P : Sylow p G} {H : Subgroup G} (hP : ↑P ≤ H) (h : H) : ↑(h • P) ≤ H :=
  Subgroup.conj_smul_le_of_le hP h
#align sylow.smul_le Sylow.smul_le

theorem Sylow.smul_subtype {P : Sylow p G} {H : Subgroup G} (hP : ↑P ≤ H) (h : H) :
    h • P.Subtype hP = (h • P).Subtype (Sylow.smul_le hP h) :=
  Sylow.ext (Subgroup.conj_smul_subgroupOf hP h)
#align sylow.smul_subtype Sylow.smul_subtype

theorem Sylow.smul_eq_iff_mem_normalizer {g : G} {P : Sylow p G} :
    g • P = P ↔ g ∈ (P : Subgroup G).normalizer :=
  by
  rw [eq_comm, SetLike.ext_iff, ← inv_mem_iff, mem_normalizer_iff, inv_inv]
  exact
    forall_congr' fun h =>
      iff_congr Iff.rfl
        ⟨fun ⟨a, b, c⟩ =>
          (congr_arg _ c).mp
            ((congr_arg (· ∈ P.1) (MulAut.inv_apply_self G (MulAut.conj g) a)).mpr b),
          fun hh => ⟨(MulAut.conj g)⁻¹ h, hh, MulAut.apply_inv_self G (MulAut.conj g) h⟩⟩
#align sylow.smul_eq_iff_mem_normalizer Sylow.smul_eq_iff_mem_normalizer

theorem Sylow.smul_eq_of_normal {g : G} {P : Sylow p G} [h : (P : Subgroup G).Normal] : g • P = P :=
  by simp only [Sylow.smul_eq_iff_mem_normalizer, normalizer_eq_top.mpr h, mem_top]
#align sylow.smul_eq_of_normal Sylow.smul_eq_of_normal

theorem Subgroup.sylow_mem_fixedPoints_iff (H : Subgroup G) {P : Sylow p G} :
    P ∈ fixedPoints H (Sylow p G) ↔ H ≤ (P : Subgroup G).normalizer := by
  simp_rw [SetLike.le_def, ← Sylow.smul_eq_iff_mem_normalizer] <;> exact Subtype.forall
#align subgroup.sylow_mem_fixed_points_iff Subgroup.sylow_mem_fixedPoints_iff

theorem IsPGroup.inf_normalizer_sylow {P : Subgroup G} (hP : IsPGroup p P) (Q : Sylow p G) :
    P ⊓ (Q : Subgroup G).normalizer = P ⊓ Q :=
  le_antisymm
    (le_inf inf_le_left
      (sup_eq_right.mp
        (Q.3 (hP.to_inf_left.to_sup_of_normal_right' Q.2 inf_le_right) le_sup_right)))
    (inf_le_inf_left P le_normalizer)
#align is_p_group.inf_normalizer_sylow IsPGroup.inf_normalizer_sylow

theorem IsPGroup.sylow_mem_fixedPoints_iff {P : Subgroup G} (hP : IsPGroup p P) {Q : Sylow p G} :
    Q ∈ fixedPoints P (Sylow p G) ↔ P ≤ Q := by
  rw [P.sylow_mem_fixed_points_iff, ← inf_eq_left, hP.inf_normalizer_sylow, inf_eq_left]
#align is_p_group.sylow_mem_fixed_points_iff IsPGroup.sylow_mem_fixedPoints_iff

/-- A generalization of **Sylow's second theorem**.
  If the number of Sylow `p`-subgroups is finite, then all Sylow `p`-subgroups are conjugate. -/
instance [hp : Fact p.Prime] [Finite (Sylow p G)] : IsPretransitive G (Sylow p G) :=
  ⟨fun P Q => by
    classical
      cases nonempty_fintype (Sylow p G)
      have H := fun {R : Sylow p G} {S : orbit G P} =>
        calc
          S ∈ fixed_points R (orbit G P) ↔ S.1 ∈ fixed_points R (Sylow p G) :=
            forall_congr' fun a => Subtype.ext_iff
          _ ↔ R.1 ≤ S := R.2.sylow_mem_fixedPoints_iff
          _ ↔ S.1.1 = R := ⟨fun h => R.3 S.1.2 h, ge_of_eq⟩

      suffices Set.Nonempty (fixed_points Q (orbit G P)) by
        exact Exists.elim this fun R hR => (congr_arg _ (Sylow.ext (H.mp hR))).mp R.2
      apply Q.2.nonempty_fixed_point_of_prime_not_dvd_card
      refine' fun h => hp.out.not_dvd_one (nat.modeq_zero_iff_dvd.mp _)
      calc
        1 = card (fixed_points P (orbit G P)) := _
        _ ≡ card (orbit G P) [MOD p] := (P.2.card_modEq_card_fixedPoints (orbit G P)).symm
        _ ≡ 0 [MOD p] := nat.modeq_zero_iff_dvd.mpr h

      rw [← Set.card_singleton (⟨P, mem_orbit_self P⟩ : orbit G P)]
      refine' card_congr' (congr_arg _ (Eq.symm _))
      rw [Set.eq_singleton_iff_unique_mem]
      exact ⟨H.mpr rfl, fun R h => Subtype.ext (Sylow.ext (H.mp h))⟩⟩

variable (p) (G)

/-- A generalization of **Sylow's third theorem**.
  If the number of Sylow `p`-subgroups is finite, then it is congruent to `1` modulo `p`. -/
theorem card_sylow_modEq_one [Fact p.Prime] [Fintype (Sylow p G)] : card (Sylow p G) ≡ 1 [MOD p] :=
  by
  refine' sylow.nonempty.elim fun P : Sylow p G => _
  have : fixed_points P.1 (Sylow p G) = {P} :=
    Set.ext fun Q : Sylow p G =>
      calc
        Q ∈ fixed_points P (Sylow p G) ↔ P.1 ≤ Q := P.2.sylow_mem_fixedPoints_iff
        _ ↔ Q.1 = P.1 := ⟨P.3 Q.2, ge_of_eq⟩
        _ ↔ Q ∈ {P} := sylow.ext_iff.symm.trans set.mem_singleton_iff.symm

  have : Fintype (fixed_points P.1 (Sylow p G)) :=
    by
    rw [this]
    infer_instance
  have : card (fixed_points P.1 (Sylow p G)) = 1 := by simp [this]
  exact (P.2.card_modEq_card_fixedPoints (Sylow p G)).trans (by rw [this])
#align card_sylow_modeq_one card_sylow_modEq_one

theorem not_dvd_card_sylow [hp : Fact p.Prime] [Fintype (Sylow p G)] : ¬p ∣ card (Sylow p G) :=
  fun h =>
  hp.1.ne_one
    (Nat.dvd_one.mp
      ((Nat.modEq_iff_dvd' zero_le_one).mp
        ((Nat.modEq_zero_iff_dvd.mpr h).symm.trans (card_sylow_modEq_one p G))))
#align not_dvd_card_sylow not_dvd_card_sylow

variable {p} {G}

/-- Sylow subgroups are isomorphic -/
def Sylow.equivSmul (P : Sylow p G) (g : G) : P ≃* (g • P : Sylow p G) :=
  equivSMul (MulAut.conj g) ↑P
#align sylow.equiv_smul Sylow.equivSmul

/-- Sylow subgroups are isomorphic -/
noncomputable def Sylow.equiv [Fact p.Prime] [Finite (Sylow p G)] (P Q : Sylow p G) : P ≃* Q :=
  by
  rw [← Classical.choose_spec (exists_smul_eq G P Q)]
  exact P.equiv_smul (Classical.choose (exists_smul_eq G P Q))
#align sylow.equiv Sylow.equiv

@[simp]
theorem Sylow.orbit_eq_top [Fact p.Prime] [Finite (Sylow p G)] (P : Sylow p G) : orbit G P = ⊤ :=
  top_le_iff.mp fun Q hQ => exists_smul_eq G P Q
#align sylow.orbit_eq_top Sylow.orbit_eq_top

theorem Sylow.stabilizer_eq_normalizer (P : Sylow p G) :
    stabilizer G P = (P : Subgroup G).normalizer :=
  ext fun g => Sylow.smul_eq_iff_mem_normalizer
#align sylow.stabilizer_eq_normalizer Sylow.stabilizer_eq_normalizer

theorem Sylow.conj_eq_normalizer_conj_of_mem_centralizer [Fact p.Prime] [Finite (Sylow p G)]
    (P : Sylow p G) (x g : G) (hx : x ∈ (P : Subgroup G).centralizer)
    (hy : g⁻¹ * x * g ∈ (P : Subgroup G).centralizer) :
    ∃ n ∈ (P : Subgroup G).normalizer, g⁻¹ * x * g = n⁻¹ * x * n :=
  by
  have h1 : ↑P ≤ (zpowers x).centralizer := by rwa [le_centralizer_iff, zpowers_le]
  have h2 : ↑(g • P) ≤ (zpowers x).centralizer :=
    by
    rw [le_centralizer_iff, zpowers_le]
    rintro - ⟨z, hz, rfl⟩
    specialize hy z hz
    rwa [← mul_assoc, ← eq_mul_inv_iff_mul_eq, mul_assoc, mul_assoc, mul_assoc, ← mul_assoc,
      eq_inv_mul_iff_mul_eq, ← mul_assoc, ← mul_assoc] at hy
  obtain ⟨h, hh⟩ := exists_smul_eq (zpowers x).centralizer ((g • P).Subtype h2) (P.subtype h1)
  simp_rw [Sylow.smul_subtype, smul_def, smul_smul] at hh
  refine' ⟨h * g, sylow.smul_eq_iff_mem_normalizer.mp (Sylow.subtype_injective hh), _⟩
  rw [← mul_assoc, Commute.right_comm (h.prop x (mem_zpowers x)), mul_inv_rev, inv_mul_cancel_right]
#align sylow.conj_eq_normalizer_conj_of_mem_centralizer Sylow.conj_eq_normalizer_conj_of_mem_centralizer

theorem Sylow.conj_eq_normalizer_conj_of_mem [Fact p.Prime] [Finite (Sylow p G)] (P : Sylow p G)
    [hP : (P : Subgroup G).IsCommutative] (x g : G) (hx : x ∈ P) (hy : g⁻¹ * x * g ∈ P) :
    ∃ n ∈ (P : Subgroup G).normalizer, g⁻¹ * x * g = n⁻¹ * x * n :=
  P.conj_eq_normalizer_conj_of_mem_centralizer x g (le_centralizer P hx) (le_centralizer P hy)
#align sylow.conj_eq_normalizer_conj_of_mem Sylow.conj_eq_normalizer_conj_of_mem

/-- Sylow `p`-subgroups are in bijection with cosets of the normalizer of a Sylow `p`-subgroup -/
noncomputable def Sylow.equivQuotientNormalizer [Fact p.Prime] [Fintype (Sylow p G)]
    (P : Sylow p G) : Sylow p G ≃ G ⧸ (P : Subgroup G).normalizer :=
  calc
    Sylow p G ≃ (⊤ : Set (Sylow p G)) := (Equiv.Set.univ (Sylow p G)).symm
    _ ≃ orbit G P := by rw [P.orbit_eq_top]
    _ ≃ G ⧸ stabilizer G P := (orbitEquivQuotientStabilizer G P)
    _ ≃ G ⧸ (P : Subgroup G).normalizer := by rw [P.stabilizer_eq_normalizer]

#align sylow.equiv_quotient_normalizer Sylow.equivQuotientNormalizer

noncomputable instance [Fact p.Prime] [Fintype (Sylow p G)] (P : Sylow p G) :
    Fintype (G ⧸ (P : Subgroup G).normalizer) :=
  ofEquiv (Sylow p G) P.equivQuotientNormalizer

theorem card_sylow_eq_card_quotient_normalizer [Fact p.Prime] [Fintype (Sylow p G)]
    (P : Sylow p G) : card (Sylow p G) = card (G ⧸ (P : Subgroup G).normalizer) :=
  card_congr P.equivQuotientNormalizer
#align card_sylow_eq_card_quotient_normalizer card_sylow_eq_card_quotient_normalizer

theorem card_sylow_eq_index_normalizer [Fact p.Prime] [Fintype (Sylow p G)] (P : Sylow p G) :
    card (Sylow p G) = (P : Subgroup G).normalizer.index :=
  (card_sylow_eq_card_quotient_normalizer P).trans (P : Subgroup G).normalizer.index_eq_card.symm
#align card_sylow_eq_index_normalizer card_sylow_eq_index_normalizer

theorem card_sylow_dvd_index [Fact p.Prime] [Fintype (Sylow p G)] (P : Sylow p G) :
    card (Sylow p G) ∣ (P : Subgroup G).index :=
  ((congr_arg _ (card_sylow_eq_index_normalizer P)).mp dvd_rfl).trans
    (index_dvd_of_le le_normalizer)
#align card_sylow_dvd_index card_sylow_dvd_index

theorem not_dvd_index_sylow' [hp : Fact p.Prime] (P : Sylow p G) [(P : Subgroup G).Normal]
    [FiniteIndex (P : Subgroup G)] : ¬p ∣ (P : Subgroup G).index :=
  by
  intro h
  haveI := (P : Subgroup G).fintypeQuotientOfFiniteIndex
  rw [index_eq_card] at h
  obtain ⟨x, hx⟩ := exists_prime_orderOf_dvd_card p h
  have h := IsPGroup.of_card ((order_eq_card_zpowers.symm.trans hx).trans (pow_one p).symm)
  let Q := (zpowers x).comap (QuotientGroup.mk' (P : Subgroup G))
  have hQ : IsPGroup p Q := by
    apply h.comap_of_ker_is_p_group
    rw [QuotientGroup.ker_mk']
    exact P.2
  replace hp := mt order_of_eq_one_iff.mpr (ne_of_eq_of_ne hx hp.1.ne_one)
  rw [← zpowers_eq_bot, ← Ne, ← bot_lt_iff_ne_bot, ←
    comap_lt_comap_of_surjective (QuotientGroup.mk'_surjective _), MonoidHom.comap_bot,
    QuotientGroup.ker_mk'] at hp
  exact hp.ne' (P.3 hQ hp.le)
#align not_dvd_index_sylow' not_dvd_index_sylow'

theorem not_dvd_index_sylow [hp : Fact p.Prime] [Finite (Sylow p G)] (P : Sylow p G)
    (hP : relindex ↑P (P : Subgroup G).normalizer ≠ 0) : ¬p ∣ (P : Subgroup G).index :=
  by
  cases nonempty_fintype (Sylow p G)
  rw [← relindex_mul_index le_normalizer, ← card_sylow_eq_index_normalizer]
  haveI : (P.subtype le_normalizer : Subgroup (P : Subgroup G).normalizer).Normal :=
    Subgroup.normal_in_normalizer
  haveI : finite_index ↑(P.subtype le_normalizer) := ⟨hP⟩
  replace hP := not_dvd_index_sylow' (P.subtype le_normalizer)
  exact hp.1.not_dvd_mul hP (not_dvd_card_sylow p G)
#align not_dvd_index_sylow not_dvd_index_sylow

/-- **Frattini's Argument**: If `N` is a normal subgroup of `G`, and if `P` is a Sylow `p`-subgroup
  of `N`, then `N_G(P) ⊔ N = G`. -/
theorem Sylow.normalizer_sup_eq_top {p : ℕ} [Fact p.Prime] {N : Subgroup G} [N.Normal]
    [Finite (Sylow p N)] (P : Sylow p N) : ((↑P : Subgroup N).map N.Subtype).normalizer ⊔ N = ⊤ :=
  by
  refine' top_le_iff.mp fun g hg => _
  obtain ⟨n, hn⟩ := exists_smul_eq N ((MulAut.conjNormal g : MulAut N) • P) P
  rw [← inv_mul_cancel_left (↑n) g, sup_comm]
  apply mul_mem_sup (N.inv_mem n.2)
  rw [Sylow.smul_def, ← mul_smul, ← MulAut.conjNormal_val, ← mul_aut.conj_normal.map_mul,
    Sylow.ext_iff, Sylow.pointwise_smul_def, pointwise_smul_def] at hn
  refine' fun x =>
    (mem_map_iff_mem
            (show Function.Injective (MulAut.conj (↑n * g)).toMonoidHom from
              (MulAut.conj (↑n * g)).Injective)).symm.trans
      _
  rw [map_map, ← congr_arg (map N.subtype) hn, map_map]
  rfl
#align sylow.normalizer_sup_eq_top Sylow.normalizer_sup_eq_top

/-- **Frattini's Argument**: If `N` is a normal subgroup of `G`, and if `P` is a Sylow `p`-subgroup
  of `N`, then `N_G(P) ⊔ N = G`. -/
theorem Sylow.normalizer_sup_eq_top' {p : ℕ} [Fact p.Prime] {N : Subgroup G} [N.Normal]
    [Finite (Sylow p N)] (P : Sylow p G) (hP : ↑P ≤ N) : (P : Subgroup G).normalizer ⊔ N = ⊤ := by
  rw [← Sylow.normalizer_sup_eq_top (P.subtype hP), P.coe_subtype, subgroup_of_map_subtype,
    inf_of_le_left hP]
#align sylow.normalizer_sup_eq_top' Sylow.normalizer_sup_eq_top'

end InfiniteSylow

open Equiv Equiv.Perm Finset Function List QuotientGroup

open BigOperators

universe u v w

variable {G : Type u} {α : Type v} {β : Type w} [Group G]

attribute [local instance] Subtype.fintype setFintype Classical.propDecidable

theorem QuotientGroup.card_preimage_mk [Fintype G] (s : Subgroup G) (t : Set (G ⧸ s)) :
    Fintype.card (QuotientGroup.mk ⁻¹' t) = Fintype.card s * Fintype.card t := by
  rw [← Fintype.card_prod, Fintype.card_congr (preimage_mk_equiv_subgroup_times_set _ _)]
#align quotient_group.card_preimage_mk QuotientGroup.card_preimage_mk

namespace Sylow

open Subgroup Submonoid MulAction

theorem mem_fixedPoints_mul_left_cosets_iff_mem_normalizer {H : Subgroup G} [Finite ↥(H : Set G)]
    {x : G} : (x : G ⧸ H) ∈ fixedPoints H (G ⧸ H) ↔ x ∈ normalizer H :=
  ⟨fun hx =>
    have ha : ∀ {y : G ⧸ H}, y ∈ orbit H (x : G ⧸ H) → y = x := fun _ => (mem_fixedPoints' _).1 hx _
    inv_mem_iff.1
      (mem_normalizer_fintype fun n (hn : n ∈ H) =>
        have : (n⁻¹ * x)⁻¹ * x ∈ H := QuotientGroup.eq.1 (ha (mem_orbit _ ⟨n⁻¹, H.inv_mem hn⟩))
        show _ ∈ H by
          rw [mul_inv_rev, inv_inv] at this
          convert this
          rw [inv_inv]),
    fun hx : ∀ n : G, n ∈ H ↔ x * n * x⁻¹ ∈ H =>
    (mem_fixedPoints' _).2 fun y =>
      Quotient.inductionOn' y fun y hy =>
        QuotientGroup.eq.2
          (let ⟨⟨b, hb₁⟩, hb₂⟩ := hy
          have hb₂ : (b * x)⁻¹ * y ∈ H := QuotientGroup.eq.1 hb₂
          inv_mem_iff.1 <|
            (hx _).2 <|
              (mul_mem_cancel_left (inv_mem hb₁)).1 <| by
                rw [hx] at hb₂ <;> simpa [mul_inv_rev, mul_assoc] using hb₂)⟩
#align sylow.mem_fixed_points_mul_left_cosets_iff_mem_normalizer Sylow.mem_fixedPoints_mul_left_cosets_iff_mem_normalizer

/-- The fixed points of the action of `H` on its cosets correspond to `normalizer H / H`. -/
def fixedPointsMulLeftCosetsEquivQuotient (H : Subgroup G) [Finite (H : Set G)] :
    MulAction.fixedPoints H (G ⧸ H) ≃
      normalizer H ⧸ Subgroup.comap ((normalizer H).Subtype : normalizer H →* G) H :=
  @subtypeQuotientEquivQuotientSubtype G (normalizer H : Set G) (id _) (id _) (fixedPoints _ _)
    (fun a => (@mem_fixedPoints_mul_left_cosets_iff_mem_normalizer _ _ _ ‹_› _).symm)
    (by
      intros
      rw [setoidHasEquiv]
      simp only [left_rel_apply]
      rfl)
#align sylow.fixed_points_mul_left_cosets_equiv_quotient Sylow.fixedPointsMulLeftCosetsEquivQuotient

/-- If `H` is a `p`-subgroup of `G`, then the index of `H` inside its normalizer is congruent
  mod `p` to the index of `H`.  -/
theorem card_quotient_normalizer_modEq_card_quotient [Fintype G] {p : ℕ} {n : ℕ} [hp : Fact p.Prime]
    {H : Subgroup G} (hH : Fintype.card H = p ^ n) :
    card (normalizer H ⧸ Subgroup.comap ((normalizer H).Subtype : normalizer H →* G) H) ≡
      card (G ⧸ H) [MOD p] :=
  by
  rw [← Fintype.card_congr (fixed_points_mul_left_cosets_equiv_quotient H)]
  exact ((IsPGroup.of_card hH).card_modEq_card_fixedPoints _).symm
#align sylow.card_quotient_normalizer_modeq_card_quotient Sylow.card_quotient_normalizer_modEq_card_quotient

/-- If `H` is a subgroup of `G` of cardinality `p ^ n`, then the cardinality of the
  normalizer of `H` is congruent mod `p ^ (n + 1)` to the cardinality of `G`.  -/
theorem card_normalizer_modEq_card [Fintype G] {p : ℕ} {n : ℕ} [hp : Fact p.Prime] {H : Subgroup G}
    (hH : Fintype.card H = p ^ n) : card (normalizer H) ≡ card G [MOD p ^ (n + 1)] :=
  by
  have : H.subgroupOf (normalizer H) ≃ H := (subgroupOfEquivOfLe le_normalizer).toEquiv
  rw [card_eq_card_quotient_mul_card_subgroup H,
    card_eq_card_quotient_mul_card_subgroup (H.subgroup_of (normalizer H)), Fintype.card_congr this,
    hH, pow_succ]
  exact (card_quotient_normalizer_modeq_card_quotient hH).mul_right' _
#align sylow.card_normalizer_modeq_card Sylow.card_normalizer_modEq_card

/-- If `H` is a `p`-subgroup but not a Sylow `p`-subgroup, then `p` divides the
  index of `H` inside its normalizer. -/
theorem prime_dvd_card_quotient_normalizer [Fintype G] {p : ℕ} {n : ℕ} [hp : Fact p.Prime]
    (hdvd : p ^ (n + 1) ∣ card G) {H : Subgroup G} (hH : Fintype.card H = p ^ n) :
    p ∣ card (normalizer H ⧸ Subgroup.comap ((normalizer H).Subtype : normalizer H →* G) H) :=
  let ⟨s, hs⟩ := exists_eq_mul_left_of_dvd hdvd
  have hcard : card (G ⧸ H) = s * p :=
    (mul_left_inj' (show card H ≠ 0 from Fintype.card_ne_zero)).1
      (by
        rwa [← card_eq_card_quotient_mul_card_subgroup H, hH, hs, pow_succ', mul_assoc, mul_comm p])
  have hm :
    s * p % p =
      card (normalizer H ⧸ Subgroup.comap ((normalizer H).Subtype : normalizer H →* G) H) % p :=
    hcard ▸ (card_quotient_normalizer_modEq_card_quotient hH).symm
  Nat.dvd_of_mod_eq_zero (by rwa [Nat.mod_eq_zero_of_dvd (dvd_mul_left _ _), eq_comm] at hm)
#align sylow.prime_dvd_card_quotient_normalizer Sylow.prime_dvd_card_quotient_normalizer

/-- If `H` is a `p`-subgroup but not a Sylow `p`-subgroup of cardinality `p ^ n`,
  then `p ^ (n + 1)` divides the cardinality of the normalizer of `H`. -/
theorem prime_pow_dvd_card_normalizer [Fintype G] {p : ℕ} {n : ℕ} [hp : Fact p.Prime]
    (hdvd : p ^ (n + 1) ∣ card G) {H : Subgroup G} (hH : Fintype.card H = p ^ n) :
    p ^ (n + 1) ∣ card (normalizer H) :=
  Nat.modEq_zero_iff_dvd.1 ((card_normalizer_modEq_card hH).trans hdvd.modEq_zero_nat)
#align sylow.prime_pow_dvd_card_normalizer Sylow.prime_pow_dvd_card_normalizer

/-- If `H` is a subgroup of `G` of cardinality `p ^ n`,
  then `H` is contained in a subgroup of cardinality `p ^ (n + 1)`
  if `p ^ (n + 1)` divides the cardinality of `G` -/
theorem exists_subgroup_card_pow_succ [Fintype G] {p : ℕ} {n : ℕ} [hp : Fact p.Prime]
    (hdvd : p ^ (n + 1) ∣ card G) {H : Subgroup G} (hH : Fintype.card H = p ^ n) :
    ∃ K : Subgroup G, Fintype.card K = p ^ (n + 1) ∧ H ≤ K :=
  let ⟨s, hs⟩ := exists_eq_mul_left_of_dvd hdvd
  have hcard : card (G ⧸ H) = s * p :=
    (mul_left_inj' (show card H ≠ 0 from Fintype.card_ne_zero)).1
      (by
        rwa [← card_eq_card_quotient_mul_card_subgroup H, hH, hs, pow_succ', mul_assoc, mul_comm p])
  have hm : s * p % p = card (normalizer H ⧸ H.subgroupOf H.normalizer) % p :=
    card_congr (fixedPointsMulLeftCosetsEquivQuotient H) ▸
      hcard ▸ (IsPGroup.of_card hH).card_modEq_card_fixedPoints _
  have hm' : p ∣ card (normalizer H ⧸ H.subgroupOf H.normalizer) :=
    Nat.dvd_of_mod_eq_zero (by rwa [Nat.mod_eq_zero_of_dvd (dvd_mul_left _ _), eq_comm] at hm)
  let ⟨x, hx⟩ := @exists_prime_orderOf_dvd_card _ (QuotientGroup.Quotient.group _) _ _ hp hm'
  have hequiv : H ≃ H.subgroupOf H.normalizer := (subgroupOfEquivOfLe le_normalizer).symm.toEquiv
  ⟨Subgroup.map (normalizer H).Subtype
      (Subgroup.comap (mk' (H.subgroupOf H.normalizer)) (zpowers x)),
    by
    show
      card
          ↥(map H.normalizer.subtype
              (comap (mk' (H.subgroup_of H.normalizer)) (Subgroup.zpowers x))) =
        p ^ (n + 1)
    suffices
      card
          ↥(Subtype.val ''
              (Subgroup.comap (mk' (H.subgroup_of H.normalizer)) (zpowers x) : Set ↥H.normalizer)) =
        p ^ (n + 1)
      by convert this using 2
    rw [Set.card_image_of_injective
        (Subgroup.comap (mk' (H.subgroup_of H.normalizer)) (zpowers x) : Set H.normalizer)
        Subtype.val_injective,
      pow_succ', ← hH, Fintype.card_congr hequiv, ← hx, orderOf_eq_card_zpowers, ←
      Fintype.card_prod]
    exact @Fintype.card_congr _ _ (id _) (id _) (preimage_mk_equiv_subgroup_times_set _ _),
    by
    intro y hy
    simp only [exists_prop, Subgroup.coeSubtype, mk'_apply, Subgroup.mem_map, Subgroup.mem_comap]
    refine' ⟨⟨y, le_normalizer hy⟩, ⟨0, _⟩, rfl⟩
    rw [zpow_zero, eq_comm, QuotientGroup.eq_one_iff]
    simpa using hy⟩
#align sylow.exists_subgroup_card_pow_succ Sylow.exists_subgroup_card_pow_succ

/-- If `H` is a subgroup of `G` of cardinality `p ^ n`,
  then `H` is contained in a subgroup of cardinality `p ^ m`
  if `n ≤ m` and `p ^ m` divides the cardinality of `G` -/
theorem exists_subgroup_card_pow_prime_le [Fintype G] (p : ℕ) :
    ∀ {n m : ℕ} [hp : Fact p.Prime] (hdvd : p ^ m ∣ card G) (H : Subgroup G) (hH : card H = p ^ n)
      (hnm : n ≤ m), ∃ K : Subgroup G, card K = p ^ m ∧ H ≤ K
  | n, m => fun hp hdvd H hH hnm =>
    (lt_or_eq_of_le hnm).elim
      (fun hnm : n < m =>
        have h0m : 0 < m := lt_of_le_of_lt n.zero_le hnm
        have wf : m - 1 < m := Nat.sub_lt h0m zero_lt_one
        have hnm1 : n ≤ m - 1 := le_tsub_of_add_le_right hnm
        let ⟨K, hK⟩ :=
          @exists_subgroup_card_pow_prime_le n (m - 1) hp
            (Nat.pow_dvd_of_le_of_pow_dvd tsub_le_self hdvd) H hH hnm1
        have hdvd' : p ^ (m - 1 + 1) ∣ card G := by rwa [tsub_add_cancel_of_le h0m.nat_succ_le]
        let ⟨K', hK'⟩ := @exists_subgroup_card_pow_succ _ _ _ _ _ hp hdvd' K hK.1
        ⟨K', by rw [hK'.1, tsub_add_cancel_of_le h0m.nat_succ_le], le_trans hK.2 hK'.2⟩)
      fun hnm : n = m => ⟨H, by simp [hH, hnm]⟩
#align sylow.exists_subgroup_card_pow_prime_le Sylow.exists_subgroup_card_pow_prime_le

/-- A generalisation of **Sylow's first theorem**. If `p ^ n` divides
  the cardinality of `G`, then there is a subgroup of cardinality `p ^ n` -/
theorem exists_subgroup_card_pow_prime [Fintype G] (p : ℕ) {n : ℕ} [Fact p.Prime]
    (hdvd : p ^ n ∣ card G) : ∃ K : Subgroup G, Fintype.card K = p ^ n :=
  let ⟨K, hK⟩ := exists_subgroup_card_pow_prime_le p hdvd ⊥ (by simp) n.zero_le
  ⟨K, hK.1⟩
#align sylow.exists_subgroup_card_pow_prime Sylow.exists_subgroup_card_pow_prime

theorem pow_dvd_card_of_pow_dvd_card [Fintype G] {p n : ℕ} [hp : Fact p.Prime] (P : Sylow p G)
    (hdvd : p ^ n ∣ card G) : p ^ n ∣ card P :=
  (hp.1.coprime_pow_of_not_dvd
          (not_dvd_index_sylow P index_ne_zero_of_finite)).symm.dvd_of_dvd_mul_left
    ((index_mul_card P.1).symm ▸ hdvd)
#align sylow.pow_dvd_card_of_pow_dvd_card Sylow.pow_dvd_card_of_pow_dvd_card

theorem dvd_card_of_dvd_card [Fintype G] {p : ℕ} [Fact p.Prime] (P : Sylow p G)
    (hdvd : p ∣ card G) : p ∣ card P :=
  by
  rw [← pow_one p] at hdvd
  have key := P.pow_dvd_card_of_pow_dvd_card hdvd
  rwa [pow_one] at key
#align sylow.dvd_card_of_dvd_card Sylow.dvd_card_of_dvd_card

/-- Sylow subgroups are Hall subgroups. -/
theorem card_coprime_index [Fintype G] {p : ℕ} [hp : Fact p.Prime] (P : Sylow p G) :
    (card P).coprime (index (P : Subgroup G)) :=
  let ⟨n, hn⟩ := IsPGroup.iff_card.mp P.2
  hn.symm ▸ (hp.1.coprime_pow_of_not_dvd (not_dvd_index_sylow P index_ne_zero_of_finite)).symm
#align sylow.card_coprime_index Sylow.card_coprime_index

theorem ne_bot_of_dvd_card [Fintype G] {p : ℕ} [hp : Fact p.Prime] (P : Sylow p G)
    (hdvd : p ∣ card G) : (P : Subgroup G) ≠ ⊥ :=
  by
  refine' fun h => hp.out.not_dvd_one _
  have key : p ∣ card (P : Subgroup G) := P.dvd_card_of_dvd_card hdvd
  rwa [h, card_bot] at key
#align sylow.ne_bot_of_dvd_card Sylow.ne_bot_of_dvd_card

/-- The cardinality of a Sylow group is `p ^ n`
 where `n` is the multiplicity of `p` in the group order. -/
theorem card_eq_multiplicity [Fintype G] {p : ℕ} [hp : Fact p.Prime] (P : Sylow p G) :
    card P = p ^ Nat.factorization (card G) p :=
  by
  obtain ⟨n, heq : card P = _⟩ := is_p_group.iff_card.mp P.is_p_group'
  refine' Nat.dvd_antisymm _ (P.pow_dvd_card_of_pow_dvd_card (Nat.ord_proj_dvd _ p))
  rw [HEq, ← hp.out.pow_dvd_iff_dvd_ord_proj (show card G ≠ 0 from card_ne_zero), ← HEq]
  exact P.1.card_subgroup_dvd_card
#align sylow.card_eq_multiplicity Sylow.card_eq_multiplicity

theorem subsingleton_of_normal {p : ℕ} [Fact p.Prime] [Finite (Sylow p G)] (P : Sylow p G)
    (h : (P : Subgroup G).Normal) : Subsingleton (Sylow p G) :=
  by
  apply Subsingleton.intro
  intro Q R
  obtain ⟨x, h1⟩ := exists_smul_eq G P Q
  obtain ⟨x, h2⟩ := exists_smul_eq G P R
  rw [Sylow.smul_eq_of_normal] at h1 h2
  rw [← h1, ← h2]
#align sylow.subsingleton_of_normal Sylow.subsingleton_of_normal

section Pointwise

open Pointwise

theorem characteristic_of_normal {p : ℕ} [Fact p.Prime] [Finite (Sylow p G)] (P : Sylow p G)
    (h : (P : Subgroup G).Normal) : (P : Subgroup G).Characteristic :=
  by
  haveI := Sylow.subsingleton_of_normal P h
  rw [characteristic_iff_map_eq]
  intro Φ
  show (Φ • P).toSubgroup = P.to_subgroup
  congr
#align sylow.characteristic_of_normal Sylow.characteristic_of_normal

end Pointwise

theorem normal_of_normalizer_normal {p : ℕ} [Fact p.Prime] [Finite (Sylow p G)] (P : Sylow p G)
    (hn : (↑P : Subgroup G).normalizer.Normal) : (↑P : Subgroup G).Normal := by
  rw [← normalizer_eq_top, ← normalizer_sup_eq_top' P le_normalizer, sup_idem]
#align sylow.normal_of_normalizer_normal Sylow.normal_of_normalizer_normal

@[simp]
theorem normalizer_normalizer {p : ℕ} [Fact p.Prime] [Finite (Sylow p G)] (P : Sylow p G) :
    (↑P : Subgroup G).normalizer.normalizer = (↑P : Subgroup G).normalizer :=
  by
  have := normal_of_normalizer_normal (P.subtype (le_normalizer.trans le_normalizer))
  simp_rw [← normalizer_eq_top, coeSubtype, ← subgroup_of_normalizer_eq le_normalizer, ←
    subgroup_of_normalizer_eq le_rfl, subgroup_of_self] at this
  rw [← subtype_range (P : Subgroup G).normalizer.normalizer, MonoidHom.range_eq_map, ← this rfl]
  exact map_comap_eq_self (le_normalizer.trans (ge_of_eq (subtype_range _)))
#align sylow.normalizer_normalizer Sylow.normalizer_normalizer

theorem normal_of_all_max_subgroups_normal [Finite G]
    (hnc : ∀ H : Subgroup G, IsCoatom H → H.Normal) {p : ℕ} [Fact p.Prime] [Finite (Sylow p G)]
    (P : Sylow p G) : (↑P : Subgroup G).Normal :=
  normalizer_eq_top.mp
    (by
      rcases eq_top_or_exists_le_coatom (↑P : Subgroup G).normalizer with (heq | ⟨K, hK, hNK⟩)
      · exact HEq
      · haveI := hnc _ hK
        have hPK : ↑P ≤ K := le_trans le_normalizer hNK
        refine' (hK.1 _).elim
        rw [← sup_of_le_right hNK, P.normalizer_sup_eq_top' hPK])
#align sylow.normal_of_all_max_subgroups_normal Sylow.normal_of_all_max_subgroups_normal

theorem normal_of_normalizerCondition (hnc : NormalizerCondition G) {p : ℕ} [Fact p.Prime]
    [Finite (Sylow p G)] (P : Sylow p G) : (↑P : Subgroup G).Normal :=
  normalizer_eq_top.mp <|
    normalizerCondition_iff_only_full_group_self_normalizing.mp hnc _ <| normalizer_normalizer _
#align sylow.normal_of_normalizer_condition Sylow.normal_of_normalizerCondition

open BigOperators

/-- If all its sylow groups are normal, then a finite group is isomorphic to the direct product
of these sylow groups.
-/
noncomputable def directProductOfNormal [Fintype G]
    (hn : ∀ {p : ℕ} [Fact p.Prime] (P : Sylow p G), (↑P : Subgroup G).Normal) :
    (∀ p : (card G).factorization.support, ∀ P : Sylow p G, (↑P : Subgroup G)) ≃* G :=
  by
  set ps := (Fintype.card G).factorization.support
  -- “The” sylow group for p
  let P : ∀ p, Sylow p G := default
  have hcomm : Pairwise fun p₁ p₂ : ps => ∀ x y : G, x ∈ P p₁ → y ∈ P p₂ → Commute x y :=
    by
    rintro ⟨p₁, hp₁⟩ ⟨p₂, hp₂⟩ hne
    haveI hp₁' := Fact.mk (Nat.prime_of_mem_factorization hp₁)
    haveI hp₂' := Fact.mk (Nat.prime_of_mem_factorization hp₂)
    have hne' : p₁ ≠ p₂ := by simpa using hne
    apply Subgroup.commute_of_normal_of_disjoint _ _ (hn (P p₁)) (hn (P p₂))
    apply IsPGroup.disjoint_of_ne p₁ p₂ hne' _ _ (P p₁).is_p_group' (P p₂).is_p_group'
  refine' MulEquiv.trans _ _
  -- There is only one sylow group for each p, so the inner product is trivial
  show (∀ p : ps, ∀ P : Sylow p G, P) ≃* ∀ p : ps, P p
  · -- here we need to help the elaborator with an explicit instantiation
    apply @MulEquiv.piCongrRight ps (fun p => ∀ P : Sylow p G, P) (fun p => P p) _ _
    rintro ⟨p, hp⟩
    haveI hp' := Fact.mk (Nat.prime_of_mem_factorization hp)
    haveI := subsingleton_of_normal _ (hn (P p))
    change (∀ P : Sylow p G, P) ≃* P p
    exact MulEquiv.piSubsingleton _ _
  show (∀ p : ps, P p) ≃* G
  apply MulEquiv.ofBijective (Subgroup.noncommPiCoprod hcomm)
  apply (bijective_iff_injective_and_card _).mpr
  constructor
  show injective _
  · apply Subgroup.injective_noncommPiCoprod_of_independent
    apply independent_of_coprime_order hcomm
    rintro ⟨p₁, hp₁⟩ ⟨p₂, hp₂⟩ hne
    haveI hp₁' := Fact.mk (Nat.prime_of_mem_factorization hp₁)
    haveI hp₂' := Fact.mk (Nat.prime_of_mem_factorization hp₂)
    have hne' : p₁ ≠ p₂ := by simpa using hne
    apply IsPGroup.coprime_card_of_ne p₁ p₂ hne' _ _ (P p₁).is_p_group' (P p₂).is_p_group'
  show card (∀ p : ps, P p) = card G
  ·
    calc
      card (∀ p : ps, P p) = ∏ p : ps, card ↥(P p) := Fintype.card_pi
      _ = ∏ p : ps, p.1 ^ (card G).factorization p.1 :=
        by
        congr 1 with ⟨p, hp⟩
        exact @card_eq_multiplicity _ _ _ p ⟨Nat.prime_of_mem_factorization hp⟩ (P p)
      _ = ∏ p in ps, p ^ (card G).factorization p :=
        (Finset.prod_finset_coe (fun p => p ^ (card G).factorization p) _)
      _ = (card G).factorization.Prod pow := rfl
      _ = card G := Nat.factorization_prod_pow_eq_self Fintype.card_ne_zero

#align sylow.direct_product_of_normal Sylow.directProductOfNormal

end Sylow

author: leanprover-community


text:
import algebra.category.FinVect

namespace kassel

noncomputable theory

open_locale matrix big_operators

variables
  {K: Type*} [field K]
  {V: Type*} [add_comm_group V] [module K V] [finite_dimensional K V]
  {ι: Type*} [fintype ι] (bV: basis ι K V)
  {ι': Type*} [fintype ι'] [decidable_eq ι'] (bV': basis ι' K V)

section lemmas

lemma basis_change (i: ι):
  bV i = ∑ (j: ι'), (bV'.to_matrix bV j i) • (bV' j) :=
by simp

lemma basis_change_dual (i: ι):
  bV.coord i = ∑ (j: ι'), (bV.to_matrix bV' i j) • (bV'.coord j) :=
begin
  ext,
  simp only [
    algebra.id.smul_eq_mul, linear_map.smul_apply, fintype.sum_apply, linear_map.coe_fn_sum, basis.coe_dual_basis, finset.sum_congr, finsupp.lapply_apply, linear_equiv.coe_coe, function.comp_app, linear_map.coe_comp,
    basis.to_matrix_apply, basis.dual_basis_apply, basis.coord, basis.sum_repr_mul_repr
  ],
end

lemma basis_change_relation (i j: ι'):
  ∑ (k: ι), bV'.to_matrix ⇑bV i k * bV.to_matrix ⇑bV' k j = (finsupp.single j 1) i :=
begin
  simp_rw basis.to_matrix_apply,
  rw [basis.sum_repr_mul_repr, basis.repr_self],
end

variables
  {α β γ: Type*} [fintype α] [fintype β] [fintype γ]
  {s t: finset α}
  {M: Type*} [add_comm_monoid M]

lemma sum_nonzero [decidable_eq α]
  (h1: t ⊆ s) (f: α → M) (h2: ∀ x ∈ s \ t, f x = 0):
  s.sum f = t.sum f :=
begin
  simp [←(finset.sum_filter_add_sum_filter_not s (λ x, x ∈ t) f)],
  rw [finset.filter_not, finset.filter_mem_eq_inter],
  simp only [(finset.inter_eq_right_iff_subset t s).mpr h1],
  simp [finset.sum_eq_zero h2],
end

lemma finset.sum_sum_comm (f: α → β → γ → M):
  ∑ (x: α) (y: β) (z: γ), f x y z = ∑ (y: β) (z: γ) (x: α), f x y z :=
begin
  rw finset.sum_comm,
  have h: ∀ y, ∑ (x: α) (z: γ), f x y z = ∑ (z: γ) (x: α), f x y z := (λ y, finset.sum_comm),
  simp_rw h,
end

end lemmas

lemma coevaluation_well_defined:
  ∑ (i: ι), bV i ⊗ₜ[K] bV.coord i = ∑ (i: ι'), bV' i ⊗ₜ[K] bV'.coord i :=
begin
  simp_rw [basis_change bV bV', basis_change_dual bV bV'],
  simp_rw [tensor_product.sum_tmul, tensor_product.tmul_sum, tensor_product.smul_tmul_smul],
  rw finset.sum_sum_comm,
  simp_rw ←finset.sum_smul,
  simp_rw basis_change_relation bV bV',
  have h := (λ x, sum_nonzero (finset.subset_univ {x}) (λ x_1, tensor_product.has_smul.smul (ite (x = x_1) 1 0) (bV' x ⊗ₜ[K] bV'.coord x_1)) _),
  simp [h],
  intro y, simp, tauto,
end

lemma coevaluation_apply_one':
  coevaluation K V 1 = ∑ (i: ι'), bV' i ⊗ₜ[K] bV'.coord i :=
begin
  rw coevaluation_apply_one,
  have h := coevaluation_well_defined (basis.of_vector_space K V) bV',
  rw ←h,
end

end kassel

author: youjo-tape

repo: lean-univ

save_path: github-repos/lean/youjo-tape-lean-univ


text:
/-
Copyright (c) 2020 Jujian Zhang. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jujian Zhang
-/

import data.nat.interval
import data.polynomial.derivative
import tactic.linarith

/-!
# Theory of iterated derivative
We define and prove some lemmas about iterated (formal) derivative for polynomials over a semiring.
-/

noncomputable theory

open finset nat polynomial
open_locale big_operators

namespace polynomial
universes u
variable {R : Type u}

section semiring

variables [semiring R] (r : R) (f p q : polynomial R) (n k : ℕ)

/-- `iterated_deriv f n` is the `n`-th formal derivative of the polynomial `f` -/
def iterated_deriv : polynomial R := derivative ^[n] f

@[simp] lemma iterated_deriv_zero_right : iterated_deriv f 0 = f := rfl

lemma iterated_deriv_succ : iterated_deriv f (n + 1) = (iterated_deriv f n).derivative :=
by rw [iterated_deriv, iterated_deriv, function.iterate_succ']

@[simp] lemma iterated_deriv_zero_left : iterated_deriv (0 : polynomial R) n = 0 :=
begin
  induction n with n hn,
  { exact iterated_deriv_zero_right _ },
  { rw [iterated_deriv_succ, hn, derivative_zero] },
end

@[simp] lemma iterated_deriv_add :
  iterated_deriv (p + q) n = iterated_deriv p n + iterated_deriv q n :=
begin
  induction n with n ih,
  { simp only [iterated_deriv_zero_right], },
  { simp only [iterated_deriv_succ, ih, derivative_add] }
end

@[simp] lemma iterated_deriv_smul : iterated_deriv (r • p) n = r • iterated_deriv p n :=
begin
  induction n with n ih,
  { simp only [iterated_deriv_zero_right] },
  { simp only [iterated_deriv_succ, ih, derivative_smul] }
end

@[simp] lemma iterated_deriv_X_zero : iterated_deriv (X : polynomial R) 0 = X :=
by simp only [iterated_deriv_zero_right]

@[simp] lemma iterated_deriv_X_one : iterated_deriv (X : polynomial R) 1 = 1 :=
by simp only [iterated_deriv, derivative_X, function.iterate_one]

@[simp] lemma iterated_deriv_X (h : 1 < n) : iterated_deriv (X : polynomial R) n = 0 :=
begin
  induction n with n ih,
  { exfalso, exact nat.not_lt_zero 1 h },
  { simp only [iterated_deriv_succ],
    by_cases H : n = 1,
    { rw H, simp only [iterated_deriv_X_one, derivative_one] },
    { replace h : 1 < n := array.push_back_idx h (ne.symm H),
      rw ih h, simp only [derivative_zero] } }
end

@[simp] lemma iterated_deriv_C_zero : iterated_deriv (C r) 0 = C r :=
by simp only [iterated_deriv_zero_right]

@[simp] lemma iterated_deriv_C (h : 0 < n) : iterated_deriv (C r) n = 0 :=
begin
  induction n with n ih,
  { exfalso, exact nat.lt_asymm h h },
  { by_cases H : n = 0,
    { rw [iterated_deriv_succ, H], simp only [iterated_deriv_C_zero, derivative_C] },
    { replace h : 0 < n := nat.pos_of_ne_zero H,
      rw [iterated_deriv_succ, ih h], simp only [derivative_zero] } }
end

@[simp] lemma iterated_deriv_one_zero : iterated_deriv (1 : polynomial R) 0 = 1 :=
by simp only [iterated_deriv_zero_right]

@[simp] lemma iterated_deriv_one : 0 < n → iterated_deriv (1 : polynomial R) n = 0 := λ h,
begin
  have eq1 : (1 : polynomial R) = C 1 := by simp only [ring_hom.map_one],
  rw eq1, exact iterated_deriv_C _ _ h,
end

end semiring

section ring
variables [ring R] (p q : polynomial R) (n : ℕ)

@[simp] lemma iterated_deriv_neg : iterated_deriv (-p) n = - iterated_deriv p n :=
begin
  induction n with n ih,
  { simp only [iterated_deriv_zero_right] },
  { simp only [iterated_deriv_succ, ih, derivative_neg] }
end

@[simp] lemma iterated_deriv_sub :
  iterated_deriv (p - q) n = iterated_deriv p n - iterated_deriv q n :=
by rw [sub_eq_add_neg, iterated_deriv_add, iterated_deriv_neg, ←sub_eq_add_neg]

end ring

section comm_semiring
variable [comm_semiring R]
variables (f p q : polynomial R) (n k : ℕ)

lemma coeff_iterated_deriv_as_prod_Ico :
  ∀ m : ℕ, (iterated_deriv f k).coeff m = (∏ i in Ico m.succ (m + k.succ), i) * (f.coeff (m+k)) :=
begin
  induction k with k ih,
  { simp only [add_zero, forall_const, one_mul, Ico_self, eq_self_iff_true,
      iterated_deriv_zero_right, prod_empty] },
  { intro m, rw [iterated_deriv_succ, coeff_derivative, ih (m+1), mul_right_comm],
    apply congr_arg2,
    { have set_eq : (Ico m.succ (m + k.succ.succ)) = (Ico (m + 1).succ (m + 1 + k.succ)) ∪ {m+1},
      { rw [union_comm, ←insert_eq, Ico_insert_succ_left, add_succ, add_succ, add_succ _ k,
            ←succ_eq_add_one, succ_add],
        rw succ_eq_add_one,
        linarith },
      rw [set_eq, prod_union],
      apply congr_arg2,
      { refl },
      { simp only [prod_singleton], norm_cast },
      { rw [disjoint_singleton_right, mem_Ico],
        exact λ h, (nat.lt_succ_self _).not_le h.1 } },
    { exact congr_arg _ (succ_add m k) } },
end

lemma coeff_iterated_deriv_as_prod_range :
  ∀ m : ℕ, (iterated_deriv f k).coeff m = f.coeff (m + k) * (∏ i in range k, ↑(m + k - i)) :=
begin
  induction k with k ih,
  { simp },
  intro m,
  calc (f.iterated_deriv k.succ).coeff m
      = f.coeff (m + k.succ) * (∏ i in range k, ↑(m + k.succ - i)) * (m + 1) :
    by rw [iterated_deriv_succ, coeff_derivative, ih m.succ, succ_add, add_succ]
  ... = f.coeff (m + k.succ) * (∏ i in range k, ↑(m + k.succ - i)) * ↑(m + 1) :
    by push_cast
  ... = f.coeff (m + k.succ) * (∏ i in range k.succ, ↑(m + k.succ - i)) :
    by rw [prod_range_succ, add_tsub_assoc_of_le k.le_succ, succ_sub le_rfl, tsub_self, mul_assoc]
end

lemma iterated_deriv_eq_zero_of_nat_degree_lt (h : f.nat_degree < n) : iterated_deriv f n = 0 :=
begin
  ext m,
  rw [coeff_iterated_deriv_as_prod_range, coeff_zero, coeff_eq_zero_of_nat_degree_lt, zero_mul],
  linarith
end

lemma iterated_deriv_mul :
  iterated_deriv (p * q) n =
  ∑ k in range n.succ,
    (C (n.choose k : R)) * iterated_deriv p (n - k) * iterated_deriv q k :=
begin
  induction n with n IH,
  { simp },

  calc (p * q).iterated_deriv n.succ
      = (∑ (k : ℕ) in range n.succ,
           C ↑(n.choose k) * p.iterated_deriv (n - k) * q.iterated_deriv k).derivative :
    by rw [iterated_deriv_succ, IH]
  ... = ∑ (k : ℕ) in range n.succ,
          C ↑(n.choose k) * p.iterated_deriv (n - k + 1) * q.iterated_deriv k +
        ∑ (k : ℕ) in range n.succ,
          C ↑(n.choose k) * p.iterated_deriv (n - k) * q.iterated_deriv (k + 1) :
    by simp_rw [derivative_sum, derivative_mul, derivative_C, zero_mul, zero_add,
                iterated_deriv_succ, sum_add_distrib]
  ... = (∑ (k : ℕ) in range n.succ,
            C ↑(n.choose k.succ) * p.iterated_deriv (n - k) * q.iterated_deriv (k + 1) +
          C ↑1 * p.iterated_deriv n.succ * q.iterated_deriv 0) +
        ∑ (k : ℕ) in range n.succ,
          C ↑(n.choose k) * p.iterated_deriv (n - k) * q.iterated_deriv (k + 1) : _
  ... = ∑ (k : ℕ) in range n.succ,
          C ↑(n.choose k) * p.iterated_deriv (n - k) * q.iterated_deriv (k + 1) +
        ∑ (k : ℕ) in range n.succ,
            C ↑(n.choose k.succ) * p.iterated_deriv (n - k) * q.iterated_deriv (k + 1) +
        C ↑1 * p.iterated_deriv n.succ * q.iterated_deriv 0 :
    by ring
  ... = ∑ (i : ℕ) in range n.succ,
          C ↑((n+1).choose (i+1)) * p.iterated_deriv (n + 1 - (i+1)) * q.iterated_deriv (i+1) +
        C ↑1 * p.iterated_deriv n.succ * q.iterated_deriv 0 :
    by simp_rw [choose_succ_succ, succ_sub_succ, cast_add, C.map_add, add_mul, sum_add_distrib]
  ... = ∑ (k : ℕ) in range n.succ.succ,
          C ↑(n.succ.choose k) * p.iterated_deriv (n.succ - k) * q.iterated_deriv k :
    by rw [sum_range_succ' _ n.succ, choose_zero_right, tsub_zero],

  congr,
  refine (sum_range_succ' _ _).trans (congr_arg2 (+) _ _),
  { rw [sum_range_succ, nat.choose_succ_self, cast_zero, C.map_zero, zero_mul, zero_mul, add_zero],
    refine sum_congr rfl (λ k hk, _),
    rw mem_range at hk,
    congr,
    rw [tsub_add_eq_add_tsub (nat.succ_le_of_lt hk), nat.succ_sub_succ] },
  { rw [choose_zero_right, tsub_zero] },
end

end comm_semiring

end polynomial

author: jjaassoonn


import ..lectures.love05_inductive_predicates_demo
import ..lectures.love13_rational_and_real_numbers_demo

/-! # LoVe Exercise 13: Rational and Real Numbers -/

set_option pp.beta true
set_option pp.generalized_field_notation false

namespace LoVe

/-! ## Question 1: Rationals

1.1. Prove the following lemma.

Hint: The lemma `fraction.mk.inj_eq` might be useful. -/

#check fraction.mk.inj_eq

lemma fraction.ext (a b : fraction) (hnum : fraction.num a = fraction.num b)
    (hdenom : fraction.denom a = fraction.denom b) :
  a = b :=
sorry

/-! 1.2. Extending the `fraction.has_mul` instance from the lecture, declare
`fraction` as an instance of `semigroup`.

Hint: Use the lemma `fraction.ext` above, and possibly `fraction.mul_num`, and
`fraction.mul_denom`. -/

#check fraction.ext
#check fraction.mul_num
#check fraction.mul_denom

@[instance] def fraction.semigroup : semigroup fraction :=
{ mul_assoc :=
    sorry,
  ..fraction.has_mul }

/-! 1.3. Extending the `rat.has_mul` instance from the lecture, declare `rat` as
an instance of `semigroup`. -/

@[instance] def rat.semigroup : semigroup rat :=
{ mul_assoc :=
    sorry,
  ..rat.has_mul }

end LoVe


text:
/-
Copyright (c) 2018 Robert Y. Lewis. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Robert Y. Lewis, Mario Carneiro, Johan Commelin
-/
import data.int.modeq
import data.zmod.basic
import linear_algebra.adic_completion
import data.padics.padic_numbers
import ring_theory.discrete_valuation_ring
import topology.metric_space.cau_seq_filter

/-!
# p-adic integers

This file defines the p-adic integers `ℤ_p` as the subtype of `ℚ_p` with norm `≤ 1`.
We show that `ℤ_p`
* is complete
* is nonarchimedean
* is a normed ring
* is a local ring
* is a discrete valuation ring

The relation between `ℤ_[p]` and `zmod p` is established in another file.

## Important definitions

* `padic_int` : the type of p-adic numbers

## Notation

We introduce the notation `ℤ_[p]` for the p-adic integers.

## Implementation notes

Much, but not all, of this file assumes that `p` is prime. This assumption is inferred automatically
by taking `[fact (nat.prime p)] as a type class argument.

Coercions into `ℤ_p` are set up to work with the `norm_cast` tactic.

## References

* [F. Q. Gouêva, *p-adic numbers*][gouvea1997]
* [R. Y. Lewis, *A formal proof of Hensel's lemma over the p-adic integers*][lewis2019]
* <https://en.wikipedia.org/wiki/P-adic_number>

## Tags

p-adic, p adic, padic, p-adic integer
-/

open nat padic metric local_ring
noncomputable theory
open_locale classical

/-- The p-adic integers ℤ_p are the p-adic numbers with norm ≤ 1. -/
def padic_int (p : ℕ) [fact p.prime] := {x : ℚ_[p] // ∥x∥ ≤ 1}
notation `ℤ_[`p`]` := padic_int p

namespace padic_int
/-! ### Ring structure and coercion to `ℚ_[p]` -/
variables {p : ℕ} [fact p.prime]

instance : has_coe ℤ_[p] ℚ_[p] := ⟨subtype.val⟩

lemma ext {x y : ℤ_[p]} : (x : ℚ_[p]) = y → x = y := subtype.ext_iff_val.2

/-- Addition on ℤ_p is inherited from ℚ_p. -/
instance : has_add ℤ_[p] :=
⟨λ ⟨x, hx⟩ ⟨y, hy⟩, ⟨x+y,
    le_trans (padic_norm_e.nonarchimedean _ _) (max_le_iff.2 ⟨hx,hy⟩)⟩⟩

/-- Multiplication on ℤ_p is inherited from ℚ_p. -/
instance : has_mul ℤ_[p] :=
⟨λ ⟨x, hx⟩ ⟨y, hy⟩, ⟨x*y,
    begin rw padic_norm_e.mul, apply mul_le_one; {assumption <|> apply norm_nonneg} end⟩⟩

/-- Negation on ℤ_p is inherited from ℚ_p. -/
instance : has_neg ℤ_[p] :=
⟨λ ⟨x, hx⟩, ⟨-x, by simpa⟩⟩

/-- Subtraction on ℤ_p is inherited from ℚ_p. -/
instance : has_sub ℤ_[p] :=
⟨λ ⟨x, hx⟩ ⟨y, hy⟩, ⟨x - y,
  by { rw sub_eq_add_neg, rw ← norm_neg at hy,
       exact le_trans (padic_norm_e.nonarchimedean _ _) (max_le_iff.2 ⟨hx, hy⟩) }⟩⟩

/-- Zero on ℤ_p is inherited from ℚ_p. -/
instance : has_zero ℤ_[p] :=
⟨⟨0, by norm_num⟩⟩

instance : inhabited ℤ_[p] := ⟨0⟩

/-- One on ℤ_p is inherited from ℚ_p. -/
instance : has_one ℤ_[p] :=
⟨⟨1, by norm_num⟩⟩

@[simp] lemma mk_zero {h} : (⟨0, h⟩ : ℤ_[p]) = (0 : ℤ_[p]) := rfl

@[simp] lemma val_eq_coe (z : ℤ_[p]) : z.val = z := rfl

@[simp, norm_cast] lemma coe_add : ∀ (z1 z2 : ℤ_[p]), ((z1 + z2 : ℤ_[p]) : ℚ_[p]) = z1 + z2
| ⟨_, _⟩ ⟨_, _⟩ := rfl

@[simp, norm_cast] lemma coe_mul : ∀ (z1 z2 : ℤ_[p]), ((z1 * z2 : ℤ_[p]) : ℚ_[p]) = z1 * z2
| ⟨_, _⟩ ⟨_, _⟩ := rfl

@[simp, norm_cast] lemma coe_neg : ∀ (z1 : ℤ_[p]), ((-z1 : ℤ_[p]) : ℚ_[p]) = -z1
| ⟨_, _⟩ := rfl

@[simp, norm_cast] lemma coe_sub : ∀ (z1 z2 : ℤ_[p]), ((z1 - z2 : ℤ_[p]) : ℚ_[p]) = z1 - z2
| ⟨_, _⟩ ⟨_, _⟩ := rfl

@[simp, norm_cast] lemma coe_one : ((1 : ℤ_[p]) : ℚ_[p]) = 1 := rfl

@[simp, norm_cast] lemma coe_coe : ∀ n : ℕ, ((n : ℤ_[p]) : ℚ_[p]) = n
| 0 := rfl
| (k+1) := by simp [coe_coe]

@[simp, norm_cast] lemma coe_coe_int : ∀ (z : ℤ), ((z : ℤ_[p]) : ℚ_[p]) = z
| (int.of_nat n) := by simp
| -[1+n] := by simp

@[simp, norm_cast] lemma coe_zero : ((0 : ℤ_[p]) : ℚ_[p]) = 0 := rfl

instance : ring ℤ_[p] :=
by refine_struct
{ add   := (+),
  mul   := (*),
  neg   := has_neg.neg,
  zero  := (0 : ℤ_[p]),
  one   := 1,
  sub   := has_sub.sub,
  npow  := @npow_rec _ ⟨1⟩ ⟨(*)⟩,
  nsmul := @nsmul_rec _ ⟨0⟩ ⟨(+)⟩,
  gsmul := @gsmul_rec _ ⟨0⟩ ⟨(+)⟩ ⟨has_neg.neg⟩ };
intros; try { refl }; ext; simp; ring

/-- The coercion from ℤ[p] to ℚ[p] as a ring homomorphism. -/
def coe.ring_hom : ℤ_[p] →+* ℚ_[p]  :=
{ to_fun := (coe : ℤ_[p] → ℚ_[p]),
  map_zero' := rfl,
  map_one' := rfl,
  map_mul' := coe_mul,
  map_add' := coe_add }

@[simp, norm_cast] lemma coe_pow (x : ℤ_[p]) (n : ℕ) : (↑(x^n) : ℚ_[p]) = (↑x : ℚ_[p])^n :=
coe.ring_hom.map_pow x n

@[simp] lemma mk_coe : ∀ (k : ℤ_[p]), (⟨k, k.2⟩ : ℤ_[p]) = k
| ⟨_, _⟩ := rfl

/-- The inverse of a p-adic integer with norm equal to 1 is also a p-adic integer. Otherwise, the
inverse is defined to be 0. -/
def inv : ℤ_[p] → ℤ_[p]
| ⟨k, _⟩ := if h : ∥k∥ = 1 then ⟨1/k, by simp [h]⟩ else 0

instance : char_zero ℤ_[p] :=
{ cast_injective :=
  λ m n h, cast_injective $
  show (m:ℚ_[p]) = n, by { rw subtype.ext_iff at h, norm_cast at h, exact h } }

@[simp, norm_cast] lemma coe_int_eq (z1 z2 : ℤ) : (z1 : ℤ_[p]) = z2 ↔ z1 = z2 :=
suffices (z1 : ℚ_[p]) = z2 ↔ z1 = z2, from iff.trans (by norm_cast) this,
by norm_cast

/--
A sequence of integers that is Cauchy with respect to the `p`-adic norm
converges to a `p`-adic integer.
-/
def of_int_seq (seq : ℕ → ℤ) (h : is_cau_seq (padic_norm p) (λ n, seq n)) : ℤ_[p] :=
⟨⟦⟨_, h⟩⟧,
 show ↑(padic_seq.norm _) ≤ (1 : ℝ), begin
   rw padic_seq.norm,
   split_ifs with hne; norm_cast,
   { exact zero_le_one },
   { apply padic_norm.of_int }
 end ⟩

end padic_int

namespace padic_int
/-!
### Instances

We now show that `ℤ_[p]` is a
* complete metric space
* normed ring
* integral domain
-/

variables (p : ℕ) [fact p.prime]

instance : metric_space ℤ_[p] := subtype.metric_space

instance complete_space : complete_space ℤ_[p] :=
have is_closed {x : ℚ_[p] | ∥x∥ ≤ 1}, from is_closed_le continuous_norm continuous_const,
this.complete_space_coe

instance : has_norm ℤ_[p] := ⟨λ z, ∥(z : ℚ_[p])∥⟩

variables {p}

protected lemma mul_comm : ∀ z1 z2 : ℤ_[p], z1*z2 = z2*z1
| ⟨q1, h1⟩ ⟨q2, h2⟩ := show (⟨q1*q2, _⟩ : ℤ_[p]) = ⟨q2*q1, _⟩, by simp [_root_.mul_comm]

protected lemma zero_ne_one : (0 : ℤ_[p]) ≠ 1 :=
show (⟨(0 : ℚ_[p]), _⟩ : ℤ_[p]) ≠ ⟨(1 : ℚ_[p]), _⟩, from mt subtype.ext_iff_val.1 zero_ne_one

protected lemma eq_zero_or_eq_zero_of_mul_eq_zero :
          ∀ (a b : ℤ_[p]), a * b = 0 → a = 0 ∨ b = 0
| ⟨a, ha⟩ ⟨b, hb⟩ := λ h : (⟨a * b, _⟩ : ℤ_[p]) = ⟨0, _⟩,
have a * b = 0, from subtype.ext_iff_val.1 h,
(mul_eq_zero.1 this).elim
  (λ h1, or.inl (by simp [h1]; refl))
  (λ h2, or.inr (by simp [h2]; refl))

lemma norm_def {z : ℤ_[p]} : ∥z∥ = ∥(z : ℚ_[p])∥ := rfl

variables (p)

instance : normed_comm_ring ℤ_[p] :=
{ dist_eq := λ ⟨_, _⟩ ⟨_, _⟩, rfl,
  norm_mul := λ ⟨_, _⟩ ⟨_, _⟩, norm_mul_le _ _,
  mul_comm := padic_int.mul_comm }

instance : norm_one_class ℤ_[p] := ⟨norm_def.trans norm_one⟩

instance is_absolute_value : is_absolute_value (λ z : ℤ_[p], ∥z∥) :=
{ abv_nonneg := norm_nonneg,
  abv_eq_zero := λ ⟨_, _⟩, by simp [norm_eq_zero],
  abv_add := λ ⟨_,_⟩ ⟨_, _⟩, norm_add_le _ _,
  abv_mul := λ _ _, by simp only [norm_def, padic_norm_e.mul, padic_int.coe_mul]}

variables {p}

instance : integral_domain ℤ_[p] :=
{ eq_zero_or_eq_zero_of_mul_eq_zero := λ x y, padic_int.eq_zero_or_eq_zero_of_mul_eq_zero x y,
  exists_pair_ne := ⟨0, 1, padic_int.zero_ne_one⟩,
  .. padic_int.normed_comm_ring p }

end padic_int

namespace padic_int
/-! ### Norm -/
variables {p : ℕ} [fact p.prime]

lemma norm_le_one : ∀ z : ℤ_[p], ∥z∥ ≤ 1
| ⟨_, h⟩ := h

@[simp] lemma norm_mul (z1 z2 : ℤ_[p]) : ∥z1 * z2∥ = ∥z1∥ * ∥z2∥ :=
by simp [norm_def]

@[simp] lemma norm_pow (z : ℤ_[p]) : ∀ n : ℕ, ∥z^n∥ = ∥z∥^n
| 0 := by simp
| (k+1) := by { rw [pow_succ, pow_succ, norm_mul], congr, apply norm_pow }

theorem nonarchimedean : ∀ (q r : ℤ_[p]), ∥q + r∥ ≤ max (∥q∥) (∥r∥)
| ⟨_, _⟩ ⟨_, _⟩ := padic_norm_e.nonarchimedean _ _

theorem norm_add_eq_max_of_ne : ∀ {q r : ℤ_[p]}, ∥q∥ ≠ ∥r∥ → ∥q+r∥ = max (∥q∥) (∥r∥)
| ⟨_, _⟩ ⟨_, _⟩ := padic_norm_e.add_eq_max_of_ne

lemma norm_eq_of_norm_add_lt_right {z1 z2 : ℤ_[p]}
  (h : ∥z1 + z2∥ < ∥z2∥) : ∥z1∥ = ∥z2∥ :=
by_contradiction $ λ hne,
  not_lt_of_ge (by rw norm_add_eq_max_of_ne hne; apply le_max_right) h

lemma norm_eq_of_norm_add_lt_left {z1 z2 : ℤ_[p]}
  (h : ∥z1 + z2∥ < ∥z1∥) : ∥z1∥ = ∥z2∥ :=
by_contradiction $ λ hne,
  not_lt_of_ge (by rw norm_add_eq_max_of_ne hne; apply le_max_left) h

@[simp] lemma padic_norm_e_of_padic_int (z : ℤ_[p]) : ∥(↑z : ℚ_[p])∥ = ∥z∥ :=
by simp [norm_def]

lemma norm_int_cast_eq_padic_norm (z : ℤ) : ∥(z : ℤ_[p])∥ = ∥(z : ℚ_[p])∥ :=
by simp [norm_def]

@[simp] lemma norm_eq_padic_norm {q : ℚ_[p]} (hq : ∥q∥ ≤ 1) :
  @norm ℤ_[p] _ ⟨q, hq⟩ = ∥q∥ := rfl

@[simp] lemma norm_p : ∥(p : ℤ_[p])∥ = p⁻¹ :=
show ∥((p : ℤ_[p]) : ℚ_[p])∥ = p⁻¹, by exact_mod_cast padic_norm_e.norm_p

@[simp] lemma norm_p_pow (n : ℕ) : ∥(p : ℤ_[p])^n∥ = p^(-n:ℤ) :=
show ∥((p^n : ℤ_[p]) : ℚ_[p])∥ = p^(-n:ℤ),
by { convert padic_norm_e.norm_p_pow n, simp, }

private def cau_seq_to_rat_cau_seq (f : cau_seq ℤ_[p] norm) :
  cau_seq ℚ_[p] (λ a, ∥a∥) :=
⟨ λ n, f n,
  λ _ hε, by simpa [norm, norm_def] using f.cauchy hε ⟩

variables (p)

instance complete : cau_seq.is_complete ℤ_[p] norm :=
⟨ λ f,
  have hqn : ∥cau_seq.lim (cau_seq_to_rat_cau_seq f)∥ ≤ 1,
    from padic_norm_e_lim_le zero_lt_one (λ _, norm_le_one _),
  ⟨ ⟨_, hqn⟩,
    λ ε, by simpa [norm, norm_def] using cau_seq.equiv_lim (cau_seq_to_rat_cau_seq f) ε⟩⟩

end padic_int

namespace padic_int

variables (p : ℕ) [hp_prime : fact p.prime]
include hp_prime

lemma exists_pow_neg_lt {ε : ℝ} (hε : 0 < ε) :
  ∃ (k : ℕ), ↑p ^ -((k : ℕ) : ℤ) < ε :=
begin
  obtain ⟨k, hk⟩ := exists_nat_gt ε⁻¹,
  use k,
  rw ← inv_lt_inv hε (_root_.fpow_pos_of_pos _ _),
  { rw [fpow_neg, inv_inv', gpow_coe_nat],
    apply lt_of_lt_of_le hk,
    norm_cast,
    apply le_of_lt,
    convert nat.lt_pow_self _ _ using 1,
    exact hp_prime.1.one_lt },
  { exact_mod_cast hp_prime.1.pos }
end

lemma exists_pow_neg_lt_rat {ε : ℚ} (hε : 0 < ε) :
  ∃ (k : ℕ), ↑p ^ -((k : ℕ) : ℤ) < ε :=
begin
  obtain ⟨k, hk⟩ := @exists_pow_neg_lt p _ ε (by exact_mod_cast hε),
  use k,
  rw (show (p : ℝ) = (p : ℚ), by simp) at hk,
  exact_mod_cast hk
end

variable {p}

lemma norm_int_lt_one_iff_dvd (k : ℤ) : ∥(k : ℤ_[p])∥ < 1 ↔ ↑p ∣ k :=
suffices ∥(k : ℚ_[p])∥ < 1 ↔ ↑p ∣ k, by rwa norm_int_cast_eq_padic_norm,
padic_norm_e.norm_int_lt_one_iff_dvd k

lemma norm_int_le_pow_iff_dvd {k : ℤ} {n : ℕ} : ∥(k : ℤ_[p])∥ ≤ ((↑p)^(-n : ℤ)) ↔ ↑p^n ∣ k :=
suffices ∥(k : ℚ_[p])∥ ≤ ((↑p)^(-n : ℤ)) ↔ ↑(p^n) ∣ k, by simpa [norm_int_cast_eq_padic_norm],
padic_norm_e.norm_int_le_pow_iff_dvd _ _

/-! ### Valuation on `ℤ_[p]` -/

/-- `padic_int.valuation` lifts the p-adic valuation on `ℚ` to `ℤ_[p]`.  -/
def valuation (x : ℤ_[p]) := padic.valuation (x : ℚ_[p])

lemma norm_eq_pow_val {x : ℤ_[p]} (hx : x ≠ 0) :
  ∥x∥ = p^(-x.valuation) :=
begin
  convert padic.norm_eq_pow_val _,
  contrapose! hx,
  exact subtype.val_injective hx
end

@[simp] lemma valuation_zero : valuation (0 : ℤ_[p]) = 0 :=
padic.valuation_zero

@[simp] lemma valuation_one : valuation (1 : ℤ_[p]) = 0 :=
padic.valuation_one

@[simp] lemma valuation_p : valuation (p : ℤ_[p]) = 1 :=
by simp [valuation, -cast_eq_of_rat_of_nat]

lemma valuation_nonneg (x : ℤ_[p]) : 0 ≤ x.valuation :=
begin
  by_cases hx : x = 0,
  { simp [hx] },
  have h : (1 : ℝ) < p := by exact_mod_cast hp_prime.1.one_lt,
  rw [← neg_nonpos, ← (fpow_strict_mono h).le_iff_le],
  show (p : ℝ) ^ -valuation x ≤ p ^ 0,
  rw [← norm_eq_pow_val hx],
  simpa using x.property,
end

@[simp] lemma valuation_p_pow_mul (n : ℕ) (c : ℤ_[p]) (hc : c ≠ 0) :
  (↑p ^ n * c).valuation = n + c.valuation :=
begin
  have : ∥↑p ^ n * c∥ = ∥(p ^ n : ℤ_[p])∥ * ∥c∥,
  { exact norm_mul _ _ },
  have aux : ↑p ^ n * c ≠ 0,
  { contrapose! hc, rw mul_eq_zero at hc, cases hc,
    { refine (hp_prime.1.ne_zero _).elim,
      exact_mod_cast (pow_eq_zero hc) },
    { exact hc } },
  rwa [norm_eq_pow_val aux, norm_p_pow, norm_eq_pow_val hc,
      ← fpow_add, ← neg_add, fpow_inj, neg_inj] at this,
  { exact_mod_cast hp_prime.1.pos },
  { exact_mod_cast hp_prime.1.ne_one },
  { exact_mod_cast hp_prime.1.ne_zero },
end

section units
/-! ### Units of `ℤ_[p]` -/

local attribute [reducible] padic_int

lemma mul_inv : ∀ {z : ℤ_[p]}, ∥z∥ = 1 → z * z.inv = 1
| ⟨k, _⟩ h :=
  begin
    have hk : k ≠ 0, from λ h', @zero_ne_one ℚ_[p] _ _ (by simpa [h'] using h),
    unfold padic_int.inv, split_ifs,
    { change (⟨k * (1/k), _⟩ : ℤ_[p]) = 1,
      simp [hk], refl },
    { apply subtype.ext_iff_val.2, simp [mul_inv_cancel hk] }
  end

lemma inv_mul {z : ℤ_[p]} (hz : ∥z∥ = 1) : z.inv * z = 1 :=
by rw [mul_comm, mul_inv hz]

lemma is_unit_iff {z : ℤ_[p]} : is_unit z ↔ ∥z∥ = 1 :=
⟨λ h, begin
  rcases is_unit_iff_dvd_one.1 h with ⟨w, eq⟩,
  refine le_antisymm (norm_le_one _) _,
  have := mul_le_mul_of_nonneg_left (norm_le_one w) (norm_nonneg z),
  rwa [mul_one, ← norm_mul, ← eq, norm_one] at this
end, λ h, ⟨⟨z, z.inv, mul_inv h, inv_mul h⟩, rfl⟩⟩

lemma norm_lt_one_add {z1 z2 : ℤ_[p]} (hz1 : ∥z1∥ < 1) (hz2 : ∥z2∥ < 1) : ∥z1 + z2∥ < 1 :=
lt_of_le_of_lt (nonarchimedean _ _) (max_lt hz1 hz2)

lemma norm_lt_one_mul {z1 z2 : ℤ_[p]} (hz2 : ∥z2∥ < 1) : ∥z1 * z2∥ < 1 :=
calc  ∥z1 * z2∥ = ∥z1∥ * ∥z2∥ : by simp
           ... < 1 : mul_lt_one_of_nonneg_of_lt_one_right (norm_le_one _) (norm_nonneg _) hz2

@[simp] lemma mem_nonunits {z : ℤ_[p]} : z ∈ nonunits ℤ_[p] ↔ ∥z∥ < 1 :=
by rw lt_iff_le_and_ne; simp [norm_le_one z, nonunits, is_unit_iff]

/-- A `p`-adic number `u` with `∥u∥ = 1` is a unit of `ℤ_[p]`. -/
def mk_units {u : ℚ_[p]} (h : ∥u∥ = 1) : units ℤ_[p] :=
let z : ℤ_[p] := ⟨u, le_of_eq h⟩ in ⟨z, z.inv, mul_inv h, inv_mul h⟩

@[simp]
lemma mk_units_eq {u : ℚ_[p]} (h : ∥u∥ = 1) : ((mk_units h : ℤ_[p]) : ℚ_[p]) = u :=
rfl

@[simp] lemma norm_units (u : units ℤ_[p]) : ∥(u : ℤ_[p])∥ = 1 :=
is_unit_iff.mp $ by simp

/-- `unit_coeff hx` is the unit `u` in the unique representation `x = u * p ^ n`.
See `unit_coeff_spec`. -/
def unit_coeff {x : ℤ_[p]} (hx : x ≠ 0) : units ℤ_[p] :=
let u : ℚ_[p] := x*p^(-x.valuation) in
have hu : ∥u∥ = 1,
by simp [hx, nat.fpow_ne_zero_of_pos (by exact_mod_cast hp_prime.1.pos) x.valuation,
         norm_eq_pow_val, fpow_neg, inv_mul_cancel, -cast_eq_of_rat_of_nat],
mk_units hu

@[simp] lemma unit_coeff_coe {x : ℤ_[p]} (hx : x ≠ 0) :
  (unit_coeff hx : ℚ_[p]) = x * p ^ (-x.valuation) := rfl

lemma unit_coeff_spec {x : ℤ_[p]} (hx : x ≠ 0) :
  x = (unit_coeff hx : ℤ_[p]) * p ^ int.nat_abs (valuation x) :=
begin
  apply subtype.coe_injective,
  push_cast,
  have repr : (x : ℚ_[p]) = (unit_coeff hx) * p ^ x.valuation,
  { rw [unit_coeff_coe, mul_assoc, ← fpow_add],
    { simp },
    { exact_mod_cast hp_prime.1.ne_zero } },
  convert repr using 2,
  rw [← gpow_coe_nat, int.nat_abs_of_nonneg (valuation_nonneg x)],
end

end units

section norm_le_iff
/-! ### Various characterizations of open unit balls -/

lemma norm_le_pow_iff_le_valuation (x : ℤ_[p]) (hx : x ≠ 0) (n : ℕ) :
  ∥x∥ ≤ p ^ (-n : ℤ) ↔ ↑n ≤ x.valuation :=
begin
  rw norm_eq_pow_val hx,
  lift x.valuation to ℕ using x.valuation_nonneg with k hk,
  simp only [int.coe_nat_le, fpow_neg, gpow_coe_nat],
  have aux : ∀ n : ℕ, 0 < (p ^ n : ℝ),
  { apply pow_pos, exact_mod_cast hp_prime.1.pos },
  rw [inv_le_inv (aux _) (aux _)],
  have : p ^ n ≤ p ^ k ↔ n ≤ k := (pow_right_strict_mono hp_prime.1.two_le).le_iff_le,
  rw [← this],
  norm_cast,
end

lemma mem_span_pow_iff_le_valuation (x : ℤ_[p]) (hx : x ≠ 0) (n : ℕ) :
  x ∈ (ideal.span {p ^ n} : ideal ℤ_[p]) ↔ ↑n ≤ x.valuation :=
begin
  rw [ideal.mem_span_singleton],
  split,
  { rintro ⟨c, rfl⟩,
    suffices : c ≠ 0,
    { rw [valuation_p_pow_mul _ _ this, le_add_iff_nonneg_right], apply valuation_nonneg, },
    contrapose! hx, rw [hx, mul_zero], },
  { rw [unit_coeff_spec hx] { occs := occurrences.pos [2] },
    lift x.valuation to ℕ using x.valuation_nonneg with k hk,
    simp only [int.nat_abs_of_nat, units.is_unit, is_unit.dvd_mul_left, int.coe_nat_le],
    intro H,
    obtain ⟨k, rfl⟩ := nat.exists_eq_add_of_le H,
    simp only [pow_add, dvd_mul_right], }
end

lemma norm_le_pow_iff_mem_span_pow (x : ℤ_[p]) (n : ℕ) :
  ∥x∥ ≤ p ^ (-n : ℤ) ↔ x ∈ (ideal.span {p ^ n} : ideal ℤ_[p]) :=
begin
  by_cases hx : x = 0,
  { subst hx,
    simp only [norm_zero, fpow_neg, gpow_coe_nat, inv_nonneg, iff_true, submodule.zero_mem],
    exact_mod_cast nat.zero_le _ },
  rw [norm_le_pow_iff_le_valuation x hx, mem_span_pow_iff_le_valuation x hx],
end

lemma norm_le_pow_iff_norm_lt_pow_add_one (x : ℤ_[p]) (n : ℤ) :
  ∥x∥ ≤ p ^ n ↔ ∥x∥ < p ^ (n + 1) :=
begin
  have aux : ∀ n : ℤ, 0 < (p ^ n : ℝ),
  { apply nat.fpow_pos_of_pos, exact hp_prime.1.pos },
  by_cases hx0 : x = 0, { simp [hx0, norm_zero, aux, le_of_lt (aux _)], },
  rw norm_eq_pow_val hx0,
  have h1p : 1 < (p : ℝ), { exact_mod_cast hp_prime.1.one_lt },
  have H := fpow_strict_mono h1p,
  rw [H.le_iff_le, H.lt_iff_lt, int.lt_add_one_iff],
end

lemma norm_lt_pow_iff_norm_le_pow_sub_one (x : ℤ_[p]) (n : ℤ) :
  ∥x∥ < p ^ n ↔ ∥x∥ ≤ p ^ (n - 1) :=
by rw [norm_le_pow_iff_norm_lt_pow_add_one, sub_add_cancel]

lemma norm_lt_one_iff_dvd (x : ℤ_[p]) : ∥x∥ < 1 ↔ ↑p ∣ x :=
begin
  have := norm_le_pow_iff_mem_span_pow x 1,
  rw [ideal.mem_span_singleton, pow_one] at this,
  rw [← this, norm_le_pow_iff_norm_lt_pow_add_one],
  simp only [gpow_zero, int.coe_nat_zero, int.coe_nat_succ, add_left_neg, zero_add],
end

@[simp] lemma pow_p_dvd_int_iff (n : ℕ) (a : ℤ) : (p ^ n : ℤ_[p]) ∣ a ↔ ↑p ^ n ∣ a :=
by rw [← norm_int_le_pow_iff_dvd, norm_le_pow_iff_mem_span_pow, ideal.mem_span_singleton]

end norm_le_iff

section dvr
/-! ### Discrete valuation ring -/

instance : local_ring ℤ_[p] :=
local_of_nonunits_ideal zero_ne_one $ λ x y, by simp; exact norm_lt_one_add

lemma p_nonnunit : (p : ℤ_[p]) ∈ nonunits ℤ_[p] :=
have (p : ℝ)⁻¹ < 1, from inv_lt_one $ by exact_mod_cast hp_prime.1.one_lt,
by simp [this]

lemma maximal_ideal_eq_span_p : maximal_ideal ℤ_[p] = ideal.span {p} :=
begin
  apply le_antisymm,
  { intros x hx,
    rw ideal.mem_span_singleton,
    simp only [local_ring.mem_maximal_ideal, mem_nonunits] at hx,
    rwa ← norm_lt_one_iff_dvd, },
  { rw [ideal.span_le, set.singleton_subset_iff], exact p_nonnunit }
end

lemma prime_p : prime (p : ℤ_[p]) :=
begin
  rw [← ideal.span_singleton_prime, ← maximal_ideal_eq_span_p],
  { apply_instance },
  { exact_mod_cast hp_prime.1.ne_zero }
end

lemma irreducible_p : irreducible (p : ℤ_[p]) :=
irreducible_of_prime prime_p

instance : discrete_valuation_ring ℤ_[p] :=
discrete_valuation_ring.of_has_unit_mul_pow_irreducible_factorization
⟨p, irreducible_p, λ x hx, ⟨x.valuation.nat_abs, unit_coeff hx,
  by rw [mul_comm, ← unit_coeff_spec hx]⟩⟩

lemma ideal_eq_span_pow_p {s : ideal ℤ_[p]} (hs : s ≠ ⊥) :
  ∃ n : ℕ, s = ideal.span {p ^ n} :=
discrete_valuation_ring.ideal_eq_span_pow_irreducible hs irreducible_p

end dvr

end padic_int