fixingSubmonoid_fixedPoints_gc — Mathlib

English

There is a Galois connection between fixing submonoids and fixed points of a monoid action: larger submonoids correspond to smaller fixed point sets, and vice versa.

Русский

Существует связь Галуа между фиксирующим подмоноидом и множеством фиксированных точек действия: большее подмоноид соответствует меньшему множеству фиксированных точек и наоборот.

LaTeX

$$$\\text{GaloisConnection}(\\text{fixingSubmonoid},\\text{fixedPoints})$$$

Lean4

/-- The Galois connection between fixing submonoids and fixed points of a monoid action -/
@[to_additive]
theorem fixingSubmonoid_fixedPoints_gc :
    GaloisConnection (OrderDual.toDual ∘ fixingSubmonoid M)
      ((fun P : Submonoid M => fixedPoints P α) ∘ OrderDual.ofDual) :=
  fun _s _P => ⟨fun h s hs p => h p.2 ⟨s, hs⟩, fun h p hp s => h s.2 ⟨p, hp⟩⟩

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