sec — Mathlib

English

For z, the equation z·f(sec z).2 = f(sec z).1 holds, reflecting the consistency of the section with the map f.

Русский

Для z выполняется z·f(sec z).2 = f(sec z).1, что отражает согласованность секции с отображением f.

LaTeX

$$$z \\cdot f((f.{\\mathsf{sec}}\,z).2) = f((f.{\\mathsf{sec}}\,z).1)$$$

Lean4

/-- Given a localization map `f : M →* N`, a section function sending `z : N` to some
`(x, y) : M × S` such that `f x * (f y)⁻¹ = z`. -/
@[to_additive /-- Given a localization map `f : M →+ N`, a section function sending `z : N`
    to some `(x, y) : M × S` such that `f x - f y = z`. -/
    ]
noncomputable def sec (f : LocalizationMap S N) (z : N) : M × S :=
  Classical.choose <| f.surj z

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