gi — Mathlib · SciLib

English

There exists a Galois insertion between adjoin and the coe map, providing a canonical lift of an intermediate field to a set and back.

Русский

Существует Galois вставка между адъюнкцией и отображением коe, задающая каноническое отображение промежуточного поля в множество и обратно.

LaTeX

$$gi : GaloisInsertion (adjoin F) (\ x => x)$$

Lean4

/-- Galois insertion between `adjoin` and `coe`. -/
def gi : GaloisInsertion (adjoin F : Set E → IntermediateField F E) (fun (x : IntermediateField F E) => (x : Set E))
    where
  choice s hs := (adjoin F s).copy s <| le_antisymm (gc.le_u_l s) hs
  gc := IntermediateField.gc
  le_l_u S := (IntermediateField.gc (S : Set E) (adjoin F S)).1 <| le_rfl
  choice_eq _ _ := copy_eq _ _ _

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