adjoin_top — Mathlib

English

Let R → S be a ring homomorphism setting and t a subset of an algebra A. The subalgebra of A generated by t together with the top subalgebra of S over R equals the scalars-restriction of the S-generated algebra: adjoin(⊤) t equals (adjoin S t) restricted to ⊤.

Русский

Пусть имеется факторная структура колец R ⟶ S и подалгебра A с подмножеством t. Подалгебра, порожденная t и верхним подалгеброй S над R, равна подалгебре, порожденной t над S, с ограничением скаляров до ⊤.

LaTeX

$$$\\operatorname{adjoin}(\\top : Subalgebra\\ R\\ S)\\ t \\,=\\, (\\operatorname{adjoin}\\ S\\ t)\\\\text{.restrictScalars}(\\top : Subalgebra\\ R\\ S)$$$

Lean4

@[simp]
theorem adjoin_top {A} [Semiring A] [Algebra S A] (t : Set A) :
    adjoin (⊤ : Subalgebra R S) t = (adjoin S t).restrictScalars (⊤ : Subalgebra R S) :=
  let equivTop : Subalgebra (⊤ : Subalgebra R S) A ≃o Subalgebra S A :=
    { toFun := fun s => { s with algebraMap_mem' := fun r => s.algebraMap_mem ⟨r, trivial⟩ }
      invFun := fun s => s.restrictScalars _
      left_inv := fun _ => SetLike.coe_injective rfl
      right_inv := fun _ => SetLike.coe_injective rfl
      map_rel_iff' := @fun _ _ => Iff.rfl }
  le_antisymm (adjoin_le <| show t ⊆ adjoin S t from subset_adjoin)
    (equivTop.symm_apply_le.mpr <| adjoin_le <| show t ⊆ adjoin (⊤ : Subalgebra R S) t from subset_adjoin)

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