Theorems · Definition · logic and foundations

FirstOrder.Language.Substructure.giMapComap

{L : FirstOrder.Language} →
  {M : Type w} →
    {N : Type u_1} →
      [inst : L.Structure M] →
        [inst_1 : L.Structure N] →
          {f : L.Hom M N} →
            Function.Surjective ⇑f →
              GaloisInsertion (FirstOrder.Language.Substructure.map f) (FirstOrder.Language.Substructure.comap f)

map f and comap f form a GaloisInsertion when f is surjective.

Defined in

Mathlib.ModelTheory.Substructures

Cited by

9 results in Mathlib

Foundations

Depth 26 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FirstOrder.Language.StructureFirstOrder.Language.Structure