Theorem: exists_not_isPrincipal_and_isPrincipal_map_aux
Proof state before:
case h
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝¹⁸ : Field K
inst✝¹⁷ : NumberField K
inst✝¹⁶ : Fintype (ClassGroup (𝓞 K))
L : Type u_4
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_2
B : Type u_3
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
inst✝¹ : IsDedekindDomain A
inst✝ : IsUnramified A B
η : Bˣ
hη : (Algebra.norm K) ((algebraMap B L) ↑η) = 1
hη' : ¬∃ α, (algebraMap B L) ↑η = (algebraMap B L) ↑α / σ ((algebraMap B L) ↑α)
this : IsDomain B
γ : A
a : Bˣ
hβ_zero : (algebraMap A B) γ * ↑a ≠ 0
hβ : ↑η * ((galRestrict A K L B) σ) ↑a = ↑a
hγ : Ideal.comap (algebraMap A B) (Ideal.span {(algebraMap A B) γ * ↑a}) = Ideal.span {γ}
⊢ (algebraMap B L) ↑η = (algebraMap B L) (↑η * ((galRestrict A K L B) σ) ↑a) / σ ((algebraMap B L) ↑a)

K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝¹⁸ : Field K
inst✝¹⁷ : NumberField K
inst✝¹⁶ : Fintype (ClassGroup (𝓞 K))
L : Type u_4
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_2
B : Type u_3
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
inst✝¹ : IsDedekindDomain A
inst✝ : IsUnramified A B
η : Bˣ
hη : (Algebra.norm K) ((algebraMap B L) ↑η) = 1
hη' : ¬∃ α, (algebraMap B L) ↑η = (algebraMap B L) ↑α / σ ((algebraMap B L) ↑α)
this : IsDomain B
γ : A
a : Bˣ
hβ_zero : (algebraMap A B) γ * ↑a ≠ 0
hβ : (algebraMap A B) γ * (↑η * ((galRestrict A K L B) σ) ↑a) = (algebraMap A B) γ * ↑a
hγ : Ideal.comap (algebraMap A B) (Ideal.span {(algebraMap A B) γ * ↑a}) = Ideal.span {γ}
⊢ (algebraMap A B) γ ≠ 0
Tactic:
rw [map_mul, ← AlgHom.coe_coe σ, ← algebraMap_galRestrictHom_apply A K L B σ a]
Proof state after:
case h
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝¹⁸ : Field K
inst✝¹⁷ : NumberField K
inst✝¹⁶ : Fintype (ClassGroup (𝓞 K))
L : Type u_4
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_2
B : Type u_3
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
inst✝¹ : IsDedekindDomain A
inst✝ : IsUnramified A B
η : Bˣ
hη : (Algebra.norm K) ((algebraMap B L) ↑η) = 1
hη' : ¬∃ α, (algebraMap B L) ↑η = (algebraMap B L) ↑α / σ ((algebraMap B L) ↑α)
this : IsDomain B
γ : A
a : Bˣ
hβ_zero : (algebraMap A B) γ * ↑a ≠ 0
hβ : ↑η * ((galRestrict A K L B) σ) ↑a = ↑a
hγ : Ideal.comap (algebraMap A B) (Ideal.span {(algebraMap A B) γ * ↑a}) = Ideal.span {γ}
⊢ (algebraMap B L) ↑η =
    (algebraMap B L) ↑η * (algebraMap B L) (((galRestrict A K L B) σ) ↑a) /
      (algebraMap B L) (((galRestrictHom A K L B) ↑σ) ↑a)

K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝¹⁸ : Field K
inst✝¹⁷ : NumberField K
inst✝¹⁶ : Fintype (ClassGroup (𝓞 K))
L : Type u_4
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_2
B : Type u_3
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
inst✝¹ : IsDedekindDomain A
inst✝ : IsUnramified A B
η : Bˣ
hη : (Algebra.norm K) ((algebraMap B L) ↑η) = 1
hη' : ¬∃ α, (algebraMap B L) ↑η = (algebraMap B L) ↑α / σ ((algebraMap B L) ↑α)
this : IsDomain B
γ : A
a : Bˣ
hβ_zero : (algebraMap A B) γ * ↑a ≠ 0
hβ : (algebraMap A B) γ * (↑η * ((galRestrict A K L B) σ) ↑a) = (algebraMap A B) γ * ↑a
hγ : Ideal.comap (algebraMap A B) (Ideal.span {(algebraMap A B) γ * ↑a}) = Ideal.span {γ}
⊢ (algebraMap A B) γ ≠ 0