Theorems · Theorem · number theory

Ideal.exists_comap_galRestrict_eq

∀ (R : Type u_1) (K : Type u_2) (L : Type u_3) (S : Type u_4) [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : Field K] [inst_4 : Field L] [inst_5 : Algebra R K] [inst_6 : IsFractionRing R K]
  [inst_7 : Algebra S L] [inst_8 : Algebra K L] [inst_9 : Algebra R L] [inst_10 : IsScalarTower R S L]
  [inst_11 : IsScalarTower R K L] [inst_12 : IsIntegralClosure S R L] [FiniteDimensional K L] [IsDedekindDomain R]
  [inst_15 : IsGalois K L] {p : Ideal R} {P₁ P₂ : Ideal S},
  P₁ ∈ p.primesOver S → P₂ ∈ p.primesOver S → ∃ σ, Ideal.comap ((galRestrict R K L S) σ) P₁ = P₂

Defined in

Mathlib.NumberTheory.RamificationInertia.Galois

Cited by

0 results in Mathlib

Foundations

Depth 204 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingCommRingAlgebraFieldFieldAlgebraIsFractionRingAlgebraAlgebraAlgebraIsScalarTowerIsScalarTowerIsIntegralClosureFiniteDimensionalIsDedekindDomainIsGalois