internlm/Lean-Github huggingface dataset:
Theorem: KummersLemma.mem_adjoin_polyRoot
Proof state before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁴ : Field K
inst✝³ : NumberField K
inst✝² : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
α : L
e : α ^ ↑p = (algebraMap K L) ((algebraMap (𝓞 K) K) ↑u)
i : ℕ
⊢ α ∈ Algebra.adjoin K {↑(polyRoot hp hζ u hcong α e i)}
Tactic:
conv_lhs => rw [polyRoot_spec hp hζ u hcong α e i]
Proof state after:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁴ : Field K
inst✝³ : NumberField K
inst✝² : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
α : L
e : α ^ ↑p = (algebraMap K L) ((algebraMap (𝓞 K) K) ↑u)
i : ℕ
⊢ (ζ ^ i)⁻¹ • (1 - (ζ - 1) • ↑(polyRoot hp hζ u hcong α e i)) ∈ Algebra.adjoin K {↑(polyRoot hp hζ u hcong α e i)}
Theorem: KummersLemma.mem_adjoin_polyRoot
Proof state before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁴ : Field K
inst✝³ : NumberField K
inst✝² : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
α : L
e : α ^ ↑p = (algebraMap K L) ((algebraMap (𝓞 K) K) ↑u)
i : ℕ
⊢ (ζ ^ i)⁻¹ • (1 - (ζ - 1) • ↑(polyRoot hp hζ u hcong α e i)) ∈ Algebra.adjoin K {↑(polyRoot hp hζ u hcong α e i)}
Tactic:
exact Subalgebra.smul_mem _ (sub_mem (one_mem _)
  (Subalgebra.smul_mem _ (Algebra.self_mem_adjoin_singleton K _) _)) _
Proof state after:
no goals
Theorem: KummersLemma.isUnramified
Proof state before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁵ : Field K
inst✝⁴ : NumberField K
inst✝³ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
L : Type u_2
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsSplittingField K L (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
⊢ IsUnramified (𝓞 K) (𝓞 L)
Tactic:
let α := polyRoot hp hζ u hcong _ (rootOfSplitsXPowSubC_pow p.pos _ L) 0
Proof state after:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁵ : Field K
inst✝⁴ : NumberField K
inst✝³ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
L : Type u_2
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsSplittingField K L (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
α : 𝓞 L := polyRoot hp hζ u hcong (rootOfSplitsXPowSubC ⋯ ((algebraMap (𝓞 K) K) ↑u) L) ⋯ 0
⊢ IsUnramified (𝓞 K) (𝓞 L)
Theorem: KummersLemma.isUnramified
Proof state before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁵ : Field K
inst✝⁴ : NumberField K
inst✝³ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
L : Type u_2
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsSplittingField K L (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
α : 𝓞 L := polyRoot hp hζ u hcong (rootOfSplitsXPowSubC ⋯ ((algebraMap (𝓞 K) K) ↑u) L) ⋯ 0
⊢ IsUnramified (𝓞 K) (𝓞 L)
Tactic:
haveI := Polynomial.IsSplittingField.finiteDimensional L (X ^ (p : ℕ) - C (u : K))
Proof state after:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁵ : Field K
inst✝⁴ : NumberField K
inst✝³ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
L : Type u_2
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsSplittingField K L (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
α : 𝓞 L := polyRoot hp hζ u hcong (rootOfSplitsXPowSubC ⋯ ((algebraMap (𝓞 K) K) ↑u) L) ⋯ 0
this : FiniteDimensional K L
⊢ IsUnramified (𝓞 K) (𝓞 L)
Theorem: KummersLemma.isUnramified
Proof state before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁵ : Field K
inst✝⁴ : NumberField K
inst✝³ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
L : Type u_2
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsSplittingField K L (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
α : 𝓞 L := polyRoot hp hζ u hcong (rootOfSplitsXPowSubC ⋯ ((algebraMap (𝓞 K) K) ↑u) L) ⋯ 0
this : FiniteDimensional K L
⊢ IsUnramified (𝓞 K) (𝓞 L)
Tactic:
have hα : Algebra.adjoin K {(α : L)} = ⊤ := by
  rw [eq_top_iff, ← Algebra.adjoin_root_eq_top_of_isSplittingField
    ⟨ζ, (mem_primitiveRoots p.pos).mpr hζ⟩ (X_pow_sub_C_irreducible_of_prime hpri.out hu)
    (rootOfSplitsXPowSubC_pow p.pos (u : K) L), Algebra.adjoin_le_iff, Set.singleton_subset_iff]
  exact mem_adjoin_polyRoot hp hζ u hcong _ _ 0
Proof state after:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁵ : Field K
inst✝⁴ : NumberField K
inst✝³ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
L : Type u_2
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsSplittingField K L (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
α : 𝓞 L := polyRoot hp hζ u hcong (rootOfSplitsXPowSubC ⋯ ((algebraMap (𝓞 K) K) ↑u) L) ⋯ 0
this : FiniteDimensional K L
hα : Algebra.adjoin K {↑α} = ⊤
⊢ IsUnramified (𝓞 K) (𝓞 L)
Theorem: KummersLemma.isUnramified
Proof state before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁵ : Field K
inst✝⁴ : NumberField K
inst✝³ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
L : Type u_2
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsSplittingField K L (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
α : 𝓞 L := polyRoot hp hζ u hcong (rootOfSplitsXPowSubC ⋯ ((algebraMap (𝓞 K) K) ↑u) L) ⋯ 0
this : FiniteDimensional K L
hα : Algebra.adjoin K {↑α} = ⊤
⊢ IsUnramified (𝓞 K) (𝓞 L)
Tactic:
constructor
Proof state after:
case isUnramifiedAt
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁵ : Field K
inst✝⁴ : NumberField K
inst✝³ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
L : Type u_2
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsSplittingField K L (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
α : 𝓞 L := polyRoot hp hζ u hcong (rootOfSplitsXPowSubC ⋯ ((algebraMap (𝓞 K) K) ↑u) L) ⋯ 0
this : FiniteDimensional K L
hα : Algebra.adjoin K {↑α} = ⊤
⊢ ∀ (p : Ideal (𝓞 K)) [inst : p.IsPrime], p ≠ ⊥ → IsUnramifiedAt (𝓞 L) p
Theorem: KummersLemma.isUnramified
Proof state before:
case isUnramifiedAt
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁵ : Field K
inst✝⁴ : NumberField K
inst✝³ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
L : Type u_2
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsSplittingField K L (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
α : 𝓞 L := polyRoot hp hζ u hcong (rootOfSplitsXPowSubC ⋯ ((algebraMap (𝓞 K) K) ↑u) L) ⋯ 0
this : FiniteDimensional K L
hα : Algebra.adjoin K {↑α} = ⊤
⊢ ∀ (p : Ideal (𝓞 K)) [inst : p.IsPrime], p ≠ ⊥ → IsUnramifiedAt (𝓞 L) p
Tactic:
intros I hI hIbot
Proof state after:
case isUnramifiedAt
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁵ : Field K
inst✝⁴ : NumberField K
inst✝³ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
L : Type u_2
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsSplittingField K L (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
α : 𝓞 L := polyRoot hp hζ u hcong (rootOfSplitsXPowSubC ⋯ ((algebraMap (𝓞 K) K) ↑u) L) ⋯ 0
this : FiniteDimensional K L
hα : Algebra.adjoin K {↑α} = ⊤
I : Ideal (𝓞 K)
hI : I.IsPrime
hIbot : I ≠ ⊥
⊢ IsUnramifiedAt (𝓞 L) I
Theorem: KummersLemma.isUnramified
Proof state before:
case isUnramifiedAt
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁵ : Field K
inst✝⁴ : NumberField K
inst✝³ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
L : Type u_2
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsSplittingField K L (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
α : 𝓞 L := polyRoot hp hζ u hcong (rootOfSplitsXPowSubC ⋯ ((algebraMap (𝓞 K) K) ↑u) L) ⋯ 0
this : FiniteDimensional K L
hα : Algebra.adjoin K {↑α} = ⊤
I : Ideal (𝓞 K)
hI : I.IsPrime
hIbot : I ≠ ⊥
⊢ IsUnramifiedAt (𝓞 L) I
Tactic:
refine isUnramifiedAt_of_Separable_minpoly (R := 𝓞 K) K (S := 𝓞 L) L I hIbot α ?_ hα ?_
Proof state after:
case isUnramifiedAt.refine_1
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁵ : Field K
inst✝⁴ : NumberField K
inst✝³ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
L : Type u_2
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsSplittingField K L (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
α : 𝓞 L := polyRoot hp hζ u hcong (rootOfSplitsXPowSubC ⋯ ((algebraMap (𝓞 K) K) ↑u) L) ⋯ 0
this : FiniteDimensional K L
hα : Algebra.adjoin K {↑α} = ⊤
I : Ideal (𝓞 K)
hI : I.IsPrime
hIbot : I ≠ ⊥
⊢ IsIntegral (𝓞 K) ↑α

case isUnramifiedAt.refine_2
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁵ : Field K
inst✝⁴ : NumberField K
inst✝³ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
L : Type u_2
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsSplittingField K L (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
α : 𝓞 L := polyRoot hp hζ u hcong (rootOfSplitsXPowSubC ⋯ ((algebraMap (𝓞 K) K) ↑u) L) ⋯ 0
this : FiniteDimensional K L
hα : Algebra.adjoin K {↑α} = ⊤
I : Ideal (𝓞 K)
hI : I.IsPrime
hIbot : I ≠ ⊥
⊢ (map (Ideal.Quotient.mk I) (minpoly (𝓞 K) ↑α)).Separable
Theorem: KummersLemma.isUnramified
Proof state before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁵ : Field K
inst✝⁴ : NumberField K
inst✝³ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
L : Type u_2
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsSplittingField K L (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
α : 𝓞 L := polyRoot hp hζ u hcong (rootOfSplitsXPowSubC ⋯ ((algebraMap (𝓞 K) K) ↑u) L) ⋯ 0
this : FiniteDimensional K L
⊢ Algebra.adjoin K {↑α} = ⊤
Tactic:
rw [eq_top_iff, ← Algebra.adjoin_root_eq_top_of_isSplittingField
  ⟨ζ, (mem_primitiveRoots p.pos).mpr hζ⟩ (X_pow_sub_C_irreducible_of_prime hpri.out hu)
  (rootOfSplitsXPowSubC_pow p.pos (u : K) L), Algebra.adjoin_le_iff, Set.singleton_subset_iff]
Proof state after:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁵ : Field K
inst✝⁴ : NumberField K
inst✝³ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
L : Type u_2
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsSplittingField K L (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
α : 𝓞 L := polyRoot hp hζ u hcong (rootOfSplitsXPowSubC ⋯ ((algebraMap (𝓞 K) K) ↑u) L) ⋯ 0
this : FiniteDimensional K L
⊢ rootOfSplitsXPowSubC ⋯ ((algebraMap (𝓞 K) K) ↑u) L ∈ ↑(Algebra.adjoin K {↑α})
Theorem: KummersLemma.isUnramified
Proof state before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁵ : Field K
inst✝⁴ : NumberField K
inst✝³ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
L : Type u_2
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsSplittingField K L (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
α : 𝓞 L := polyRoot hp hζ u hcong (rootOfSplitsXPowSubC ⋯ ((algebraMap (𝓞 K) K) ↑u) L) ⋯ 0
this : FiniteDimensional K L
⊢ rootOfSplitsXPowSubC ⋯ ((algebraMap (𝓞 K) K) ↑u) L ∈ ↑(Algebra.adjoin K {↑α})
Tactic:
exact mem_adjoin_polyRoot hp hζ u hcong _ _ 0
Proof state after:
no goals
Theorem: KummersLemma.isUnramified
Proof state before:
case isUnramifiedAt.refine_1
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁵ : Field K
inst✝⁴ : NumberField K
inst✝³ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
L : Type u_2
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsSplittingField K L (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
α : 𝓞 L := polyRoot hp hζ u hcong (rootOfSplitsXPowSubC ⋯ ((algebraMap (𝓞 K) K) ↑u) L) ⋯ 0
this : FiniteDimensional K L
hα : Algebra.adjoin K {↑α} = ⊤
I : Ideal (𝓞 K)
hI : I.IsPrime
hIbot : I ≠ ⊥
⊢ IsIntegral (𝓞 K) ↑α
Tactic:
exact IsIntegral.tower_top α.prop
Proof state after:
no goals
Theorem: KummersLemma.isUnramified
Proof state before:
case isUnramifiedAt.refine_2
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁵ : Field K
inst✝⁴ : NumberField K
inst✝³ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
L : Type u_2
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsSplittingField K L (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
α : 𝓞 L := polyRoot hp hζ u hcong (rootOfSplitsXPowSubC ⋯ ((algebraMap (𝓞 K) K) ↑u) L) ⋯ 0
this : FiniteDimensional K L
hα : Algebra.adjoin K {↑α} = ⊤
I : Ideal (𝓞 K)
hI : I.IsPrime
hIbot : I ≠ ⊥
⊢ (map (Ideal.Quotient.mk I) (minpoly (𝓞 K) ↑α)).Separable
Tactic:
rw [minpoly_polyRoot' hp hζ u hcong hu]
Proof state after:
case isUnramifiedAt.refine_2
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁵ : Field K
inst✝⁴ : NumberField K
inst✝³ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
L : Type u_2
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsSplittingField K L (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
α : 𝓞 L := polyRoot hp hζ u hcong (rootOfSplitsXPowSubC ⋯ ((algebraMap (𝓞 K) K) ↑u) L) ⋯ 0
this : FiniteDimensional K L
hα : Algebra.adjoin K {↑α} = ⊤
I : Ideal (𝓞 K)
hI : I.IsPrime
hIbot : I ≠ ⊥
⊢ (map (Ideal.Quotient.mk I) (poly hp hζ u hcong)).Separable
Theorem: KummersLemma.isUnramified
Proof state before:
case isUnramifiedAt.refine_2
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁵ : Field K
inst✝⁴ : NumberField K
inst✝³ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
L : Type u_2
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsSplittingField K L (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
α : 𝓞 L := polyRoot hp hζ u hcong (rootOfSplitsXPowSubC ⋯ ((algebraMap (𝓞 K) K) ↑u) L) ⋯ 0
this : FiniteDimensional K L
hα : Algebra.adjoin K {↑α} = ⊤
I : Ideal (𝓞 K)
hI : I.IsPrime
hIbot : I ≠ ⊥
⊢ (map (Ideal.Quotient.mk I) (poly hp hζ u hcong)).Separable
Tactic:
haveI := hI.isMaximal hIbot
Proof state after:
case isUnramifiedAt.refine_2
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁵ : Field K
inst✝⁴ : NumberField K
inst✝³ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
L : Type u_2
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsSplittingField K L (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
α : 𝓞 L := polyRoot hp hζ u hcong (rootOfSplitsXPowSubC ⋯ ((algebraMap (𝓞 K) K) ↑u) L) ⋯ 0
this✝ : FiniteDimensional K L
hα : Algebra.adjoin K {↑α} = ⊤
I : Ideal (𝓞 K)
hI : I.IsPrime
hIbot : I ≠ ⊥
this : I.IsMaximal
⊢ (map (Ideal.Quotient.mk I) (poly hp hζ u hcong)).Separable
Theorem: KummersLemma.isUnramified
Proof state before:
case isUnramifiedAt.refine_2
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁵ : Field K
inst✝⁴ : NumberField K
inst✝³ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
L : Type u_2
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsSplittingField K L (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
α : 𝓞 L := polyRoot hp hζ u hcong (rootOfSplitsXPowSubC ⋯ ((algebraMap (𝓞 K) K) ↑u) L) ⋯ 0
this✝ : FiniteDimensional K L
hα : Algebra.adjoin K {↑α} = ⊤
I : Ideal (𝓞 K)
hI : I.IsPrime
hIbot : I ≠ ⊥
this : I.IsMaximal
⊢ (map (Ideal.Quotient.mk I) (poly hp hζ u hcong)).Separable
Tactic:
exact separable_poly hp hζ u hcong hu I
Proof state after:
no goals
Theorem: FltRegular.CaseI.may_assume
Proof state before:
p : ℕ
hpri : Fact p.Prime
⊢ SlightlyEasier → Statement
Tactic:
intro Heasy
Proof state after:
p : ℕ
hpri : Fact p.Prime
Heasy : SlightlyEasier
⊢ Statement
Theorem: FltRegular.CaseI.may_assume
Proof state before:
p : ℕ
hpri : Fact p.Prime
Heasy : SlightlyEasier
⊢ Statement
Tactic:
intro a b c p hpri hreg hI H
Proof state after:
p✝ : ℕ
hpri✝ : Fact p✝.Prime
Heasy : SlightlyEasier
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
⊢ False
Theorem: FltRegular.CaseI.may_assume
Proof state before:
p✝ : ℕ
hpri✝ : Fact p✝.Prime
Heasy : SlightlyEasier
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
⊢ False
Tactic:
have hodd : p ≠ 2 := by
  intro h
  rw [h] at H hI
  refine' hI _
  refine' Dvd.dvd.mul_left _ _
  simp only [Nat.cast_ofNat] at hI ⊢
  rw [← even_iff_two_dvd, ← Int.odd_iff_not_even] at hI
  rw [← even_iff_two_dvd, ← Int.even_pow' (show 2 ≠ 0 by norm_num), ← H]
  exact (Int.Odd.of_mul_left (Odd.of_mul_left hI)).pow.add_odd
    (Int.Odd.of_mul_right (Odd.of_mul_left hI)).pow
Proof state after:
p✝ : ℕ
hpri✝ : Fact p✝.Prime
Heasy : SlightlyEasier
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
hodd : p ≠ 2
⊢ False
Theorem: FltRegular.CaseI.may_assume
Proof state before:
p✝ : ℕ
hpri✝ : Fact p✝.Prime
Heasy : SlightlyEasier
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
hodd : p ≠ 2
⊢ False
Tactic:
have hprod : a * b * c ≠ 0 := by
  intro h
  simp [h] at hI
Proof state after:
p✝ : ℕ
hpri✝ : Fact p✝.Prime
Heasy : SlightlyEasier
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
hodd : p ≠ 2
hprod : a * b * c ≠ 0
⊢ False
Theorem: FltRegular.CaseI.may_assume
Proof state before:
p✝ : ℕ
hpri✝ : Fact p✝.Prime
Heasy : SlightlyEasier
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
hodd : p ≠ 2
hprod : a * b * c ≠ 0
hp5 : 5 ≤ p
⊢ False
Tactic:
rcases MayAssume.coprime H hprod with ⟨Hxyz, hunit, hprodxyx⟩
Proof state after:
case intro.intro
p✝ : ℕ
hpri✝ : Fact p✝.Prime
Heasy : SlightlyEasier
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
hodd : p ≠ 2
hprod : a * b * c ≠ 0
hp5 : 5 ≤ p
Hxyz : (a / {a, b, c}.gcd id) ^ p + (b / {a, b, c}.gcd id) ^ p = (c / {a, b, c}.gcd id) ^ p
hunit : {a / {a, b, c}.gcd id, b / {a, b, c}.gcd id, c / {a, b, c}.gcd id}.gcd id = 1
hprodxyx : a / {a, b, c}.gcd id * (b / {a, b, c}.gcd id) * (c / {a, b, c}.gcd id) ≠ 0
⊢ False
Theorem: FltRegular.CaseI.may_assume
Proof state before:
case intro.intro
p✝ : ℕ
hpri✝ : Fact p✝.Prime
Heasy : SlightlyEasier
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
hodd : p ≠ 2
hprod : a * b * c ≠ 0
hp5 : 5 ≤ p
Hxyz : (a / {a, b, c}.gcd id) ^ p + (b / {a, b, c}.gcd id) ^ p = (c / {a, b, c}.gcd id) ^ p
hunit : {a / {a, b, c}.gcd id, b / {a, b, c}.gcd id, c / {a, b, c}.gcd id}.gcd id = 1
hprodxyx : a / {a, b, c}.gcd id * (b / {a, b, c}.gcd id) * (c / {a, b, c}.gcd id) ≠ 0
⊢ False
Tactic:
let d := ({a, b, c} : Finset ℤ).gcd id
Proof state after:
case intro.intro
p✝ : ℕ
hpri✝ : Fact p✝.Prime
Heasy : SlightlyEasier
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
hodd : p ≠ 2
hprod : a * b * c ≠ 0
hp5 : 5 ≤ p
Hxyz : (a / {a, b, c}.gcd id) ^ p + (b / {a, b, c}.gcd id) ^ p = (c / {a, b, c}.gcd id) ^ p
hunit : {a / {a, b, c}.gcd id, b / {a, b, c}.gcd id, c / {a, b, c}.gcd id}.gcd id = 1
hprodxyx : a / {a, b, c}.gcd id * (b / {a, b, c}.gcd id) * (c / {a, b, c}.gcd id) ≠ 0
d : ℤ := {a, b, c}.gcd id
⊢ False
Theorem: FltRegular.CaseI.may_assume
Proof state before:
case intro.intro
p✝ : ℕ
hpri✝ : Fact p✝.Prime
Heasy : SlightlyEasier
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
hodd : p ≠ 2
hprod : a * b * c ≠ 0
hp5 : 5 ≤ p
Hxyz : (a / {a, b, c}.gcd id) ^ p + (b / {a, b, c}.gcd id) ^ p = (c / {a, b, c}.gcd id) ^ p
hunit : {a / {a, b, c}.gcd id, b / {a, b, c}.gcd id, c / {a, b, c}.gcd id}.gcd id = 1
hprodxyx : a / {a, b, c}.gcd id * (b / {a, b, c}.gcd id) * (c / {a, b, c}.gcd id) ≠ 0
d : ℤ := {a, b, c}.gcd id
⊢ False
Tactic:
have hdiv : ¬↑p ∣ a / d * (b / d) * (c / d) :=
  by
  have hadiv : d ∣ a := gcd_dvd (by simp)
  have hbdiv : d ∣ b := gcd_dvd (by simp)
  have hcdiv : d ∣ c := gcd_dvd (by simp)
  intro hdiv
  replace hdiv := dvd_mul_of_dvd_right hdiv (d * d * d)
  rw [mul_assoc, ← mul_assoc d, ← mul_assoc d, Int.mul_ediv_cancel' hadiv, mul_assoc, mul_comm a,
    mul_assoc (b / d), ← mul_assoc _ (b / d), Int.mul_ediv_cancel' hbdiv, mul_comm, mul_assoc,
    mul_assoc, Int.ediv_mul_cancel hcdiv, mul_comm, mul_assoc, mul_comm c, ← mul_assoc] at hdiv
  exact hI hdiv
Proof state after:
case intro.intro
p✝ : ℕ
hpri✝ : Fact p✝.Prime
Heasy : SlightlyEasier
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
hodd : p ≠ 2
hprod : a * b * c ≠ 0
hp5 : 5 ≤ p
Hxyz : (a / {a, b, c}.gcd id) ^ p + (b / {a, b, c}.gcd id) ^ p = (c / {a, b, c}.gcd id) ^ p
hunit : {a / {a, b, c}.gcd id, b / {a, b, c}.gcd id, c / {a, b, c}.gcd id}.gcd id = 1
hprodxyx : a / {a, b, c}.gcd id * (b / {a, b, c}.gcd id) * (c / {a, b, c}.gcd id) ≠ 0
d : ℤ := {a, b, c}.gcd id
hdiv : ¬↑p ∣ a / d * (b / d) * (c / d)
⊢ False
Theorem: FltRegular.CaseI.may_assume
Proof state before:
case intro.intro
p✝ : ℕ
hpri✝ : Fact p✝.Prime
Heasy : SlightlyEasier
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
hodd : p ≠ 2
hprod : a * b * c ≠ 0
hp5 : 5 ≤ p
Hxyz : (a / {a, b, c}.gcd id) ^ p + (b / {a, b, c}.gcd id) ^ p = (c / {a, b, c}.gcd id) ^ p
hunit : {a / {a, b, c}.gcd id, b / {a, b, c}.gcd id, c / {a, b, c}.gcd id}.gcd id = 1
hprodxyx : a / {a, b, c}.gcd id * (b / {a, b, c}.gcd id) * (c / {a, b, c}.gcd id) ≠ 0
d : ℤ := {a, b, c}.gcd id
hdiv : ¬↑p ∣ a / d * (b / d) * (c / d)
⊢ False
Tactic:
obtain ⟨X, Y, Z, H1, H2, H3, _, H5⟩ := a_not_cong_b hpri.out hp5 hprodxyx Hxyz hunit hdiv
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
p✝ : ℕ
hpri✝ : Fact p✝.Prime
Heasy : SlightlyEasier
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
hodd : p ≠ 2
hprod : a * b * c ≠ 0
hp5 : 5 ≤ p
Hxyz : (a / {a, b, c}.gcd id) ^ p + (b / {a, b, c}.gcd id) ^ p = (c / {a, b, c}.gcd id) ^ p
hunit : {a / {a, b, c}.gcd id, b / {a, b, c}.gcd id, c / {a, b, c}.gcd id}.gcd id = 1
hprodxyx : a / {a, b, c}.gcd id * (b / {a, b, c}.gcd id) * (c / {a, b, c}.gcd id) ≠ 0
d : ℤ := {a, b, c}.gcd id
hdiv : ¬↑p ∣ a / d * (b / d) * (c / d)
X Y Z : ℤ
H1 : X ^ p + Y ^ p = Z ^ p
H2 : {X, Y, Z}.gcd id = 1
H3 : ¬X ≡ Y [ZMOD ↑p]
left✝ : X * Y * Z ≠ 0
H5 : ¬↑p ∣ X * Y * Z
⊢ False