Documentation

TauCeti.FieldTheory.IntermediateField.Lift

Intermediate fields of an intermediate field #

For E an intermediate field of L / F, the intermediate fields of E / F are the intermediate fields of L / F lying below E. Mathlib supplies the two maps — IntermediateField.lift and IntermediateField.restrict — and one of the two round trips (lift_restrict). This file adds the other round trip and the order-embedding statement, and packages them as an order isomorphism

IntermediateField F E ≃o Set.Iic E.

Having the correspondence as a single OrderIso rather than as a pair of monotone maps is what lets it be composed with the Galois correspondence, which is also an OrderIso; that composition is the subfield dictionary of TauCeti/FieldTheory/Galois/SubfieldDictionary.lean.

Main results #

source
@[simp]
theorem IntermediateField.restrict_lift {F : Type u_1} {L : Type u_2} [Field F] [Field L] [Algebra F L] {E : IntermediateField F L} (E' : IntermediateField F ↥E) :
restrict ⋯ = E'

Restricting a lifted intermediate field recovers it. This is the round trip complementary to Mathlib's lift_restrict.

source
@[simp]
theorem IntermediateField.lift_le_lift_iff {F : Type u_1} {L : Type u_2} [Field F] [Field L] [Algebra F L] {E : IntermediateField F L} {a b : IntermediateField F ↥E} :
lift a ≤ lift b ↔ a ≤ b

lift reflects the order. Monotonicity alone would only give one direction; the converse is what makes liftOrderIso an order isomorphism rather than a monotone bijection.

source
def IntermediateField.liftOrderIso {F : Type u_1} {L : Type u_2} [Field F] [Field L] [Algebra F L] (E : IntermediateField F L) :
IntermediateField F ↥E ≃o ↑(Set.Iic E)

The intermediate fields of E / F are the intermediate fields of L / F below E, as an order isomorphism. liftOrderIso_apply and liftOrderIso_symm_apply are the evaluation rules downstream files use; the body is definitional only inside this module.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem IntermediateField.liftOrderIso_apply {F : Type u_1} {L : Type u_2} [Field F] [Field L] [Algebra F L] {E : IntermediateField F L} (E' : IntermediateField F ↥E) :
    ↑(E.liftOrderIso E') = lift E'
    source
    @[simp]
    theorem IntermediateField.liftOrderIso_symm_apply {F : Type u_1} {L : Type u_2} [Field F] [Field L] [Algebra F L] {E : IntermediateField F L} (E' : ↑(Set.Iic E)) :
    E.liftOrderIso.symm E' = restrict ⋯