internlm/Lean-Github huggingface dataset:
Theorem: Ideal.isPrincipal_pow_finrank_of_isPrincipal_map
Proof state before:
case hAB
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
I : Ideal A
hI : Submodule.IsPrincipal (map (algebraMap A B) I)
this✝² : IsDomain B
this✝¹ : IsNoetherian A B
this✝ : IsDedekindDomain B
this : IsFractionRing B L
⊢ Function.Injective ⇑((algebraMap K L).comp (algebraMap A K))
Tactic:
exact (algebraMap K L).injective.comp (IsFractionRing.injective _ _)
Proof state after:
no goals
Theorem: Ideal.isPrincipal_pow_finrank_of_isPrincipal_map
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
I : Ideal A
hI : Submodule.IsPrincipal (map (algebraMap A B) I)
this✝⁴ : IsDomain B
this✝³ : IsNoetherian A B
this✝² : IsDedekindDomain B
this✝¹ : IsFractionRing B L
hAB : NoZeroSMulDivisors A B
this✝ : Algebra (FractionRing A) (FractionRing B) := FractionRing.liftAlgebra A (FractionRing B)
this : IsScalarTower A (FractionRing A) (FractionRing B)
⊢ (algebraMap (FractionRing A) (FractionRing B)).comp ↑(FractionRing.algEquiv A K).symm.toRingEquiv =
    (↑(FractionRing.algEquiv B L).symm.toRingEquiv).comp (algebraMap K L)
Tactic:
apply IsLocalization.ringHom_ext (nonZeroDivisors A)
Proof state after:
case H.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
I : Ideal A
hI : Submodule.IsPrincipal (map (algebraMap A B) I)
this✝⁴ : IsDomain B
this✝³ : IsNoetherian A B
this✝² : IsDedekindDomain B
this✝¹ : IsFractionRing B L
hAB : NoZeroSMulDivisors A B
this✝ : Algebra (FractionRing A) (FractionRing B) := FractionRing.liftAlgebra A (FractionRing B)
this : IsScalarTower A (FractionRing A) (FractionRing B)
⊢ ((algebraMap (FractionRing A) (FractionRing B)).comp ↑(FractionRing.algEquiv A K).symm.toRingEquiv).comp
      (algebraMap A K) =
    ((↑(FractionRing.algEquiv B L).symm.toRingEquiv).comp (algebraMap K L)).comp (algebraMap A K)
Theorem: Ideal.isPrincipal_pow_finrank_of_isPrincipal_map
Proof state before:
case H.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
I : Ideal A
hI : Submodule.IsPrincipal (map (algebraMap A B) I)
this✝⁴ : IsDomain B
this✝³ : IsNoetherian A B
this✝² : IsDedekindDomain B
this✝¹ : IsFractionRing B L
hAB : NoZeroSMulDivisors A B
this✝ : Algebra (FractionRing A) (FractionRing B) := FractionRing.liftAlgebra A (FractionRing B)
this : IsScalarTower A (FractionRing A) (FractionRing B)
⊢ ((algebraMap (FractionRing A) (FractionRing B)).comp ↑(FractionRing.algEquiv A K).symm.toRingEquiv).comp
      (algebraMap A K) =
    ((↑(FractionRing.algEquiv B L).symm.toRingEquiv).comp (algebraMap K L)).comp (algebraMap A K)
Tactic:
ext
Proof state after:
case H.h.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
I : Ideal A
hI : Submodule.IsPrincipal (map (algebraMap A B) I)
this✝⁴ : IsDomain B
this✝³ : IsNoetherian A B
this✝² : IsDedekindDomain B
this✝¹ : IsFractionRing B L
hAB : NoZeroSMulDivisors A B
this✝ : Algebra (FractionRing A) (FractionRing B) := FractionRing.liftAlgebra A (FractionRing B)
this : IsScalarTower A (FractionRing A) (FractionRing B)
x✝ : A
⊢ (((algebraMap (FractionRing A) (FractionRing B)).comp ↑(FractionRing.algEquiv A K).symm.toRingEquiv).comp
        (algebraMap A K))
      x✝ =
    (((↑(FractionRing.algEquiv B L).symm.toRingEquiv).comp (algebraMap K L)).comp (algebraMap A K)) x✝
Theorem: Ideal.isPrincipal_pow_finrank_of_isPrincipal_map
Proof state before:
case H.h.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
I : Ideal A
hI : Submodule.IsPrincipal (map (algebraMap A B) I)
this✝⁴ : IsDomain B
this✝³ : IsNoetherian A B
this✝² : IsDedekindDomain B
this✝¹ : IsFractionRing B L
hAB : NoZeroSMulDivisors A B
this✝ : Algebra (FractionRing A) (FractionRing B) := FractionRing.liftAlgebra A (FractionRing B)
this : IsScalarTower A (FractionRing A) (FractionRing B)
x✝ : A
⊢ (((algebraMap (FractionRing A) (FractionRing B)).comp ↑(FractionRing.algEquiv A K).symm.toRingEquiv).comp
        (algebraMap A K))
      x✝ =
    (((↑(FractionRing.algEquiv B L).symm.toRingEquiv).comp (algebraMap K L)).comp (algebraMap A K)) x✝
Tactic:
simp only [AlgEquiv.toRingEquiv_eq_coe, RingHom.coe_comp, RingHom.coe_coe,
  AlgEquiv.coe_ringEquiv, Function.comp_apply, AlgEquiv.commutes,
  ← IsScalarTower.algebraMap_apply]
Proof state after:
case H.h.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
I : Ideal A
hI : Submodule.IsPrincipal (map (algebraMap A B) I)
this✝⁴ : IsDomain B
this✝³ : IsNoetherian A B
this✝² : IsDedekindDomain B
this✝¹ : IsFractionRing B L
hAB : NoZeroSMulDivisors A B
this✝ : Algebra (FractionRing A) (FractionRing B) := FractionRing.liftAlgebra A (FractionRing B)
this : IsScalarTower A (FractionRing A) (FractionRing B)
x✝ : A
⊢ (algebraMap A (FractionRing B)) x✝ = (FractionRing.algEquiv B L).symm ((algebraMap A L) x✝)
Theorem: Ideal.isPrincipal_pow_finrank_of_isPrincipal_map
Proof state before:
case H.h.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
I : Ideal A
hI : Submodule.IsPrincipal (map (algebraMap A B) I)
this✝⁴ : IsDomain B
this✝³ : IsNoetherian A B
this✝² : IsDedekindDomain B
this✝¹ : IsFractionRing B L
hAB : NoZeroSMulDivisors A B
this✝ : Algebra (FractionRing A) (FractionRing B) := FractionRing.liftAlgebra A (FractionRing B)
this : IsScalarTower A (FractionRing A) (FractionRing B)
x✝ : A
⊢ (algebraMap A (FractionRing B)) x✝ = (FractionRing.algEquiv B L).symm ((algebraMap A L) x✝)
Tactic:
rw [IsScalarTower.algebraMap_apply A B L, AlgEquiv.commutes, ← IsScalarTower.algebraMap_apply]
Proof state after:
no goals
Theorem: Ideal.isPrincipal_pow_finrank_of_isPrincipal_map
Proof state before:
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
I : Ideal A
hI : Submodule.IsPrincipal (map (algebraMap A B) I)
this✝⁵ : IsDomain B
this✝⁴ : IsNoetherian A B
this✝³ : IsDedekindDomain B
this✝² : IsFractionRing B L
hAB : NoZeroSMulDivisors A B
this✝¹ : Algebra (FractionRing A) (FractionRing B) := FractionRing.liftAlgebra A (FractionRing B)
this✝ : IsScalarTower A (FractionRing A) (FractionRing B)
H :
  (algebraMap (FractionRing A) (FractionRing B)).comp ↑(FractionRing.algEquiv A K).symm.toRingEquiv =
    (↑(FractionRing.algEquiv B L).symm.toRingEquiv).comp (algebraMap K L)
this : IsSeparable (FractionRing A) (FractionRing B)
⊢ finrank (FractionRing A) (FractionRing B) = finrank K L
Tactic:
simpa only [Cardinal.toNat_lift] using congr_arg Cardinal.toNat
  (Algebra.lift_rank_eq_of_equiv_equiv (FractionRing.algEquiv A K).symm.toRingEquiv
    (FractionRing.algEquiv B L).symm.toRingEquiv H).symm
Proof state after:
no goals
Theorem: exists_not_isPrincipal_and_isPrincipal_map
Proof 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)›
Proof 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)
Theorem: exists_not_isPrincipal_and_isPrincipal_map
Proof 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σ
Proof 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)
Theorem: exists_not_isPrincipal_and_isPrincipal_map
Proof 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η')
Proof state after:
no goals
Theorem: dvd_card_classGroup_of_isUnramified_isCyclic
Proof state before:
K✝ : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝²⁵ : Field K✝
inst✝²⁴ : NumberField K✝
inst✝²³ : Fintype (ClassGroup (𝓞 K✝))
L✝ : Type ?u.157534
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.159425
B : Type ?u.159428
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
⊢ finrank K L ∣ Fintype.card (ClassGroup (𝓞 K))
Tactic:
obtain ⟨I, hI, hI'⟩ := exists_not_isPrincipal_and_isPrincipal_map K L hKL hKL'
Proof state after:
case intro.intro
K✝ : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝²⁵ : Field K✝
inst✝²⁴ : NumberField K✝
inst✝²³ : Fintype (ClassGroup (𝓞 K✝))
L✝ : Type ?u.157534
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.159425
B : Type ?u.159428
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 : Ideal (𝓞 K)
hI : ¬Submodule.IsPrincipal I
hI' : Submodule.IsPrincipal (Ideal.map (algebraMap (𝓞 K) (𝓞 L)) I)
⊢ finrank K L ∣ Fintype.card (ClassGroup (𝓞 K))
Theorem: dvd_card_classGroup_of_isUnramified_isCyclic
Proof state before:
case intro.intro
K✝ : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝²⁵ : Field K✝
inst✝²⁴ : NumberField K✝
inst✝²³ : Fintype (ClassGroup (𝓞 K✝))
L✝ : Type ?u.157534
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.159425
B : Type ?u.159428
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 : Ideal (𝓞 K)
hI : ¬Submodule.IsPrincipal I
hI' : Submodule.IsPrincipal (Ideal.map (algebraMap (𝓞 K) (𝓞 L)) I)
⊢ finrank K L ∣ Fintype.card (ClassGroup (𝓞 K))
Tactic:
letI := Fact.mk hKL
Proof state after:
case intro.intro
K✝ : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝²⁵ : Field K✝
inst✝²⁴ : NumberField K✝
inst✝²³ : Fintype (ClassGroup (𝓞 K✝))
L✝ : Type ?u.157534
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.159425
B : Type ?u.159428
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 : Ideal (𝓞 K)
hI : ¬Submodule.IsPrincipal I
hI' : Submodule.IsPrincipal (Ideal.map (algebraMap (𝓞 K) (𝓞 L)) I)
this : Fact (finrank K L).Prime := { out := hKL }
⊢ finrank K L ∣ Fintype.card (ClassGroup (𝓞 K))