map_reindex — Mathlib

English

For morphisms f: S → T and indices, the map intertwines with reindex: map n₂ f ≫ reindex i T = reindex i S ≫ map n₁ f.

Русский

Для морфизмов f: S → T и индексов отображение взаимодействует с переиндексацией: map n₂ f ≫ reindex i T = reindex i S ≫ map n₁ f.

LaTeX

$$$\\mathrm{map}\\ n_2\\ f \\;\\gg \\; \\mathrm{reindex} i\\ T = \\mathrm{reindex} i\\ S \\;\\gg \\; \\mathrm{map}\\ n_1\\ f.$$$

Lean4

@[reassoc (attr := simp)]
theorem map_reindex {n₁ n₂ : Type v} (i : n₁ → n₂) {S T : Scheme.{max u v}} (f : S ⟶ T) :
    map n₂ f ≫ reindex i T = reindex i S ≫ map n₁ f := by apply hom_ext <;> simp

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