reindex_over — Mathlib

English

For any i: m → n, the reindex functor reindex i preserves the projection to S; i.e., reindex i S ≫ 𝔸(m; S) ↓ S = 𝔸(n; S) ↓ S.

Русский

Для любого i: m → n перестановка индексов сохраняет проекцию на S: reindex i S ≫ 𝔸(m; S) ↓ S = 𝔸(n; S) ↓ S.

LaTeX

$$$\\mathrm{reindex}\\ i\\ S \\circ (\\mathbb{A}(m; S) \\downarrow S) = (\\mathbb{A}(n; S) \\downarrow S).$$$

Lean4

@[simp, reassoc]
theorem reindex_over {n m : Type v} (i : m → n) (S : Scheme.{max u v}) : reindex i S ≫ 𝔸(m; S) ↘ S = 𝔸(n; S) ↘ S :=
  pullback.lift_fst _ _ _

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