English
The union of a chain of lifts exists and itself forms a lift, provided the ambient algebraic setting holds.
Русский
Объединение цепи Lift существует и образует lift в условиях заданной алгебраической структуры.
LaTeX
$$$\text{union}(c,\,\text{hc}) : \text{Lifts } F E K$ is a lift when $c$ is a chain.$$
Lean4
/-- `σ : L →ₐ[F] K` is an extendible lift ("extendible pair" in [Isaacs1980]) if for every
intermediate field `M` that is finite-dimensional over `L`, `σ` extends to some `M →ₐ[F] K`.
In our definition we only require `M` to be finitely generated over `L`, which is equivalent
if the ambient field `E` is algebraic over `F` (which is the case in our main application).
We also allow the domain of the extension to be an intermediate field that properly contains `M`,
since one can always restrict the domain to `M`. -/
def IsExtendible (σ : Lifts F E K) : Prop :=
∀ S : Finset E, ∃ τ ≥ σ, (S : Set E) ⊆ τ.carrier
