Intermediate fields #
Let L / K
be a field extension, given as an instance algebra K L
.
This file defines the type of fields in between K
and L
, intermediate_field K L
.
An intermediate_field K L
is a subfield of L
which contains (the image of) K
,
i.e. it is a subfield L
and a subalgebra K L
.
Main definitions #
-
intermediate_field K L
: the type of intermediate fields betweenK
andL
. -
subalgebra.to_intermediate_field
: turns a subalgebra closed under⁻¹
into an intermediate field -
subfield.to_intermediate_field
: turns a subfield containing the image ofK
into an intermediate field -
intermediate_field.map
: map an intermediate field along analg_hom
Implementation notes #
Intermediate fields are defined with a structure extending subfield
and subalgebra
.
A subalgebra
is closed under all operations except ⁻¹
,
Tags #
intermediate field, field extension
Reinterpret an intermediate_field
as a subalgebra
.
- carrier : set L
- one_mem' : 1 ∈ c.carrier
- mul_mem' : ∀ {a b : L}, a ∈ c.carrier → b ∈ c.carrier → a * b ∈ c.carrier
- zero_mem' : 0 ∈ c.carrier
- add_mem' : ∀ {a b : L}, a ∈ c.carrier → b ∈ c.carrier → a + b ∈ c.carrier
- algebra_map_mem' : ∀ (r : K), ⇑(algebra_map K L) r ∈ c.carrier
- neg_mem' : ∀ {x : L}, x ∈ c.carrier → -x ∈ c.carrier
- inv_mem' : ∀ (x : L), x ∈ c.carrier → x⁻¹ ∈ c.carrier
S : intermediate_field K L
is a subset of L
such that there is a field
tower L / S / K
.
Reinterpret an intermediate_field
as a subfield
.
Equations
Equations
- intermediate_field.has_coe_to_sort = {S := Type u_2, coe := λ (S : intermediate_field K L), ↥(S.carrier)}
Equations
- intermediate_field.has_mem = {mem := λ (m : L) (S : intermediate_field K L), m ∈ ↑S}
Two intermediate fields are equal if the underlying subsets are equal.
Two intermediate fields are equal if they have the same elements.
An intermediate field contains the image of the smaller field.
An intermediate field contains the ring's 1.
An intermediate field contains the ring's 0.
An intermediate field is closed under multiplication.
An intermediate field is closed under scalar multiplication.
An intermediate field is closed under addition.
An intermediate field is closed under subtraction
An intermediate field is closed under negation.
An intermediate field is closed under inverses.
An intermediate field is closed under division.
Sum of a multiset of elements in a intermediate_field
is in the intermediate_field
.
Product of elements of an intermediate field indexed by a finset
is in the intermediate_field.
Sum of elements in a 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
An intermediate field inherits a field structure
Equations
- S.to_field = S.to_subfield.to_field
Equations
- S.algebra = S.to_subalgebra.algebra
Equations
If f : L →+* L'
fixes K
, S.map f
is the intermediate field between L'
and K
such that x ∈ S ↔ f x ∈ S.map f
.
The embedding from an intermediate field of L / K
to L
.
Equations
- S.val = S.to_subalgebra.val
Equations
- intermediate_field.partial_order = {le := λ (S T : intermediate_field K L), ↑S ⊆ ↑T, lt := preorder.lt._default (λ (S T : intermediate_field K L), ↑S ⊆ ↑T), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}
Lift an intermediate_field of an intermediate_field
Lift an intermediate_field of an intermediate_field
Equations
Equations
Equations
- intermediate_field.lift2_alg = {to_has_scalar := {smul := λ (a : K) (b : ↥E), (⇑((algebra_map ↥F ↥E).comp (algebra_map K ↥F)) a) * b}, to_ring_hom := {to_fun := ⇑((algebra_map ↥F ↥E).comp (algebra_map K ↥F)), map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}, commutes' := _, smul_def' := _}
lift2
is isomorphic to the original intermediate_field
.
If L/K
is algebraic, the K
-subalgebras of L
are all fields.
Equations
- subalgebra_equiv_intermediate_field alg = {to_equiv := {to_fun := λ (S : subalgebra K L), S.to_intermediate_field _, inv_fun := λ (S : intermediate_field K L), S.to_subalgebra, left_inv := _, right_inv := _}, map_rel_iff' := _}