Intermediate fields #
L / K be a field extension, given as an instance
algebra K L.
This file defines the type of fields in between
intermediate_field K L.
intermediate_field K L is a subfield of
L which contains (the image of)
i.e. it is a
subfield L and a
subalgebra K L.
Main definitions #
intermediate_field K L: the type of intermediate fields between
subalgebra.to_intermediate_field: turns a subalgebra closed under
⁻¹into an intermediate field
subfield.to_intermediate_field: turns a subfield containing the image of
Kinto an intermediate field
Implementation notes #
intermediate field, field extension
- to_subalgebra : subalgebra K L
- neg_mem' : ∀ (x : L), x ∈ self.to_subalgebra.carrier → -x ∈ self.to_subalgebra.carrier
- inv_mem' : ∀ (x : L), x ∈ self.to_subalgebra.carrier → x⁻¹ ∈ self.to_subalgebra.carrier
S : intermediate_field K L is a subset of
L such that there is a field
L / S / K.
Copy of an intermediate field with a new
carrier equal to the old one. Useful to fix
Product of elements of an intermediate field indexed by a
finset is in the intermediate_field.
Turn a subalgebra closed under inverses into an intermediate field
Turn a subfield of
L containing the image of
K into an intermediate field
f : L →+* L' fixes
S.map f is the intermediate field between
x ∈ S ↔ f x ∈ S.map f.
Lift an intermediate_field of an intermediate_field
L/K is algebraic, the
L are all fields.