instFiberFunctorGetFiberFunctor — Mathlib

English

The arbitrarily chosen fiber functor associated to GaloisCategory is a fiber functor.

Русский

Выбранный произвольным образом фибровый функтор, связанный с GaloisCategory, является фибровым функтором.

LaTeX

$$$\text{FiberFunctor}(\text{GaloisCategory.getFiberFunctor } C)$$$

Lean4

/-- The arbitrarily chosen fiber functor `GaloisCategory.getFiberFunctor` is a fiber functor. -/
noncomputable instance : FiberFunctor (GaloisCategory.getFiberFunctor C) :=
  Classical.choice <| Classical.choose_spec (@GaloisCategory.hasFiberFunctor C _ _)

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