Theorem: exists_not_isPrincipal_and_isPrincipal_map (FltRegular/NumberTheory/Hilbert94.lean)

State before:
K✝ : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝²⁵ : Field K✝
inst✝²⁴ : NumberField K✝
inst✝²³ : Fintype (ClassGroup (𝓞 K✝))
L✝ : Type ?u.146081
inst✝²² : Field L✝
inst✝²¹ : Algebra K✝ L✝
inst✝²⁰ : FiniteDimensional K✝ L✝
inst✝¹⁹ : IsGalois K✝ L✝
σ : L✝ ≃ₐ[K✝] L✝
hσ : ∀ (x : L✝ ≃ₐ[K✝] L✝), x ∈ Subgroup.zpowers σ
hKL✝ : finrank K✝ L✝ = ↑p
A : Type ?u.147972
B : Type ?u.147975
inst✝¹⁸ : CommRing A
inst✝¹⁷ : CommRing B
inst✝¹⁶ : Algebra A B
inst✝¹⁵ : Algebra A L✝
inst✝¹⁴ : Algebra A K✝
inst✝¹³ : Algebra B L✝
inst✝¹² : IsScalarTower A B L✝
inst✝¹¹ : IsScalarTower A K✝ L✝
inst✝¹⁰ : IsFractionRing A K✝
inst✝⁹ : IsIntegralClosure B A L✝
K : Type u_2
L : Type u_3
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : NumberField K
inst✝⁵ : NumberField L
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : IsGalois K L
inst✝¹ : IsUnramified (𝓞 K) (𝓞 L)
inst✝ : IsCyclic (L ≃ₐ[K] L)
hKL : (finrank K L).Prime
hKL' : finrank K L ≠ 2
⊢ ∃ I, ¬Submodule.IsPrincipal I ∧ Submodule.IsPrincipal (Ideal.map (algebraMap (𝓞 K) (𝓞 L)) I)
Tactic:
obtain ⟨⟨σ, hσ⟩⟩ := ‹IsCyclic (L ≃ₐ[K] L)›
State after:
case mk.intro
K✝ : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝²⁵ : Field K✝
inst✝²⁴ : NumberField K✝
inst✝²³ : Fintype (ClassGroup (𝓞 K✝))
L✝ : Type ?u.146081
inst✝²² : Field L✝
inst✝²¹ : Algebra K✝ L✝
inst✝²⁰ : FiniteDimensional K✝ L✝
inst✝¹⁹ : IsGalois K✝ L✝
σ✝ : L✝ ≃ₐ[K✝] L✝
hσ✝ : ∀ (x : L✝ ≃ₐ[K✝] L✝), x ∈ Subgroup.zpowers σ✝
hKL✝ : finrank K✝ L✝ = ↑p
A : Type ?u.147972
B : Type ?u.147975
inst✝¹⁸ : CommRing A
inst✝¹⁷ : CommRing B
inst✝¹⁶ : Algebra A B
inst✝¹⁵ : Algebra A L✝
inst✝¹⁴ : Algebra A K✝
inst✝¹³ : Algebra B L✝
inst✝¹² : IsScalarTower A B L✝
inst✝¹¹ : IsScalarTower A K✝ L✝
inst✝¹⁰ : IsFractionRing A K✝
inst✝⁹ : IsIntegralClosure B A L✝
K : Type u_2
L : Type u_3
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : NumberField K
inst✝⁵ : NumberField L
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : IsGalois K L
inst✝¹ : IsUnramified (𝓞 K) (𝓞 L)
inst✝ : IsCyclic (L ≃ₐ[K] L)
hKL : (finrank K L).Prime
hKL' : finrank K L ≠ 2
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
⊢ ∃ I, ¬Submodule.IsPrincipal I ∧ Submodule.IsPrincipal (Ideal.map (algebraMap (𝓞 K) (𝓞 L)) I)

State before:
case mk.intro
K✝ : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝²⁵ : Field K✝
inst✝²⁴ : NumberField K✝
inst✝²³ : Fintype (ClassGroup (𝓞 K✝))
L✝ : Type ?u.146081
inst✝²² : Field L✝
inst✝²¹ : Algebra K✝ L✝
inst✝²⁰ : FiniteDimensional K✝ L✝
inst✝¹⁹ : IsGalois K✝ L✝
σ✝ : L✝ ≃ₐ[K✝] L✝
hσ✝ : ∀ (x : L✝ ≃ₐ[K✝] L✝), x ∈ Subgroup.zpowers σ✝
hKL✝ : finrank K✝ L✝ = ↑p
A : Type ?u.147972
B : Type ?u.147975
inst✝¹⁸ : CommRing A
inst✝¹⁷ : CommRing B
inst✝¹⁶ : Algebra A B
inst✝¹⁵ : Algebra A L✝
inst✝¹⁴ : Algebra A K✝
inst✝¹³ : Algebra B L✝
inst✝¹² : IsScalarTower A B L✝
inst✝¹¹ : IsScalarTower A K✝ L✝
inst✝¹⁰ : IsFractionRing A K✝
inst✝⁹ : IsIntegralClosure B A L✝
K : Type u_2
L : Type u_3
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : NumberField K
inst✝⁵ : NumberField L
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : IsGalois K L
inst✝¹ : IsUnramified (𝓞 K) (𝓞 L)
inst✝ : IsCyclic (L ≃ₐ[K] L)
hKL : (finrank K L).Prime
hKL' : finrank K L ≠ 2
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
⊢ ∃ I, ¬Submodule.IsPrincipal I ∧ Submodule.IsPrincipal (Ideal.map (algebraMap (𝓞 K) (𝓞 L)) I)
Tactic:
obtain ⟨η, hη, hη'⟩ := Hilbert92 hKL hKL' σ hσ
State after:
case mk.intro.intro.intro
K✝ : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝²⁵ : Field K✝
inst✝²⁴ : NumberField K✝
inst✝²³ : Fintype (ClassGroup (𝓞 K✝))
L✝ : Type ?u.146081
inst✝²² : Field L✝
inst✝²¹ : Algebra K✝ L✝
inst✝²⁰ : FiniteDimensional K✝ L✝
inst✝¹⁹ : IsGalois K✝ L✝
σ✝ : L✝ ≃ₐ[K✝] L✝
hσ✝ : ∀ (x : L✝ ≃ₐ[K✝] L✝), x ∈ Subgroup.zpowers σ✝
hKL✝ : finrank K✝ L✝ = ↑p
A : Type ?u.147972
B : Type ?u.147975
inst✝¹⁸ : CommRing A
inst✝¹⁷ : CommRing B
inst✝¹⁶ : Algebra A B
inst✝¹⁵ : Algebra A L✝
inst✝¹⁴ : Algebra A K✝
inst✝¹³ : Algebra B L✝
inst✝¹² : IsScalarTower A B L✝
inst✝¹¹ : IsScalarTower A K✝ L✝
inst✝¹⁰ : IsFractionRing A K✝
inst✝⁹ : IsIntegralClosure B A L✝
K : Type u_2
L : Type u_3
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : NumberField K
inst✝⁵ : NumberField L
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : IsGalois K L
inst✝¹ : IsUnramified (𝓞 K) (𝓞 L)
inst✝ : IsCyclic (L ≃ₐ[K] L)
hKL : (finrank K L).Prime
hKL' : finrank K L ≠ 2
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
η : (𝓞 L)ˣ
hη : (Algebra.norm K) ((algebraMap (𝓞 L) L) ↑η) = 1
hη' : ∀ (ε : (𝓞 L)ˣ), (algebraMap (𝓞 L) L) ↑η ≠ (algebraMap (𝓞 L) L) ↑ε / σ ((algebraMap (𝓞 L) L) ↑ε)
⊢ ∃ I, ¬Submodule.IsPrincipal I ∧ Submodule.IsPrincipal (Ideal.map (algebraMap (𝓞 K) (𝓞 L)) I)

State before:
case mk.intro.intro.intro
K✝ : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝²⁵ : Field K✝
inst✝²⁴ : NumberField K✝
inst✝²³ : Fintype (ClassGroup (𝓞 K✝))
L✝ : Type ?u.146081
inst✝²² : Field L✝
inst✝²¹ : Algebra K✝ L✝
inst✝²⁰ : FiniteDimensional K✝ L✝
inst✝¹⁹ : IsGalois K✝ L✝
σ✝ : L✝ ≃ₐ[K✝] L✝
hσ✝ : ∀ (x : L✝ ≃ₐ[K✝] L✝), x ∈ Subgroup.zpowers σ✝
hKL✝ : finrank K✝ L✝ = ↑p
A : Type ?u.147972
B : Type ?u.147975
inst✝¹⁸ : CommRing A
inst✝¹⁷ : CommRing B
inst✝¹⁶ : Algebra A B
inst✝¹⁵ : Algebra A L✝
inst✝¹⁴ : Algebra A K✝
inst✝¹³ : Algebra B L✝
inst✝¹² : IsScalarTower A B L✝
inst✝¹¹ : IsScalarTower A K✝ L✝
inst✝¹⁰ : IsFractionRing A K✝
inst✝⁹ : IsIntegralClosure B A L✝
K : Type u_2
L : Type u_3
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : NumberField K
inst✝⁵ : NumberField L
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : IsGalois K L
inst✝¹ : IsUnramified (𝓞 K) (𝓞 L)
inst✝ : IsCyclic (L ≃ₐ[K] L)
hKL : (finrank K L).Prime
hKL' : finrank K L ≠ 2
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
η : (𝓞 L)ˣ
hη : (Algebra.norm K) ((algebraMap (𝓞 L) L) ↑η) = 1
hη' : ∀ (ε : (𝓞 L)ˣ), (algebraMap (𝓞 L) L) ↑η ≠ (algebraMap (𝓞 L) L) ↑ε / σ ((algebraMap (𝓞 L) L) ↑ε)
⊢ ∃ I, ¬Submodule.IsPrincipal I ∧ Submodule.IsPrincipal (Ideal.map (algebraMap (𝓞 K) (𝓞 L)) I)
Tactic:
exact exists_not_isPrincipal_and_isPrincipal_map_aux (A := (𝓞 K)) σ hσ η hη (not_exists.mpr hη')
State after:
no goals