English
If S is EssFiniteType over R, then after base changing to T, the algebra T ⊗_R S is EssFiniteType over T.
Русский
Если S имеет EssFiniteType над R, то после базовой смены базиса T образуется T ⊗_R S, который имеет EssFiniteType над T.
LaTeX
$$EssFiniteType R S ⇒ EssFiniteType T (T ⊗_R S)$$
Lean4
instance baseChange [h : EssFiniteType R S] : EssFiniteType T (T ⊗[R] S) := by
classical
rw [essFiniteType_iff] at h ⊢
obtain ⟨σ, hσ⟩ := h
use σ.image Algebra.TensorProduct.includeRight
intro s
induction s using TensorProduct.induction_on with
| zero => exact ⟨1, one_mem _, isUnit_one, by simp⟩
| tmul x y =>
obtain ⟨t, h₁, h₂, h₃⟩ := hσ y
have H (x : S) (hx : x ∈ Algebra.adjoin R (σ : Set S)) :
1 ⊗ₜ[R] x ∈
Algebra.adjoin T ((σ.image Algebra.TensorProduct.includeRight : Finset (T ⊗[R] S)) : Set (T ⊗[R] S)) :=
by
have :
Algebra.TensorProduct.includeRight x ∈
(Algebra.adjoin R (σ : Set S)).map (Algebra.TensorProduct.includeRight (A := T)) :=
Subalgebra.mem_map.mpr ⟨_, hx, rfl⟩
rw [← Algebra.adjoin_adjoin_of_tower R]
apply Algebra.subset_adjoin
simpa [← Algebra.adjoin_image] using this
refine ⟨Algebra.TensorProduct.includeRight t, H _ h₁, h₂.map _, ?_⟩
simp only [Algebra.TensorProduct.includeRight_apply, Algebra.TensorProduct.tmul_mul_tmul, mul_one]
rw [← mul_one x, ← smul_eq_mul, ← TensorProduct.smul_tmul']
apply Subalgebra.smul_mem
exact H _ h₃
| add x y hx hy =>
obtain ⟨tx, hx₁, hx₂, hx₃⟩ := hx
obtain ⟨ty, hy₁, hy₂, hy₃⟩ := hy
refine ⟨_, mul_mem hx₁ hy₁, hx₂.mul hy₂, ?_⟩
rw [add_mul, ← mul_assoc, mul_comm tx ty, ← mul_assoc]
exact add_mem (mul_mem hx₃ hy₁) (mul_mem hy₃ hx₁)
