of_comp — Mathlib

English

If f is an injective AlgHom and H asserts IsTranscendenceBasis R (f ∘ x), then IsTranscendenceBasis R x.

Русский

Если f — инъективный гомоморфизм Алгебра, и H имеет IsTranscendenceBasis R (f ∘ x), тогда IsTranscendenceBasis R x.

LaTeX

$$$(\\text{H}) \\Rightarrow \\text{IsTB}_R x$$$

Lean4

theorem of_comp {x : ι → A} (f : A →ₐ[R] A') (h : Function.Injective f) (H : IsTranscendenceBasis R (f ∘ x)) :
    IsTranscendenceBasis R x :=
  by
  refine ⟨(AlgHom.algebraicIndependent_iff f h).mp H.1, ?_⟩
  intro s hs hs'
  have :=
    H.2 (f '' s) ((algebraicIndependent_image h.injOn).mp ((AlgHom.algebraicIndependent_iff f h).mpr hs))
      (by rw [Set.range_comp]; exact Set.image_mono hs')
  rwa [Set.range_comp, (Set.image_injective.mpr h).eq_iff] at this

Похожие утверждения