English
If A and L are linearly disjoint over F and A is algebraic over F, then a certain lifted rank equality holds between adjoin constructions and extensions to F.
Русский
Если A и L линейно независимы над F и A алгебраично над F, тогда существует соответствующая тождественная равенство рангов после тильдов для адъюнктов и расширений.
LaTeX
$$$\text{lifted rank equality}$$$
Lean4
/-- If `A` and `L` are linearly disjoint over `F`, one of them is algebraic,
then `[L(A) : A] = [L : F]`. Note that in Lean `L(A)` is not naturally an `A`-algebra,
so this result is stated in a cumbersome way. -/
theorem lift_adjoin_rank_eq_lift_rank_right_of_isAlgebraic (H : A.LinearDisjoint L)
(halg : Algebra.IsAlgebraic F A ∨ Algebra.IsAlgebraic F L) :
Cardinal.lift.{w}
(Module.rank A
(extendScalars (show A ≤ (adjoin L (A : Set E)).restrictScalars F from subset_adjoin L (A : Set E)))) =
Cardinal.lift.{v} (Module.rank F L) :=
by
rw [(AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)).toLinearEquiv.lift_rank_eq, Cardinal.lift_inj, ←
Subalgebra.LinearDisjoint.adjoin_rank_eq_rank_right H]
set L' := (IsScalarTower.toAlgHom F L E).range
have heq : (adjoin L (A : Set E)).toSubalgebra.toSubsemiring = (Algebra.adjoin A (L' : Set E)).toSubsemiring :=
by
rw [adjoin_toSubalgebra_of_isAlgebraic _ _ halg.symm, Algebra.adjoin_toSubsemiring, Algebra.adjoin_toSubsemiring,
Set.union_comm]
congr 2
ext x
simp
refine
rank_eq_of_equiv_equiv (RingHom.id A) (RingEquiv.subsemiringCongr heq).toAddEquiv Function.bijective_id
fun ⟨a, ha⟩ ⟨x, hx⟩ ↦ ?_
ext
simp_rw [Algebra.smul_def]
rfl
