gc — Mathlib · SciLib

English

There is a Galois connection between adjoin and the inclusion of subalgebras: s ⊆ S if and only if adjoin s ≤ S.

Русский

Существует Галуа-сопряжение между образованием adjoin и включением подпалгебр: s ⊆ S тогда и только тогда adjoin s ≤ S.

LaTeX

$$$s \subseteq S \iff \operatorname{adjoin}_R(s) \le S$$$

Lean4

protected theorem gc : GaloisConnection (adjoin R : Set A → NonUnitalSubalgebra R A) (↑) := fun s S =>
  ⟨fun H => (NonUnitalSubsemiring.subset_closure.trans Submodule.subset_span).trans H, fun H =>
    show Submodule.span R _ ≤ S.toSubmodule from
      Submodule.span_le.mpr <|
        show NonUnitalSubsemiring.closure s ≤ S.toNonUnitalSubsemiring from NonUnitalSubsemiring.closure_le.2 H⟩

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