natTrans_ext_of_isGalois — Mathlib

English

Two natural transformations t,s: F ⟶ G are equal if they agree on all IsGalois objects.

Русский

Два натуральных преобразования t,s: F ⟶ G равны, если они согласованы на всех Galois-объектах.

LaTeX

$$$\\forall X\\,[IsGalois X]\\; t.app X = s.app X \\Rightarrow t = s$$$

Lean4

/-- To check equality of natural transformations `F ⟶ G`, it suffices to check it on
Galois objects. -/
theorem natTrans_ext_of_isGalois {G : C ⥤ FintypeCat.{w}} {t s : F ⟶ G}
    (h : ∀ (X : C) [IsGalois X], t.app X = s.app X) : t = s :=
  by
  ext X x
  obtain ⟨A, f, a, _, rfl⟩ := exists_hom_from_galois_of_fiber F X x
  rw [FunctorToFintypeCat.naturality, FunctorToFintypeCat.naturality, h A]

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