Lean4
@[stacks 0561]
theorem of_restrict_scalars_finitePresentation [Algebra A B] [IsScalarTower R A B] [FinitePresentation.{w₁, w₃} R B]
[FiniteType R A] : FinitePresentation.{w₂, w₃} A B := by
classical
obtain ⟨n, f, hf, s, hs⟩ := FinitePresentation.out (R := R) (A := B)
letI RX := MvPolynomial (Fin n) R
letI AX := MvPolynomial (Fin n) A
refine ⟨n, MvPolynomial.aeval (f ∘ X), ?_, ?_⟩
· rw [← AlgHom.range_eq_top, ← Algebra.adjoin_range_eq_range_aeval, Set.range_comp f MvPolynomial.X, eq_top_iff, ←
@adjoin_adjoin_of_tower R A B, adjoin_image, adjoin_range_X, Algebra.map_top, (AlgHom.range_eq_top _).mpr hf]
exact fun {x} => subset_adjoin ⟨⟩
· obtain ⟨t, ht⟩ := FiniteType.out (R := R) (A := A)
have := fun i : t => hf (algebraMap A B i)
choose t' ht' using this
have ht'' : Algebra.adjoin R (algebraMap A AX '' t ∪ Set.range (X : _ → AX)) = ⊤ :=
by
rw [adjoin_union_eq_adjoin_adjoin, ←
Subalgebra.restrictScalars_top R (A := AX) (S := { x // x ∈ adjoin R ((algebraMap A AX) '' t) })]
refine congrArg (Subalgebra.restrictScalars R) ?_
rw [adjoin_algebraMap, ht]
apply Subalgebra.restrictScalars_injective R
rw [← adjoin_restrictScalars, adjoin_range_X, Subalgebra.restrictScalars_top, Subalgebra.restrictScalars_top]
letI g : t → AX := fun x => MvPolynomial.C (x : A) - map (algebraMap R A) (t' x)
refine ⟨s.image (map (algebraMap R A)) ∪ t.attach.image g, ?_⟩
rw [Finset.coe_union, Finset.coe_image, Finset.coe_image, Finset.attach_eq_univ, Finset.coe_univ, Set.image_univ]
let s₀ := (MvPolynomial.map (algebraMap R A)) '' s ∪ Set.range g
let I := RingHom.ker (MvPolynomial.aeval (R := A) (f ∘ MvPolynomial.X))
change Ideal.span s₀ = I
have leI :
Ideal.span ((MvPolynomial.map (algebraMap R A)) '' s ∪ Set.range g) ≤
RingHom.ker (MvPolynomial.aeval (R := A) (f ∘ MvPolynomial.X)) :=
by
rw [Ideal.span_le]
rintro _ (⟨x, hx, rfl⟩ | ⟨⟨x, hx⟩, rfl⟩) <;> rw [SetLike.mem_coe, RingHom.mem_ker]
· rw [MvPolynomial.aeval_map_algebraMap (R := R) (A := A), ← aeval_unique]
have := Ideal.subset_span hx
rwa [hs] at this
·
rw [map_sub, MvPolynomial.aeval_map_algebraMap, ← aeval_unique, MvPolynomial.aeval_C, ht', Subtype.coe_mk,
sub_self]
apply leI.antisymm
intro x hx
rw [RingHom.mem_ker] at hx
let s₀ := (MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
change x ∈ Ideal.span s₀
have : x ∈ (MvPolynomial.map (algebraMap R A) : _ →+* AX).range.toAddSubmonoid ⊔ (Ideal.span s₀).toAddSubmonoid :=
by
have : x ∈ (⊤ : Subalgebra R AX) := trivial
rw [← ht''] at this
refine adjoin_induction ?_ ?_ ?_ ?_ this
· rintro _ (⟨x, hx, rfl⟩ | ⟨i, rfl⟩)
· rw [MvPolynomial.algebraMap_eq, ← sub_add_cancel (MvPolynomial.C x) (map (algebraMap R A) (t' ⟨x, hx⟩)),
add_comm]
apply AddSubmonoid.add_mem_sup
· exact Set.mem_range_self _
· apply Ideal.subset_span
apply Set.mem_union_right
exact Set.mem_range_self _
· apply AddSubmonoid.mem_sup_left
exact ⟨X i, map_X _ _⟩
· intro r
apply AddSubmonoid.mem_sup_left
exact ⟨C r, map_C _ _⟩
· intro _ _ _ _ h₁ h₂
exact add_mem h₁ h₂
· intro x₁ x₂ _ _ h₁ h₂
obtain ⟨_, ⟨p₁, rfl⟩, q₁, hq₁, rfl⟩ := AddSubmonoid.mem_sup.mp h₁
obtain ⟨_, ⟨p₂, rfl⟩, q₂, hq₂, rfl⟩ := AddSubmonoid.mem_sup.mp h₂
rw [add_mul, mul_add, add_assoc, ← map_mul]
apply AddSubmonoid.add_mem_sup
· exact Set.mem_range_self _
· refine add_mem (Ideal.mul_mem_left _ _ hq₂) (Ideal.mul_mem_right _ _ hq₁)
obtain ⟨_, ⟨p, rfl⟩, q, hq, rfl⟩ := AddSubmonoid.mem_sup.mp this
rw [map_add, aeval_map_algebraMap, ← aeval_unique, show MvPolynomial.aeval (f ∘ X) q = 0 from leI hq,
add_zero] at hx
suffices Ideal.span (s : Set RX) ≤ (Ideal.span s₀).comap (MvPolynomial.map <| algebraMap R A)
by
refine add_mem ?_ hq
rw [hs] at this
exact this hx
rw [Ideal.span_le]
intro x hx
apply Ideal.subset_span
apply Set.mem_union_left
exact Set.mem_image_of_mem _ hx
