English
Under a setting with integral closure S of R in a finite extension L, the Finite rank identity relates finrank of quotients to finrank of the extension L/K, connecting algebraic and analytic ranks.
Русский
При замыкании S над R в конечном расширении L связь между финrank и размерностями остаётся через фракции.
LaTeX
$$$\\\\operatorname{finrank}_{R} (S) = \\,\\\\operatorname{finrank}_{K} (L)$$$
Lean4
/-- If `p` is a maximal ideal of `R`, and `S` is the integral closure of `R` in `L`,
then the dimension `[S/pS : R/p]` is equal to `[Frac(S) : Frac(R)]`. -/
theorem finrank_quotient_map [IsDomain S] [IsDedekindDomain R] [Algebra K L] [Algebra R L] [IsScalarTower R K L]
[IsScalarTower R S L] [hp : p.IsMaximal] [Module.Finite R S] :
finrank (R ⧸ p) (S ⧸ map (algebraMap R S) p) = finrank K L := by
-- Choose an arbitrary basis `b` for `[S/pS : R/p]`.
-- We'll use the previous results to turn it into a basis on `[Frac(S) : Frac(R)]`.
let ι := Module.Free.ChooseBasisIndex (R ⧸ p) (S ⧸ map (algebraMap R S) p)
let b : Basis ι (R ⧸ p) (S ⧸ map (algebraMap R S) p) :=
Module.Free.chooseBasis _
_
-- Namely, choose a representative `b' i : S` for each `b i : S / pS`.
let b' : ι → S := fun i => (Ideal.Quotient.mk_surjective (b i)).choose
have b_eq_b' : ⇑b = (Submodule.mkQ (map (algebraMap R S) p)).restrictScalars R ∘ b' :=
funext fun i => (Ideal.Quotient.mk_surjective (b i)).choose_spec.symm
let b'' : ι → L := algebraMap S L ∘ b'
have b''_li : LinearIndependent K b'' := ?_
· have b''_sp : Submodule.span K (Set.range b'') = ⊤ :=
?_
-- Since the two bases have the same index set, the spaces have the same dimension.
· let c : Basis ι K L := Basis.mk b''_li b''_sp.ge
rw [finrank_eq_card_basis b, finrank_eq_card_basis c]
-- It remains to show that the basis is indeed linear independent and spans the whole space.
· rw [Set.range_comp]
refine
FinrankQuotientMap.span_eq_top p hp.ne_top _
(top_le_iff.mp ?_)
-- The nicest way to show `S ≤ span b' ⊔ pS` is by reducing both sides modulo pS.
-- However, this would imply distinguishing between `pS` as `S`-ideal,
-- and `pS` as `R`-submodule, since they have different (non-defeq) quotients.
-- Instead we'll lift `x mod pS ∈ span b` to `y ∈ span b'` for some `y - x ∈ pS`.
intro x _
have mem_span_b :
((Submodule.mkQ (map (algebraMap R S) p)) x : S ⧸ map (algebraMap R S) p) ∈
Submodule.span (R ⧸ p) (Set.range b) :=
b.mem_span _
rw [← @Submodule.restrictScalars_mem R, Submodule.restrictScalars_span R (R ⧸ p) Ideal.Quotient.mk_surjective,
b_eq_b', Set.range_comp, ← Submodule.map_span] at mem_span_b
obtain ⟨y, y_mem, y_eq⟩ := Submodule.mem_map.mp mem_span_b
suffices y + -(y - x) ∈ _ by simpa
rw [LinearMap.restrictScalars_apply, Submodule.mkQ_apply, Submodule.mkQ_apply, Submodule.Quotient.eq] at y_eq
exact add_mem (Submodule.mem_sup_left y_mem) (neg_mem <| Submodule.mem_sup_right y_eq)
· have := b.linearIndependent; rw [b_eq_b'] at this
convert
FinrankQuotientMap.linearIndependent_of_nontrivial K _ ((Algebra.linearMap S L).restrictScalars R) _
((Submodule.mkQ _).restrictScalars R) this
· rw [Quotient.algebraMap_eq, Ideal.mk_ker]
exact hp.ne_top
· exact IsFractionRing.injective S L
