fst_map — Mathlib

English

The composition of fstHom with map equals the fstHom after map, i.e., the left projection is compatible with the functorial lift.

Русский

Составление fstHom с map эквивалентно fstHom после map; левая проекция совместима с лифтом.

LaTeX

$$$\\text{fstHom}_{R',R'N} \\circ (\\mathrm{map}\\ f) = \\text{fstHom}_{R',R'M}$$$

Lean4

@[simp]
theorem fst_map (f : M →ₗ[R'] N) (x : TrivSqZeroExt R' M) : fst (map f x) = fst x := by
  simp [map, lift_def, Algebra.ofId_apply, algebraMap_eq_inl]

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