Documentation

RealClosedField.PrimitiveElement.Quadratic

theorem Polynomial.X_sq_sub_C_irreducible_iff_not_isSquare {F : Type u_1} [Field F] (a : F) :

Irreducible (X ^ 2 - C a) ↔ ¬IsSquare a

structure IsIntegralGenSqrt {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] (r : S) (a : R) extends IsIntegralUniqueGen r (Polynomial.X ^ 2 - Polynomial.C a) :

adjoin_eq_top : R[r] = ⊤
ker_aeval : RingHom.ker (Polynomial.aeval r) = Ideal.span {Polynomial.X ^ 2 - Polynomial.C a}
monic : (Polynomial.X ^ 2 - Polynomial.C a).Monic

Instances For

theorem IsIntegralGenSqrt.sq_root {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {r : S} {a : R} (h : IsIntegralGenSqrt r a) :

r ^ 2 = (algebraMap R S) a

theorem IsIntegralGenSqrt.nontrivial {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {r : S} {a : R} (h : IsIntegralGenSqrt r a) [Nontrivial R] :

theorem IsIntegralGenSqrt.finrank {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {r : S} {a : R} (h : IsIntegralGenSqrt r a) [Nontrivial R] :

Module.finrank R S = 2

theorem IsIntegralGenSqrt.isQuadraticExtension {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {r : S} {a : R} (h : IsIntegralGenSqrt r a) [Nontrivial R] :

Algebra.IsQuadraticExtension R S

noncomputable def IsIntegralGenSqrt.basis {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {r : S} {a : R} (h : IsIntegralGenSqrt r a) [Nontrivial R] :

Module.Basis (Fin 2) R S

Equations

h.basis = ⋯.basis.reindex (finCongr ⋯)

Instances For

theorem IsIntegralGenSqrt.basis_0 {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {r : S} {a : R} (h : IsIntegralGenSqrt r a) [Nontrivial R] :

h.basis 0 = 1

theorem IsIntegralGenSqrt.basis_1 {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {r : S} {a : R} (h : IsIntegralGenSqrt r a) [Nontrivial R] :

h.basis 1 = r

@[reducible]

noncomputable def IsIntegralGenSqrt.coeff {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {r : S} {a : R} (h : IsIntegralGenSqrt r a) :

S →ₗ[R] ℕ →₀ R

Equations

h.coeff = ⋯.coeff

Instances For

theorem IsIntegralGenSqrt.basis_repr_eq_coeff {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {r : S} {a : R} (h : IsIntegralGenSqrt r a) [Nontrivial R] (y : S) (i : Fin 2) :

(h.basis.repr y) i = (h.coeff y) ↑i

theorem IsIntegralGenSqrt.coeff_apply_of_two_le {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {r : S} {a : R} (h : IsIntegralGenSqrt r a) [Nontrivial R] (z : S) {i : ℕ} (hi : 2 ≤ i) :

(h.coeff z) i = 0

@[simp]

theorem IsIntegralGenSqrt.coeff_one {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {r : S} {a : R} (h : IsIntegralGenSqrt r a) [Nontrivial R] :

h.coeff 1 = fun₀ | 0 => 1

@[simp]

theorem IsIntegralGenSqrt.coeff_root {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {r : S} {a : R} (h : IsIntegralGenSqrt r a) [Nontrivial R] :

h.coeff r = fun₀ | 1 => 1

@[simp]

theorem IsIntegralGenSqrt.coeff_algebraMap {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {r : S} {a : R} (h : IsIntegralGenSqrt r a) [Nontrivial R] (k : R) :

h.coeff ((algebraMap R S) k) = fun₀ | 0 => k

@[simp]

theorem IsIntegralGenSqrt.coeff_ofNat {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {r : S} {a : R} (h : IsIntegralGenSqrt r a) [Nontrivial R] (n : ℕ) [n.AtLeastTwo] :

h.coeff (OfNat.ofNat n) = fun₀ | 0 => ↑n

theorem IsIntegralGenSqrt.ext_elem {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {r : S} {a : R} (h : IsIntegralGenSqrt r a) [Nontrivial R] ⦃y z : S⦄ (hyz : ∀ i < 2, (h.coeff y) i = (h.coeff z) i) :

y = z

theorem IsIntegralGenSqrt.ext_elem_iff {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {r : S} {a : R} (h : IsIntegralGenSqrt r a) [Nontrivial R] {y z : S} :

y = z ↔ ∀ i < 2, (h.coeff y) i = (h.coeff z) i

theorem IsIntegralGenSqrt.self_eq_coeff {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {r : S} {a : R} (h : IsIntegralGenSqrt r a) [Nontrivial R] (x : S) :

x = (algebraMap R S) ((h.coeff x) 0) + (algebraMap R S) ((h.coeff x) 1) * r

theorem IsIntegralGenSqrt.coeff_of_add_of_mul_root {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {r : S} {a : R} (h : IsIntegralGenSqrt r a) [Nontrivial R] {x y : R} :

h.coeff ((algebraMap R S) x + (algebraMap R S) y * r) = fun₀ | 0 => x | 1 => y

@[simp]

theorem IsIntegralGenSqrt.coeff_mul {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [Nontrivial R] {r : S} {a : R} (h : IsIntegralGenSqrt r a) (x y : S) :

h.coeff (x * y) = fun₀ | 0 => (h.coeff x) 0 * (h.coeff y) 0 + a * (h.coeff x) 1 * (h.coeff y) 1 | 1 => (h.coeff x) 0 * (h.coeff y) 1 + (h.coeff y) 0 * (h.coeff x) 1

@[simp]

theorem IsIntegralGenSqrt.coeff_pow_two {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [Nontrivial R] {r : S} {a : R} (h : IsIntegralGenSqrt r a) (x : S) :

h.coeff (x ^ 2) = fun₀ | 0 => (h.coeff x) 0 ^ 2 + a * (h.coeff x) 1 ^ 2 | 1 => 2 * (h.coeff x) 0 * (h.coeff x) 1

theorem IsIntegralGenSqrt.not_isSquare {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {r : L} {a : K} (h : IsIntegralGenSqrt r a) :

theorem IsIntegralGenSqrt.ne_zero {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {r : L} {a : K} (h : IsIntegralGenSqrt r a) :

a ≠ 0

theorem IsIntegralUnique.of_sqrt {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {a : K} (ha : ¬IsSquare a) {r : L} (h : r ^ 2 = (algebraMap K L) a) :

IsIntegralUnique r (Polynomial.X ^ 2 - Polynomial.C a)

theorem IsQuadraticExtension.isGenerator_of_notMem_bot {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {r : L} [Algebra.IsQuadraticExtension K L] (h : r ∉ ⊥) :

Algebra.IsGenerator K r

theorem IsIntegralGenSqrt.of_sqrt {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {r : L} {a : K} [Algebra.IsQuadraticExtension K L] (h₁ : r ∉ ⊥) (h₂ : r ^ 2 = (algebraMap K L) a) :

IsIntegralGenSqrt r a

theorem Algebra.IsQuadraticExtension.exists_isAdjoinRootMonic_X_pow_two_sub_C {K : Type u_1} (L : Type u_2) [Field K] [Field L] [Algebra K L] [IsQuadraticExtension K L] (hK : ringChar K ≠ 2) :

∃ (a : K), IsAdjoinRootMonic' L (Polynomial.X ^ 2 - Polynomial.C a)

theorem IsIntegralGenSqrt.isSquare_div {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {r₁ r₂ : L} {a₁ a₂ : K} (hK : ringChar K ≠ 2) (h₁ : IsIntegralGenSqrt r₁ a₁) (h₂ : IsIntegralGenSqrt r₂ a₂) :

IsSquare (a₁ / a₂)

theorem IsAdjoinRootMonic'.isSquare_div {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {a₁ a₂ : K} (hK : ringChar K ≠ 2) (h₁ : IsAdjoinRootMonic' L (Polynomial.X ^ 2 - Polynomial.C a₁)) (h₂ : IsAdjoinRootMonic' L (Polynomial.X ^ 2 - Polynomial.C a₂)) :

IsSquare (a₁ / a₂)

theorem IsAdjoinRootMonic'.of_isIntegralGenSqrt_of_isSquare_div {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {r₁ : L} {a₁ a₂ : K} (ha₂ : a₂ ≠ 0) (ha : IsSquare (a₁ / a₂)) (h : IsIntegralGenSqrt r₁ a₁) :

IsAdjoinRootMonic' L (Polynomial.X ^ 2 - Polynomial.C a₂)

theorem IsAdjoinRootMonic'.of_isAdjoinRootMonic_of_isSquare_div {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {a₁ a₂ : K} (ha₂ : a₂ ≠ 0) (ha : IsSquare (a₁ / a₂)) (h : IsAdjoinRootMonic' L (Polynomial.X ^ 2 - Polynomial.C a₁)) :

IsAdjoinRootMonic' L (Polynomial.X ^ 2 - Polynomial.C a₂)

noncomputable def deg_2_classify {K : Type u_1} [Field K] (hK : ringChar K ≠ 2) :

Kˣ ⧸ Subgroup.square Kˣ ≃ { L : IntermediateField K (AlgebraicClosure K) // Algebra.IsQuadraticExtension K ↥L }

Equations

One or more equations did not get rendered due to their size.

Instances For

@[simp]

theorem deg_2_classify_symm_apply {K : Type u_1} [Field K] (hK : ringChar K ≠ 2) (L : { L : IntermediateField K (AlgebraicClosure K) // Algebra.IsQuadraticExtension K ↥L }) :

(deg_2_classify hK).symm L = match L with | ⟨L, hL⟩ => ⟦Units.mk0 (Classical.choose ⋯) ⋯⟧

@[simp]

theorem deg_2_classify_apply {K : Type u_1} [Field K] (hK : ringChar K ≠ 2) (a✝ : Quotient (QuotientGroup.leftRel (Subgroup.square Kˣ))) :

(deg_2_classify hK) a✝ = Quotient.lift (fun (a : Kˣ) => sorry) ⋯ a✝

theorem isSquare_of_isSumSq_of_forall_adjoinRoot_i_isSquare {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (hL : IsAdjoinRootMonic' L (Polynomial.X ^ 2 + 1)) (h : ∀ (x : L), IsSquare x) {a : K} (ha : IsSumSq a) :