reindex_comp — Mathlib

English

Reindexing is functorial: reindex (j ∘ i) S = reindex j S ≫ reindex i S for i: n₁ → n₂, j: n₂ → n₃.

Русский

Переиндексация — это функторная: reindex (j ∘ i) S = reindex j S ≫ reindex i S.

LaTeX

$$$\\mathrm{reindex}(j \\circ i) S = \\mathrm{reindex}(j) S \\\\circ \\mathrm{reindex}(i) S.$$$

Lean4

@[simp, reassoc]
theorem reindex_comp {n₁ n₂ n₃ : Type v} (i : n₁ → n₂) (j : n₂ → n₃) (S : Scheme.{max u v}) :
    reindex (j ∘ i) S = reindex j S ≫ reindex i S :=
  by
  have H₁ : reindex (j ∘ i) S ≫ 𝔸(n₁; S) ↘ S = (reindex j S ≫ reindex i S) ≫ 𝔸(n₁; S) ↘ S := by simp
  have H₂ (k) : (reindex (j ∘ i) S).appTop (coord S k) = (reindex j S).appTop ((reindex i S).appTop (coord S k)) :=
    by
    rw [reindex_appTop_coord, reindex_appTop_coord, reindex_appTop_coord]
    rfl
  exact hom_ext H₁ H₂

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