def SomeLocalRings.RingHom.StabilizesBaseField {𝕜 : Type u_1} [Field 𝕜] {A : Type u_2} {B : Type u_3} [Ring A] [Ring B] [Algebra 𝕜 A] [Algebra 𝕜 B] (f : A →+* B) : Prop

Definition 2.1. For A and B two 𝕜-algebras, we say that a ring morphism f : A →+* B stabilizes 𝕜 if there exists a field automorphism σ_f : 𝕜 ≃+* 𝕜 such that for all a : 𝕜, f (algebraMap 𝕜 A a) = algebraMap 𝕜 B (σ_f a).

Equations

• SomeLocalRings.RingHom.StabilizesBaseField f = ∃ (σ_f : 𝕜 ≃+* 𝕜), ∀ (a : 𝕜), f ((algebraMap 𝕜 A) a) = (algebraMap 𝕜 B) (σ_f a)

def SomeLocalRings.RingHom.StabilizesBaseFieldWith {𝕜 : Type u_1} [Field 𝕜] {A : Type u_2} {B : Type u_3} [Ring A] [Ring B] [Algebra 𝕜 A] [Algebra 𝕜 B] (f : A →+* B) (σ_f : 𝕜 ≃+* 𝕜) : Prop

A ring morphism f : A →+* B stabilizes 𝕜 with respect to a given automorphism σ_f.

Equations

• SomeLocalRings.RingHom.StabilizesBaseFieldWith f σ_f = ∀ (a : 𝕜), f ((algebraMap 𝕜 A) a) = (algebraMap 𝕜 B) (σ_f a)

noncomputable def SomeLocalRings.RingHom.rangeSubmodule {𝕜 : Type u_1} [Field 𝕜] {A : Type u_2} {B : Type u_3} [Ring A] [Ring B] [Algebra 𝕜 A] [Algebra 𝕜 B] (f : A →+* B) (σ_f : 𝕜 ≃+* 𝕜) (hf : StabilizesBaseFieldWith f σ_f) : Submodule 𝕜 B

Given f : A →+* B stabilizing 𝕜 with respect to σ_f, the range of f is a 𝕜-submodule of B.

This corresponds to the statement that Im(f) is a 𝕜-vector subspace of B.

Equations

• SomeLocalRings.RingHom.rangeSubmodule f σ_f hf = { carrier := Set.range ⇑f, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

theorem SomeLocalRings.exists_submodule_range_eq_of_stabilizesBaseFieldWith {𝕜 : Type u_1} [Field 𝕜] {A : Type u_2} {B : Type u_3} [Ring A] [Ring B] [Algebra 𝕜 A] [Algebra 𝕜 B] (f : A →+* B) (σ_f : 𝕜 ≃+* 𝕜) (hf : RingHom.StabilizesBaseFieldWith f σ_f) : ∃ (V : Submodule 𝕜 B), ↑V = Set.range ⇑f

Proposition 2.2. Let 𝕜 be a field. Let A and B be finite dimensional algebras over 𝕜 and let f : A →+* B be a ring morphism stabilizing 𝕜 with respect to σ_f : 𝕜 ≃+* 𝕜.

1. Im(f) is a 𝕜-vector subspace of B.
2. If f is injective then dim(Im(f)) = dim(A).
3. If f is injective and dim(A) = dim(B) then f is an isomorphism.
4. If f is an isomorphism then f⁻¹ stabilizes 𝕜 and σ_{f⁻¹} = σ_f⁻¹.
5. If f is an isomorphism then dim(A) = dim(B).
6. Let I be a proper ideal of B, and let π : B →+* B ⧸ I be the projection. Then π ∘ f stabilizes 𝕜 and σ_{π ∘ f} = σ_f.
7. Let J be an ideal of A lying in the kernel of f. Then the induced morphism f̄ : A ⧸ J →+* B factorising f stabilizes 𝕜 and σ_{f̄} = σ_f.

theorem SomeLocalRings.finrank_compHom_symm {𝕜 : Type u_1} [Field 𝕜] {A : Type u_2} [Ring A] [Algebra 𝕜 A] [FiniteDimensional 𝕜 A] (σ : 𝕜 ≃+* 𝕜) : Module.finrank 𝕜 A = Module.finrank 𝕜 A

Twisting scalar multiplication by a field automorphism preserves Module.finrank.

theorem SomeLocalRings.finrank_rangeSubmodule_eq_finrank_of_injective {𝕜 : Type u_1} [Field 𝕜] {A : Type u_2} {B : Type u_3} [Ring A] [Ring B] [Algebra 𝕜 A] [Algebra 𝕜 B] [FiniteDimensional 𝕜 A] [FiniteDimensional 𝕜 B] (f : A →+* B) (σ_f : 𝕜 ≃+* 𝕜) (hf : RingHom.StabilizesBaseFieldWith f σ_f) (hinj : Function.Injective ⇑f) : Module.finrank 𝕜 ↥(RingHom.rangeSubmodule f σ_f hf) = Module.finrank 𝕜 A

theorem SomeLocalRings.exists_ringEquiv_of_injective_of_finrank_eq {𝕜 : Type u_1} [Field 𝕜] {A : Type u_2} {B : Type u_3} [Ring A] [Ring B] [Algebra 𝕜 A] [Algebra 𝕜 B] [FiniteDimensional 𝕜 A] [FiniteDimensional 𝕜 B] (f : A →+* B) (σ_f : 𝕜 ≃+* 𝕜) (hf : RingHom.StabilizesBaseFieldWith f σ_f) (hinj : Function.Injective ⇑f) (hfinrank : Module.finrank 𝕜 A = Module.finrank 𝕜 B) : ∃ (e : A ≃+* B), e.toRingHom = f

theorem SomeLocalRings.stabilizesBaseFieldWith_inv_of_ringEquiv {𝕜 : Type u_1} [Field 𝕜] {A : Type u_2} {B : Type u_3} [Ring A] [Ring B] [Algebra 𝕜 A] [Algebra 𝕜 B] (e : A ≃+* B) (σ_e : 𝕜 ≃+* 𝕜) (he : RingHom.StabilizesBaseFieldWith e.toRingHom σ_e) : RingHom.StabilizesBaseFieldWith e.symm.toRingHom σ_e.symm

theorem SomeLocalRings.finrank_eq_of_ringEquiv {𝕜 : Type u_1} [Field 𝕜] {A : Type u_2} {B : Type u_3} [Ring A] [Ring B] [Algebra 𝕜 A] [Algebra 𝕜 B] [FiniteDimensional 𝕜 A] [FiniteDimensional 𝕜 B] (e : A ≃+* B) (σ_e : 𝕜 ≃+* 𝕜) (he : RingHom.StabilizesBaseFieldWith e.toRingHom σ_e) : Module.finrank 𝕜 A = Module.finrank 𝕜 B

theorem SomeLocalRings.stabilizesBaseFieldWith_comp_quotient_mk {𝕜 : Type u_1} [Field 𝕜] {A : Type u_2} {B : Type u_3} [Ring A] [Ring B] [Algebra 𝕜 A] [Algebra 𝕜 B] (f : A →+* B) (σ_f : 𝕜 ≃+* 𝕜) (hf : RingHom.StabilizesBaseFieldWith f σ_f) (I : Ideal B) [I.IsTwoSided] (hI : I ≠ ⊤) : RingHom.StabilizesBaseFieldWith ((Ideal.Quotient.mk I).comp f) σ_f

theorem SomeLocalRings.stabilizesBaseFieldWith_quotientLift {𝕜 : Type u_1} [Field 𝕜] {A : Type u_2} {B : Type u_3} [Ring A] [Ring B] [Algebra 𝕜 A] [Algebra 𝕜 B] (f : A →+* B) (σ_f : 𝕜 ≃+* 𝕜) (hf : RingHom.StabilizesBaseFieldWith f σ_f) (J : Ideal A) [J.IsTwoSided] (hJ : ∀ a ∈ J, f a = 0) : RingHom.StabilizesBaseFieldWith (Ideal.Quotient.lift J f hJ) σ_f

theorem SomeLocalRings.polynomial_mapEquiv_fix_X {𝕜 : Type u_1} [Field 𝕜] (σ : 𝕜 ≃+* 𝕜) : (Polynomial.mapEquiv σ) Polynomial.X = Polynomial.X

Polynomial.mapEquiv fixes the variable X.

theorem SomeLocalRings.polynomial_mapEquiv_stabilizesBaseFieldWith {𝕜 : Type u_1} [Field 𝕜] (σ : 𝕜 ≃+* 𝕜) : RingHom.StabilizesBaseFieldWith (Polynomial.mapEquiv σ).toRingHom σ

Polynomial.mapEquiv stabilizes the base field with the given automorphism.

theorem SomeLocalRings.polynomialRingEquiv_eq_mapEquiv_of_fix_X_of_stabilizesBaseFieldWith {𝕜 : Type u_1} [Field 𝕜] (σ : 𝕜 ≃+* 𝕜) (e : Polynomial 𝕜 ≃+* Polynomial 𝕜) (hX : e Polynomial.X = Polynomial.X) (he : RingHom.StabilizesBaseFieldWith e.toRingHom σ) : e = Polynomial.mapEquiv σ

If a ring automorphism of 𝕜[X] fixes X and acts on the base field 𝕜 by σ, then it is Polynomial.mapEquiv σ.

theorem SomeLocalRings.existsUnique_polynomialRingEquiv_stabilizesBaseFieldWith_fixing_X {𝕜 : Type u_1} [Field 𝕜] (σ : 𝕜 ≃+* 𝕜) : ∃! σX : Polynomial 𝕜 ≃+* Polynomial 𝕜, σX Polynomial.X = Polynomial.X ∧ RingHom.StabilizesBaseFieldWith σX.toRingHom σ

Proposition 2.3. Let 𝕜 be a field and let σ : 𝕜 ≃+* 𝕜 be a field automorphism. Then there is a unique ring automorphism σX : Polynomial 𝕜 ≃+* Polynomial 𝕜 stabilizing 𝕜 with respect to σ such that σX(X) = X.

theorem SomeLocalRings.prop2_4_natDegree_eq {𝕜 : Type u_1} [Field 𝕜] (P₁ P₂ : Polynomial 𝕜) (hP₁ : Irreducible P₁) (hP₂ : Irreducible P₂) (f : Polynomial 𝕜 ⧸ Ideal.span {P₁} ≃+* Polynomial 𝕜 ⧸ Ideal.span {P₂}) (σ_f : 𝕜 ≃+* 𝕜) (hf : RingHom.StabilizesBaseFieldWith f.toRingHom σ_f) : P₁.natDegree = P₂.natDegree

A ring isomorphism 𝕜[X]/(P₁) ≃+* 𝕜[X]/(P₂) stabilizing 𝕜 forces equal natDegree.

theorem SomeLocalRings.quotient_mk_mod_eq_mk {𝕜 : Type u_1} [Field 𝕜] (P p : Polynomial 𝕜) : (Ideal.Quotient.mk (Ideal.span {P})) (p % P) = (Ideal.Quotient.mk (Ideal.span {P})) p

In the quotient by the principal ideal (P), a polynomial and its remainder modulo P agree.

theorem SomeLocalRings.prop2_4_exists_reduced_poly_rep {𝕜 : Type u_1} [Field 𝕜] (P : Polynomial 𝕜) (hP : P.natDegree ≠ 0) (z : Polynomial 𝕜 ⧸ Ideal.span {P}) : ∃ (Q : Polynomial 𝕜), Q.natDegree < P.natDegree ∧ (Ideal.Quotient.mk (Ideal.span {P})) Q = z

Every element of 𝕜[X]⧸(P) has a representative of natDegree < natDegree(P).

theorem SomeLocalRings.prop2_4_unique_reduced_poly_rep {𝕜 : Type u_1} [Field 𝕜] {P Q Q' : Polynomial 𝕜} (hQ : Q.natDegree < P.natDegree) (hQ' : Q'.natDegree < P.natDegree) (h : (Ideal.Quotient.mk (Ideal.span {P})) Q = (Ideal.Quotient.mk (Ideal.span {P})) Q') : Q = Q'

If two polynomials of natDegree < natDegree(P) represent the same element in 𝕜[X]⧸(P), then they are equal.

theorem SomeLocalRings.proposition_2_4 {𝕜 : Type u_1} [Field 𝕜] (P₁ P₂ : Polynomial 𝕜) (hP₁ : Irreducible P₁) (hP₂ : Irreducible P₂) (f : Polynomial 𝕜 ⧸ Ideal.span {P₁} ≃+* Polynomial 𝕜 ⧸ Ideal.span {P₂}) (σ_f : 𝕜 ≃+* 𝕜) (hf : RingHom.StabilizesBaseFieldWith f.toRingHom σ_f) : P₁.natDegree = P₂.natDegree ∧ have σX := Classical.choose ⋯; ∃! Qf : Polynomial 𝕜, Qf.natDegree < P₁.natDegree ∧ ∃ (fX : Polynomial 𝕜 →+* Polynomial 𝕜), fX Polynomial.X = Qf ∧ RingHom.StabilizesBaseFieldWith fX σ_f ∧ (∀ (P : Polynomial 𝕜), fX P = (σX P).comp Qf) ∧ (∃ (hIJ : Ideal.span {P₁} ≤ Ideal.comap fX (Ideal.span {P₂})), Ideal.quotientMap (Ideal.span {P₂}) fX hIJ = f.toRingHom) ∧ (∃ (Sf : Polynomial 𝕜), (σX P₁).comp Qf = Sf * P₂) ∧ (∀ (P : Polynomial 𝕜), (∃ (S : Polynomial 𝕜), (σX P).comp Qf = S * P₂) → ∃ (R : Polynomial 𝕜), P = R * P₁) ∧ ∀ (n : ℕ), ∃ (hIJn : Ideal.span {P₁ ^ n} ≤ Ideal.comap fX (Ideal.span {P₂ ^ n})), RingHom.StabilizesBaseFieldWith (Ideal.quotientMap (Ideal.span {P₂ ^ n}) fX hIJn) σ_f

Proposition 2.4. Assume 𝕜 is a field and P₁, P₂ are irreducible polynomials in 𝕜[X]. Let f : 𝕜[X]/(P₁) ≃+* 𝕜[X]/(P₂) be a ring isomorphism stabilizing 𝕜 with respect to σ_f.

1. deg(P₁) = deg(P₂).
2. There exists a unique polynomial Q_f ∈ 𝕜[X] with 1 ≤ deg(Q_f) < deg(P₁) such that f is induced by a ring morphism f_X : 𝕜[X] →+* 𝕜[X] stabilizing 𝕜 with respect to σ_f and given by P ↦ σ_f^X(P) ∘ Q_f, where σ_f^X is as in Proposition 2.3.
3. σ_f^X(P₁) ∘ Q_f = S_f * P₂ for some polynomial S_f.
4. If σ_f^X(P) ∘ Q_f = S * P₂ then P = R * P₁.
5. The morphism f_X maps (P₁^n) into (P₂^n) and hence induces f_{X,n} : 𝕜[X]/(P₁^n) →+* 𝕜[X]/(P₂^n) stabilizing 𝕜.

theorem SomeLocalRings.prop2_5_dvd_P1_of_dvd_P2_fX {𝕜 : Type u_1} [Field 𝕜] (P₁ P₂ : Polynomial 𝕜) (f : Polynomial 𝕜 ⧸ Ideal.span {P₁} ≃+* Polynomial 𝕜 ⧸ Ideal.span {P₂}) (fX : Polynomial 𝕜 →+* Polynomial 𝕜) (hIJ : Ideal.span {P₁} ≤ Ideal.comap fX (Ideal.span {P₂})) (hf_ind : Ideal.quotientMap (Ideal.span {P₂}) fX hIJ = f.toRingHom) (P : Polynomial 𝕜) : P₂ ∣ fX P → P₁ ∣ P

If P₂ ∣ fX P, then P₁ ∣ P (using injectivity of the induced map on (P₁)-quotients).

theorem SomeLocalRings.prop2_5_pow_dvd_P1_of_pow_dvd_P2_fX {𝕜 : Type u_1} [Field 𝕜] (P₁ P₂ : Polynomial 𝕜) (hP₂ : Irreducible P₂) (f : Polynomial 𝕜 ⧸ Ideal.span {P₁} ≃+* Polynomial 𝕜 ⧸ Ideal.span {P₂}) (fX : Polynomial 𝕜 →+* Polynomial 𝕜) (hIJ : Ideal.span {P₁} ≤ Ideal.comap fX (Ideal.span {P₂})) (hf_ind : Ideal.quotientMap (Ideal.span {P₂}) fX hIJ = f.toRingHom) (Sf : Polynomial 𝕜) (hSf : fX P₁ = Sf * P₂) : IsCoprime Sf P₂ → ∀ (k : ℕ) (P : Polynomial 𝕜), P₂ ^ k ∣ fX P → P₁ ^ k ∣ P

If S_f is coprime to P₂, then divisibility of fX(P) by P₂^k forces divisibility of P by P₁^k.

theorem SomeLocalRings.prop2_5_injective_quotientMap_pow {𝕜 : Type u_1} [Field 𝕜] (P₁ P₂ : Polynomial 𝕜) (hP₂ : Irreducible P₂) (f : Polynomial 𝕜 ⧸ Ideal.span {P₁} ≃+* Polynomial 𝕜 ⧸ Ideal.span {P₂}) (fX : Polynomial 𝕜 →+* Polynomial 𝕜) (hIJ : Ideal.span {P₁} ≤ Ideal.comap fX (Ideal.span {P₂})) (hf_ind : Ideal.quotientMap (Ideal.span {P₂}) fX hIJ = f.toRingHom) (Sf : Polynomial 𝕜) (hSf : fX P₁ = Sf * P₂) (n : ℕ) (hIJn : Ideal.span {P₁ ^ n} ≤ Ideal.comap fX (Ideal.span {P₂ ^ n})) : IsCoprime Sf P₂ → Function.Injective ⇑(Ideal.quotientMap (Ideal.span {P₂ ^ n}) fX hIJn)

Injectivity of the induced map f_{X,n} under the coprimality hypothesis.

theorem SomeLocalRings.prop2_5_exists_ringEquiv_of_isCoprime {𝕜 : Type u_1} [Field 𝕜] (P₁ P₂ : Polynomial 𝕜) (hP₁ : Irreducible P₁) (hP₂ : Irreducible P₂) (f : Polynomial 𝕜 ⧸ Ideal.span {P₁} ≃+* Polynomial 𝕜 ⧸ Ideal.span {P₂}) (σ_f : 𝕜 ≃+* 𝕜) (hf : RingHom.StabilizesBaseFieldWith f.toRingHom σ_f) (fX : Polynomial 𝕜 →+* Polynomial 𝕜) (hfX : RingHom.StabilizesBaseFieldWith fX σ_f) (hIJ : Ideal.span {P₁} ≤ Ideal.comap fX (Ideal.span {P₂})) (hf_ind : Ideal.quotientMap (Ideal.span {P₂}) fX hIJ = f.toRingHom) (Sf : Polynomial 𝕜) (hSf : fX P₁ = Sf * P₂) (n : ℕ) (hIJn : Ideal.span {P₁ ^ n} ≤ Ideal.comap fX (Ideal.span {P₂ ^ n})) : IsCoprime Sf P₂ → ∃ (e : Polynomial 𝕜 ⧸ Ideal.span {P₁ ^ n} ≃+* Polynomial 𝕜 ⧸ Ideal.span {P₂ ^ n}), e.toRingHom = Ideal.quotientMap (Ideal.span {P₂ ^ n}) fX hIJn

If S_f is coprime to P₂, then the induced map f_{X,n} : 𝕜[X]/(P₁^n) → 𝕜[X]/(P₂^n) is an isomorphism.