English
Right inclusion commutes with tensoring: tensoring followed by inr equals inr composed with the corresponding morphisms.
Русский
Правое включение совместно с тензоризацией: тензорирование за которым следует inr эквивалентно композиции inr с соответствующими гомоморфизмами.
LaTeX
$$$\\forall x_1,y_1,x_2,y_2,\\; f_1:x_1\\to y_1,\\; f_2:x_2\\to y_2:\\; inr\\; x_1\\; x_2 \\; \\otimes_m\\; (f_1\\otimes_m f_2) = f_2\\; \\otimes_m\\; inr\\; y_1\\; y_2.$$$
Lean4
@[reassoc (attr := simp)]
theorem inr_comp_tensorHom {x₁ y₁ x₂ y₂ : AugmentedSimplexCategory} (f₁ : x₁ ⟶ y₁) (f₂ : x₂ ⟶ y₂) :
inr x₁ x₂ ≫ (f₁ ⊗ₘ f₂) = f₂ ≫ inr y₁ y₂ :=
match x₁, y₁, x₂, y₂, f₁, f₂ with
| .of x₁, .of y₁, .of x₂, .of y₂, f₁, f₂ =>
by
change inr' _ _ ≫ tensorHomOf _ _ = WithInitial.down f₂ ≫ inr' _ _
ext i : 3
dsimp [tensorHomOf]
have e₁ := inr'_eval x₁ x₂ i
have e₂ := inr'_eval y₁ y₂ <| (WithInitial.down f₂).toOrderHom i
simp only [SimplexCategory.len_mk] at e₁ e₂
rw [e₁, e₂]
simp only [SimplexCategory.eqToHom_toOrderHom, SimplexCategory.len_mk, Nat.succ_eq_add_one,
OrderEmbedding.toOrderHom_coe, OrderIso.coe_toOrderEmbedding, Fin.castOrderIso_apply, Fin.cast_cast,
Fin.cast_eq_self, Fin.cast_inj]
conv_lhs =>
change
Fin.addCases (fun i ↦ Fin.castAdd (y₂.len + 1) (f₁.toOrderHom i))
(fun i ↦ Fin.natAdd (y₁.len + 1) (f₂.toOrderHom i)) (Fin.natAdd (x₁.len + 1) i)
rw [Fin.addCases_right]
rfl
| .star, _, _, _, f₁, f₂ => by cat_disch
| _, _, .star, _, _, _ => rfl
