Theorem: quotient_zero_sub_one_comp_aut (FltRegular/NumberTheory/Cyclotomic/MoreLemmas.lean)

State before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
σ : 𝓞 K →+* 𝓞 K
⊢ (Ideal.Quotient.mk (Ideal.span {↑hζ.unit' - 1})).comp σ = Ideal.Quotient.mk (Ideal.span {↑hζ.unit' - 1})
Tactic:
have : Fact (Nat.Prime p) := hpri
State after:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
σ : 𝓞 K →+* 𝓞 K
this : Fact (↑p).Prime
⊢ (Ideal.Quotient.mk (Ideal.span {↑hζ.unit' - 1})).comp σ = Ideal.Quotient.mk (Ideal.span {↑hζ.unit' - 1})

State before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
σ : 𝓞 K →+* 𝓞 K
this : Fact (↑p).Prime
⊢ (Ideal.Quotient.mk (Ideal.span {↑hζ.unit' - 1})).comp σ = Ideal.Quotient.mk (Ideal.span {↑hζ.unit' - 1})
Tactic:
letI := IsCyclotomicExtension.numberField {p} ℚ K
State after:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
σ : 𝓞 K →+* 𝓞 K
this✝ : Fact (↑p).Prime
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
⊢ (Ideal.Quotient.mk (Ideal.span {↑hζ.unit' - 1})).comp σ = Ideal.Quotient.mk (Ideal.span {↑hζ.unit' - 1})

State before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
σ : 𝓞 K →+* 𝓞 K
this✝ : Fact (↑p).Prime
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
⊢ (Ideal.Quotient.mk (Ideal.span {↑hζ.unit' - 1})).comp σ = Ideal.Quotient.mk (Ideal.span {↑hζ.unit' - 1})
Tactic:
letI : AddGroup (𝓞 K ⧸ Ideal.span (singleton (hζ.unit' - 1: 𝓞 K))) := inferInstance
State after:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
σ : 𝓞 K →+* 𝓞 K
this✝¹ : Fact (↑p).Prime
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : AddGroup (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}) := inferInstance
⊢ (Ideal.Quotient.mk (Ideal.span {↑hζ.unit' - 1})).comp σ = Ideal.Quotient.mk (Ideal.span {↑hζ.unit' - 1})

State before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
σ : 𝓞 K →+* 𝓞 K
this✝¹ : Fact (↑p).Prime
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : AddGroup (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}) := inferInstance
⊢ (Ideal.Quotient.mk (Ideal.span {↑hζ.unit' - 1})).comp σ = Ideal.Quotient.mk (Ideal.span {↑hζ.unit' - 1})
Tactic:
apply RingHom.toIntAlgHom_injective
State after:
case a
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
σ : 𝓞 K →+* 𝓞 K
this✝¹ : Fact (↑p).Prime
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : AddGroup (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}) := inferInstance
⊢ ((Ideal.Quotient.mk (Ideal.span {↑hζ.unit' - 1})).comp σ).toIntAlgHom =
    (Ideal.Quotient.mk (Ideal.span {↑hζ.unit' - 1})).toIntAlgHom

State before:
case a
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
σ : 𝓞 K →+* 𝓞 K
this✝¹ : Fact (↑p).Prime
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : AddGroup (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}) := inferInstance
⊢ ((Ideal.Quotient.mk (Ideal.span {↑hζ.unit' - 1})).comp σ).toIntAlgHom =
    (Ideal.Quotient.mk (Ideal.span {↑hζ.unit' - 1})).toIntAlgHom
Tactic:
apply hζ.integralPowerBasis'.algHom_ext
State after:
case a.h
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
σ : 𝓞 K →+* 𝓞 K
this✝¹ : Fact (↑p).Prime
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : AddGroup (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}) := inferInstance
⊢ ((Ideal.Quotient.mk (Ideal.span {↑hζ.unit' - 1})).comp σ).toIntAlgHom hζ.integralPowerBasis'.gen =
    (Ideal.Quotient.mk (Ideal.span {↑hζ.unit' - 1})).toIntAlgHom hζ.integralPowerBasis'.gen

State before:
case a.h
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
σ : 𝓞 K →+* 𝓞 K
this✝¹ : Fact (↑p).Prime
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : AddGroup (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}) := inferInstance
⊢ ((Ideal.Quotient.mk (Ideal.span {↑hζ.unit' - 1})).comp σ).toIntAlgHom hζ.integralPowerBasis'.gen =
    (Ideal.Quotient.mk (Ideal.span {↑hζ.unit' - 1})).toIntAlgHom hζ.integralPowerBasis'.gen
Tactic:
rw [show hζ.integralPowerBasis'.gen = hζ.unit' from Subtype.ext (by simp)]
State after:
case a.h
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
σ : 𝓞 K →+* 𝓞 K
this✝¹ : Fact (↑p).Prime
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : AddGroup (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}) := inferInstance
⊢ ((Ideal.Quotient.mk (Ideal.span {↑hζ.unit' - 1})).comp σ).toIntAlgHom ↑hζ.unit' =
    (Ideal.Quotient.mk (Ideal.span {↑hζ.unit' - 1})).toIntAlgHom ↑hζ.unit'

State before:
case a.h
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
σ : 𝓞 K →+* 𝓞 K
this✝¹ : Fact (↑p).Prime
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : AddGroup (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}) := inferInstance
⊢ ((Ideal.Quotient.mk (Ideal.span {↑hζ.unit' - 1})).comp σ).toIntAlgHom ↑hζ.unit' =
    (Ideal.Quotient.mk (Ideal.span {↑hζ.unit' - 1})).toIntAlgHom ↑hζ.unit'
Tactic:
simp only [RingHom.toIntAlgHom, RingHom.toMonoidHom_eq_coe, AlgHom.coe_mk, RingHom.coe_mk,
  MonoidHom.coe_coe, RingHom.coe_comp, RingHom.coe_coe, Function.comp_apply]
State after:
case a.h
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
σ : 𝓞 K →+* 𝓞 K
this✝¹ : Fact (↑p).Prime
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : AddGroup (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}) := inferInstance
⊢ (Ideal.Quotient.mk (Ideal.span {↑hζ.unit' - 1})) (σ ↑hζ.unit') =
    (Ideal.Quotient.mk (Ideal.span {↑hζ.unit' - 1})) ↑hζ.unit'

State before:
case a.h
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
σ : 𝓞 K →+* 𝓞 K
this✝¹ : Fact (↑p).Prime
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : AddGroup (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}) := inferInstance
⊢ (Ideal.Quotient.mk (Ideal.span {↑hζ.unit' - 1})) (σ ↑hζ.unit') =
    (Ideal.Quotient.mk (Ideal.span {↑hζ.unit' - 1})) ↑hζ.unit'
Tactic:
rw [← sub_eq_zero, ← map_sub, Ideal.Quotient.eq_zero_iff_mem, Ideal.mem_span_singleton]
State after:
case a.h
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
σ : 𝓞 K →+* 𝓞 K
this✝¹ : Fact (↑p).Prime
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : AddGroup (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}) := inferInstance
⊢ ↑hζ.unit' - 1 ∣ σ ↑hζ.unit' - ↑hζ.unit'

State before:
case a.h
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
σ : 𝓞 K →+* 𝓞 K
this✝¹ : Fact (↑p).Prime
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : AddGroup (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}) := inferInstance
⊢ ↑hζ.unit' - 1 ∣ σ ↑hζ.unit' - ↑hζ.unit'
Tactic:
apply hζ.unit'_coe.sub_one_dvd_sub hpri.out
State after:
case a.h.hη₁
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
σ : 𝓞 K →+* 𝓞 K
this✝¹ : Fact (↑p).Prime
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : AddGroup (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}) := inferInstance
⊢ σ ↑hζ.unit' ∈ nthRootsFinset (↑p) (𝓞 K)

case a.h.hη₂
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
σ : 𝓞 K →+* 𝓞 K
this✝¹ : Fact (↑p).Prime
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : AddGroup (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}) := inferInstance
⊢ ↑hζ.unit' ∈ nthRootsFinset (↑p) (𝓞 K)

State before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
σ : 𝓞 K →+* 𝓞 K
this✝¹ : Fact (↑p).Prime
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : AddGroup (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}) := inferInstance
⊢ ↑hζ.integralPowerBasis'.gen = ↑↑hζ.unit'
Tactic:
simp
State after:
no goals

State before:
case a.h.hη₁
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
σ : 𝓞 K →+* 𝓞 K
this✝¹ : Fact (↑p).Prime
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : AddGroup (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}) := inferInstance
⊢ σ ↑hζ.unit' ∈ nthRootsFinset (↑p) (𝓞 K)
Tactic:
rw [mem_nthRootsFinset p.pos, ← map_pow, hζ.unit'_coe.pow_eq_one, map_one]
State after:
no goals

State before:
case a.h.hη₂
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
σ : 𝓞 K →+* 𝓞 K
this✝¹ : Fact (↑p).Prime
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : AddGroup (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}) := inferInstance
⊢ ↑hζ.unit' ∈ nthRootsFinset (↑p) (𝓞 K)
Tactic:
rw [mem_nthRootsFinset p.pos, hζ.unit'_coe.pow_eq_one]
State after:
no goals