substructureReduct — Mathlib

English

Reduces the language of a substructure along a language hom; produces an embedding of L'.Substructure M into L.Substructure M.

Русский

Уменьшение языка подструктуры вдоль гомоморфизма языка; получается вложение L'.Substructure M в L.Substructure M.

LaTeX

$$$\mathrm{substructureReduct}(\phi) : L'.Substructure M \hookrightarrow L.Substructure M$$$

Lean4

/-- Reduces the language of a substructure along a language hom. -/
def substructureReduct (φ : L →ᴸ L') [φ.IsExpansionOn M] : L'.Substructure M ↪o L.Substructure M
    where
  toFun
    S :=
    { carrier := S
      fun_mem := fun {n} f x hx => by
        have h := S.fun_mem (φ.onFunction f) x hx
        simp only [LHom.map_onFunction, Substructure.mem_carrier] at h
        exact h }
  inj' S T
    h := by
    simp only [SetLike.coe_set_eq, Substructure.mk.injEq] at h
    exact h
  map_rel_iff' {_ _} := Iff.rfl

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