Documentation

TauCeti.NumberTheory.NumberField.RingOfIntegers.Transport

Transporting ideals of a ring of integers along an isomorphism of fields #

An isomorphism of fields e : K ≃+* L restricts to NumberField.RingOfIntegers.mapRingEquiv e between the rings of integers, and pulling ideals back along it identifies the ideals of 𝓞 L with those of 𝓞 K. This file records that this identification is functorial and reflects the zero ideal, which is what a construction transported along e needs in order to be well defined on nonzero ideals.

Main results #

source
@[simp]
theorem NumberField.RingOfIntegers.mapRingEquiv_refl_apply {K : Type u_1} [Field K] (x : RingOfIntegers K) :
(mapRingEquiv (RingEquiv.refl K)) x = x

The identity isomorphism of fields restricts to the identity on integers.

source
@[simp]
theorem NumberField.RingOfIntegers.mapRingEquiv_trans_apply {K : Type u_1} {L : Type u_2} {M : Type u_3} [Field K] [Field L] [Field M] (e : K ≃+* L) (e' : L ≃+* M) (x : RingOfIntegers K) :
(mapRingEquiv e') ((mapRingEquiv e) x) = (mapRingEquiv (e.trans e')) x

Restricting to integers is compatible with composing isomorphisms of fields.

source
@[simp]
theorem Ideal.comap_mapRingEquiv_refl {K : Type u_1} [Field K] (I : Ideal (NumberField.RingOfIntegers K)) :
comap (NumberField.RingOfIntegers.mapRingEquiv (RingEquiv.refl K)) I = I

Pulling back along the identity isomorphism is the identity on ideals.

source
@[simp]
theorem Ideal.comap_mapRingEquiv_trans {K : Type u_1} {L : Type u_2} {M : Type u_3} [Field K] [Field L] [Field M] (I : Ideal (NumberField.RingOfIntegers M)) (e : K ≃+* L) (e' : L ≃+* M) :
comap (NumberField.RingOfIntegers.mapRingEquiv e) (comap (NumberField.RingOfIntegers.mapRingEquiv e') I) = comap (NumberField.RingOfIntegers.mapRingEquiv (e.trans e')) I

Pulling back along e and then e' is pulling back along e.trans e'.

source
@[simp]
theorem Ideal.comap_mapRingEquiv_eq_bot_iff {K : Type u_1} {L : Type u_2} [Field K] [Field L] (I : Ideal (NumberField.RingOfIntegers L)) (e : K ≃+* L) :
comap (NumberField.RingOfIntegers.mapRingEquiv e) I = ⊥ ↔ I = ⊥

The pullback of an ideal along an isomorphism of fields is the zero ideal exactly when the ideal is. This is what keeps a transported construction on the nonzero ideals.