Lean4
/-- If `b` mod `p` spans `S/p` as `R/p`-space, then `b` itself spans `Frac(S)` as `K`-space.
Here,
* `p` is an ideal of `R` such that `R / p` is nontrivial
* `K` is a field that has an embedding of `R` (in particular we can take `K = Frac(R)`)
* `L` is a field extension of `K`
* `S` is the integral closure of `R` in `L`
More precisely, we avoid quotients in this statement and instead require that `b ∪ pS` spans `S`.
-/
theorem span_eq_top [IsDomain R] [IsDomain S] [Algebra K L] [Module.Finite R S] [Algebra R L] [IsScalarTower R S L]
[IsScalarTower R K L] [Algebra.IsAlgebraic R S] [NoZeroSMulDivisors R K] (hp : p ≠ ⊤) (b : Set S)
(hb' : Submodule.span R b ⊔ (p.map (algebraMap R S)).restrictScalars R = ⊤) :
Submodule.span K (algebraMap S L '' b) = ⊤ :=
by
have hRL : Function.Injective (algebraMap R L) :=
by
rw [IsScalarTower.algebraMap_eq R K L]
exact
(algebraMap K L).injective.comp
(FaithfulSMul.algebraMap_injective R K)
-- Let `M` be the `R`-module spanned by the proposed basis elements.
let M : Submodule R S := Submodule.span R b
obtain ⟨n, a, ha⟩ :=
@Module.Finite.exists_fin R (S ⧸ M) _ _ _
_
-- Because the image of `p` in `S / M` is `⊤`,
have smul_top_eq : p • (⊤ : Submodule R (S ⧸ M)) = ⊤ := by
calc
p • ⊤ = Submodule.map M.mkQ (p • ⊤) := by rw [Submodule.map_smul'', Submodule.map_top, M.range_mkQ]
_ = ⊤ := by
rw [Ideal.smul_top_eq_map, (Submodule.map_mkQ_eq_top M _).mpr hb']
-- we can write the elements of `a` as `p`-linear combinations of other elements of `a`.
have exists_sum : ∀ x : S ⧸ M, ∃ a' : Fin n → R, (∀ i, a' i ∈ p) ∧ ∑ i, a' i • a i = x :=
by
intro x
obtain ⟨a'', ha'', hx⟩ :=
(Submodule.mem_ideal_smul_span_iff_exists_sum p a x).1
(by { rw [ha, smul_top_eq]; exact Submodule.mem_top
} : x ∈ p • Submodule.span R (Set.range a))
· refine ⟨fun i => a'' i, fun i => ha'' _, ?_⟩
rw [← hx, Finsupp.sum_fintype]
exact fun _ => zero_smul _ _
choose A' hA'p hA' using fun i =>
exists_sum
(a i)
-- This gives us a(n invertible) matrix `A` such that `det A ∈ (M = span R b)`,
let A : Matrix (Fin n) (Fin n) R := Matrix.of A' - 1
let B := A.adjugate
have A_smul : ∀ i, ∑ j, A i j • a j = 0 := by
intros
simp [A, Matrix.sub_apply, Matrix.of_apply, Matrix.one_apply, sub_smul, Finset.sum_sub_distrib, hA', sub_self]
-- since `span S {det A} / M = 0`.
have d_smul : ∀ i, A.det • a i = 0 := by
intro i
calc
A.det • a i = ∑ j, (B * A) i j • a j := ?_
_ = ∑ k, B i k • ∑ j, A k j • a j := ?_
_ = 0 := Finset.sum_eq_zero fun k _ => ?_
·
simp only [B, Matrix.adjugate_mul, Matrix.smul_apply, Matrix.one_apply, smul_eq_mul, ite_true, mul_ite, mul_one,
mul_zero, ite_smul, zero_smul, Finset.sum_ite_eq, Finset.mem_univ]
· simp only [Matrix.mul_apply, Finset.smul_sum, Finset.sum_smul, smul_smul]
rw [Finset.sum_comm]
·
rw [A_smul, smul_zero]
-- In the rings of integers we have the desired inclusion.
have span_d : (Submodule.span S ({algebraMap R S A.det} : Set S)).restrictScalars R ≤ M :=
by
intro x hx
rw [Submodule.restrictScalars_mem] at hx
obtain ⟨x', rfl⟩ := Submodule.mem_span_singleton.mp hx
rw [smul_eq_mul, mul_comm, ← Algebra.smul_def] at hx ⊢
rw [← Submodule.Quotient.mk_eq_zero, Submodule.Quotient.mk_smul]
obtain ⟨a', _, quot_x_eq⟩ := exists_sum (Submodule.Quotient.mk x')
rw [← quot_x_eq, Finset.smul_sum]
conv =>
lhs; congr; next => skip
intro x; rw [smul_comm A.det, d_smul, smul_zero]
exact Finset.sum_const_zero
refine
top_le_iff.mp
(calc
⊤ = (Ideal.span {algebraMap R L A.det}).restrictScalars K := ?_
_ ≤ Submodule.span K (algebraMap S L '' b) := ?_)
-- Because `det A ≠ 0`, we have `span L {det A} = ⊤`.
· rw [eq_comm, Submodule.restrictScalars_eq_top_iff, Ideal.span_singleton_eq_top]
refine IsUnit.mk0 _ ((map_ne_zero_iff (algebraMap R L) hRL).mpr ?_)
refine ne_zero_of_map (f := Ideal.Quotient.mk p) ?_
haveI := Ideal.Quotient.nontrivial hp
calc
Ideal.Quotient.mk p A.det = Matrix.det ((Ideal.Quotient.mk p).mapMatrix A) := by rw [RingHom.map_det]
_ = Matrix.det ((Ideal.Quotient.mk p).mapMatrix (Matrix.of A' - 1)) := rfl
_ = Matrix.det fun i j => (Ideal.Quotient.mk p) (A' i j) - (1 : Matrix (Fin n) (Fin n) (R ⧸ p)) i j := ?_
_ = Matrix.det (-1 : Matrix (Fin n) (Fin n) (R ⧸ p)) := ?_
_ = (-1 : R ⧸ p) ^ n := by rw [Matrix.det_neg, Fintype.card_fin, Matrix.det_one, mul_one]
_ ≠ 0 := IsUnit.ne_zero (isUnit_one.neg.pow _)
· refine congr_arg Matrix.det (Matrix.ext fun i j => ?_)
rw [map_sub, RingHom.mapMatrix_apply, map_one]
rfl
· refine congr_arg Matrix.det (Matrix.ext fun i j => ?_)
rw [Ideal.Quotient.eq_zero_iff_mem.mpr (hA'p i j), zero_sub]
rfl
-- And we conclude `L = span L {det A} ≤ span K b`, so `span K b` spans everything.
· intro x hx
rw [Submodule.restrictScalars_mem, IsScalarTower.algebraMap_apply R S L] at hx
exact IsFractionRing.ideal_span_singleton_map_subset R hRL span_d hx
