adjoin_adjoin_coe_preimage — Mathlib

English

For any subset s of A, the subalgebra generated by the preimage of s under the inclusion map from adjoin R s to A equals the top subalgebra.

Русский

Пусть s ⊆ A. Порождение подалгебры из предобраза s по включению из adjoin R s в A равно верхнему подалгебре.

LaTeX

$$$\\operatorname{adjoin}\\_R\\left( (\\uparrow)^{-1}(s) \\right) = \\top$$$

Lean4

@[simp]
theorem adjoin_adjoin_coe_preimage {s : Set A} : adjoin R (((↑) : adjoin R s → A) ⁻¹' s) = ⊤ :=
  by
  refine
    eq_top_iff.2 fun ⟨x, hx⟩ ↦ adjoin_induction (fun a ha ↦ ?_) (fun r ↦ ?_) (fun _ _ _ _ ↦ ?_) (fun _ _ _ _ ↦ ?_) hx
  · exact subset_adjoin ha
  · exact Subalgebra.algebraMap_mem _ r
  · exact Subalgebra.add_mem _
  · exact Subalgebra.mul_mem _

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