Discriminant fields under base-field isomorphisms

Compatible ring isomorphisms e : F ≃+* F' and τ : E ≃+* E' carry the discriminant field of f : F[X] in E onto that of f.map e in E'. This compares extensions with different base fields, whereas TauCeti.discrField_map compares extensions over the same base field.

The image equality TauCeti.discrField_map_ringEquiv is stated using subfields: the two intermediate fields have different base types, so IntermediateField.map does not apply. TauCeti.discrFieldRingEquiv restricts the ambient isomorphism to these fields and commutes with the base isomorphism. No square root needs to be chosen, and the result includes the cases of a zero or square discriminant, characteristic two, and ambient fields containing no square root.

The construction uses the discriminant base-change identity and Mathlib's Subring.equivMapOfInjective to restrict the ambient isomorphism.

theorem TauCeti.discrField_map_ringEquiv {F : Type u_1} {F' : Type u_2} {E : Type u_3} {E' : Type u_4} [Field F] [Field F'] [Field E] [Field E'] [Algebra F E] [Algebra F' E'] {f : Polynomial F} {e : F ≃+* F'} {τ : E ≃+* E'} (hcomm : (↑τ).comp (algebraMap F E) = (algebraMap F' E').comp ↑e) : Subfield.map (↑τ) (discrField f E).toSubfield = (discrField (Polynomial.map (↑e) f) E').toSubfield

Compatible isomorphisms of the base and ambient fields carry the discriminant field onto that of the polynomial with transported coefficients.

noncomputable def TauCeti.discrFieldRingEquiv {F : Type u_1} {F' : Type u_2} {E : Type u_3} {E' : Type u_4} [Field F] [Field F'] [Field E] [Field E'] [Algebra F E] [Algebra F' E'] {f : Polynomial F} {e : F ≃+* F'} {τ : E ≃+* E'} (hcomm : (↑τ).comp (algebraMap F E) = (algebraMap F' E').comp ↑e) : ↥(discrField f E) ≃+* ↥(discrField (Polynomial.map (↑e) f) E')

The restriction of a compatible ambient isomorphism to the discriminant fields. It lies over the given base-field isomorphism, as expressed by TauCeti.discrFieldRingEquiv_algebraMap.

Equations

• TauCeti.discrFieldRingEquiv hcomm = ((TauCeti.discrField f E).toSubfield.equivMapOfInjective ↑τ ⋯).trans (RingEquiv.subfieldCongr ⋯)

@[simp]

theorem TauCeti.discrFieldRingEquiv_apply {F : Type u_1} {F' : Type u_2} {E : Type u_3} {E' : Type u_4} [Field F] [Field F'] [Field E] [Field E'] [Algebra F E] [Algebra F' E'] {f : Polynomial F} {e : F ≃+* F'} {τ : E ≃+* E'} (hcomm : (↑τ).comp (algebraMap F E) = (algebraMap F' E').comp ↑e) (x : ↥(discrField f E)) : ↑((discrFieldRingEquiv hcomm) x) = τ ↑x

On elements, the induced isomorphism is the ambient isomorphism.

@[simp]

theorem TauCeti.discrFieldRingEquiv_symm_apply {F : Type u_1} {F' : Type u_2} {E : Type u_3} {E' : Type u_4} [Field F] [Field F'] [Field E] [Field E'] [Algebra F E] [Algebra F' E'] {f : Polynomial F} {e : F ≃+* F'} {τ : E ≃+* E'} (hcomm : (↑τ).comp (algebraMap F E) = (algebraMap F' E').comp ↑e) (x : ↥(discrField (Polynomial.map (↑e) f) E')) : ↑((discrFieldRingEquiv hcomm).symm x) = τ.symm ↑x

The inverse induced isomorphism is the inverse ambient isomorphism.

@[simp]

theorem TauCeti.discrFieldRingEquiv_algebraMap {F : Type u_1} {F' : Type u_2} {E : Type u_3} {E' : Type u_4} [Field F] [Field F'] [Field E] [Field E'] [Algebra F E] [Algebra F' E'] {f : Polynomial F} {e : F ≃+* F'} {τ : E ≃+* E'} (hcomm : (↑τ).comp (algebraMap F E) = (algebraMap F' E').comp ↑e) (x : F) : (discrFieldRingEquiv hcomm) ((algebraMap F ↥(discrField f E)) x) = (algebraMap F' ↥(discrField (Polynomial.map (↑e) f) E')) (e x)

The discriminant-field isomorphism commutes with the base-field isomorphism.

@[simp]

theorem TauCeti.discrFieldRingEquiv_symm_algebraMap {F : Type u_1} {F' : Type u_2} {E : Type u_3} {E' : Type u_4} [Field F] [Field F'] [Field E] [Field E'] [Algebra F E] [Algebra F' E'] {f : Polynomial F} {e : F ≃+* F'} {τ : E ≃+* E'} (hcomm : (↑τ).comp (algebraMap F E) = (algebraMap F' E').comp ↑e) (x : F') : (discrFieldRingEquiv hcomm).symm ((algebraMap F' ↥(discrField (Polynomial.map (↑e) f) E')) x) = (algebraMap F ↥(discrField f E)) (e.symm x)

The inverse discriminant-field isomorphism commutes with the inverse base isomorphism.