sigmaIso — Mathlib

English

There is a canonical isomorphism in CompHausLike P between the finite coproduct of the fibers of a locally constant r and the base Q: finiteCoproduct(fiber r) ≅ Q.

Русский

Существует каноническое изоморфное отображение в CompHausLike P между конечным coproduct волокон локально константной функции r и базовым объектом Q: finiteCoproduct(fiber r) ≅ Q.

LaTeX

$$$\operatorname{finiteCoproduct}(\operatorname{fiber} r) \cong Q$$$

Lean4

/-- The canonical map from the coproduct induced by `f` to `S` as an isomorphism in
`CompHausLike P`. -/
noncomputable def sigmaIso [HasExplicitFiniteCoproducts.{u} P] : (finiteCoproduct (fiber r)) ≅ Q :=
  isoOfBijective (ofHom _ (sigmaIsoHom r)) ⟨sigmaIsoHom_inj r, sigmaIsoHom_surj r⟩

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