Prime ideal orbits in a quadratic number-field extension. These are the arithmetic inputs for factoring invariant ideals into extended base ideals and ramified prime factors.

theorem CCDN.quadratic_integer_ideal_action (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] (σ : Gal(K/F)) (I : Ideal (NumberField.RingOfIntegers K)) : σ • I = Ideal.map (NumberField.RingOfIntegers.mapAlgEquiv σ).toRingEquiv.toRingHom I

The action of σ : K ≃ₐ[F] K on ideals of 𝓞 K is the image under the induced automorphism of 𝓞 K.

theorem CCDN.quadratic_prime_ramification_one_or_two (F : Type u_1) (K : Type u_2) [Field F] [Field K] [NumberField F] [NumberField K] [Algebra F K] [FiniteDimensional F K] (hd : Module.finrank F K = 2) (Q : Ideal (NumberField.RingOfIntegers K)) [Q.IsPrime] : Q.ramificationIdx (NumberField.RingOfIntegers F) = 1 ∨ Q.ramificationIdx (NumberField.RingOfIntegers F) = 2

In a quadratic extension K / F, every prime ideal of 𝓞 K has ramification index 1 or 2 over 𝓞 F.

theorem CCDN.quadratic_moving_prime_unramified (F : Type u_1) (K : Type u_2) [Field F] [Field K] [NumberField F] [NumberField K] [Algebra F K] [FiniteDimensional F K] (hd : Module.finrank F K = 2) (σ : Gal(K/F)) (hσ : σ ≠ 1) (Q : Ideal (NumberField.RingOfIntegers K)) [Q.IsPrime] (hmove : σ • Q ≠ Q) : Q.ramificationIdx (NumberField.RingOfIntegers F) = 1

In a quadratic extension with nontrivial automorphism σ, a prime ideal of 𝓞 K not fixed by σ is unramified over 𝓞 F.

theorem CCDN.quadratic_fixed_prime_extension (F : Type u_1) (K : Type u_2) [Field F] [Field K] [NumberField F] [NumberField K] [Algebra F K] [FiniteDimensional F K] (hd : Module.finrank F K = 2) (σ : Gal(K/F)) (hσ : σ ≠ 1) (Q : Ideal (NumberField.RingOfIntegers K)) [Q.IsPrime] (hQ : Q ≠ ⊥) (hfix : σ • Q = Q) : Ideal.map (algebraMap (NumberField.RingOfIntegers F) (NumberField.RingOfIntegers K)) (Ideal.under (NumberField.RingOfIntegers F) Q) = Q ^ Q.ramificationIdx (NumberField.RingOfIntegers F)

In a quadratic extension with nontrivial automorphism σ, a nonzero prime Q of 𝓞 K fixed by σ is the only prime above its contraction P, so P 𝓞 K = Q ^ e with e its ramification index.

theorem CCDN.quadratic_moving_prime_extension (F : Type u_1) (K : Type u_2) [Field F] [Field K] [NumberField F] [NumberField K] [Algebra F K] [FiniteDimensional F K] (hd : Module.finrank F K = 2) (σ : Gal(K/F)) (hσ : σ ≠ 1) (Q : Ideal (NumberField.RingOfIntegers K)) [Q.IsPrime] (hQ : Q ≠ ⊥) (hmove : σ • Q ≠ Q) : Ideal.map (algebraMap (NumberField.RingOfIntegers F) (NumberField.RingOfIntegers K)) (Ideal.under (NumberField.RingOfIntegers F) Q) = Q * σ • Q

In a quadratic extension with nontrivial automorphism σ, a nonzero prime Q of 𝓞 K not fixed by σ satisfies P 𝓞 K = Q * σ Q, where P is its contraction to 𝓞 F.