FiniteDescent.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Finite-dimensional descent over algebraic central scalar extensions. This does not construct the Kurosh counterexample. All coefficient fields and finite spanning spaces below are constructed. No assumption supplies a descended multiplication table or generating span.

theorem OAI.Kurosh022.finite_descent_two_generators line 22

Source documentation

Finite descent over an algebraic central scalar extension. The target algebra may be noncommutative. Coordinates of one are included explicitly, so the chosen finite basis need not have first vector one.

theorem finite_descent_two_generators
    (K F D : Type*) [Field K] [Field F] [Ring D]
    [Algebra K F] [Algebra F D] [Algebra K D] [IsScalarTower K F D]
    [Algebra.IsAlgebraic K F] [FiniteDimensional F D]
    (x y : D) (hgen : Algebra.adjoin K ({x, y} : Set D) = ⊤) :
    FiniteDimensional K D := by
…

theorem OAI.Kurosh022.finite_over_actual_center_descends line 93

Source documentation

The actual-center specialization; Subring.center D is the native center, not an abstract nominated scalar field or an assumed finite descent witness.

theorem finite_over_actual_center_descends
    (K D : Type*) [Field K] [DivisionRing D] [Algebra K D]
    [Algebra.IsAlgebraic K D] [FiniteDimensional (Subring.center D) D]
    (x y : D) (hgen : Algebra.adjoin K ({x, y} : Set D) = ⊤) :
    FiniteDimensional K D := by
…