English
If R→S and S→T have EssFiniteType, then R→T has EssFiniteType.
Русский
Если R→S и S→T имеют EssFiniteType, то R→T имеет EssFiniteType.
LaTeX
$$EssFiniteType R S ∧ EssFiniteType S T ⇒ EssFiniteType R T$$
Lean4
theorem comp [h₁ : EssFiniteType R S] [h₂ : EssFiniteType S T] : EssFiniteType R T :=
by
rw [essFiniteType_iff] at h₁ h₂ ⊢
classical
obtain ⟨s, hs⟩ := h₁
obtain ⟨t, ht⟩ := h₂
use s.image (IsScalarTower.toAlgHom R S T) ∪ t
simp only [Finset.coe_union, Finset.coe_image, Algebra.adjoin_union, Algebra.adjoin_image]
intro x
obtain ⟨y, hy₁, hy₂, hy₃⟩ := ht x
obtain ⟨t₁, h₁, h₂, h₃⟩ := EssFiniteType.aux _ _ _ _ hs _ y hy₁
obtain ⟨t₂, h₄, h₅, h₆⟩ := EssFiniteType.aux _ _ _ _ hs _ _ hy₃
refine ⟨t₂ • t₁ • y, ?_, ?_, ?_⟩
· rw [Algebra.smul_def]
exact mul_mem (Algebra.mem_sup_left ⟨_, h₄, rfl⟩) h₃
· rw [Algebra.smul_def, Algebra.smul_def]
exact (h₅.map _).mul ((h₂.map _).mul hy₂)
· rw [← mul_smul, mul_comm, smul_mul_assoc, mul_comm, mul_comm y, mul_smul, Algebra.smul_def]
exact mul_mem (Algebra.mem_sup_left ⟨_, h₁, rfl⟩) h₆
