normalizeObj_congr — Mathlib

English

If two morphisms f,g between objects X,Y in FreeMonoidalCategory agree after normalization, then their normalizations with respect to n are equal.

Русский

Если две морфизма f,g между X,Y сходятся после нормализации, то их нормализации по n совпадают.

LaTeX

$$$ \forall n, f=g \Rightarrow normalizeObj X n = normalizeObj Y n $$$

Lean4

theorem normalizeObj_congr (n : NormalMonoidalObject C) {X Y : F C} (f : X ⟶ Y) : normalizeObj X n = normalizeObj Y n :=
  by
  rcases f with ⟨f'⟩
  apply @congr_fun _ _ fun n => normalizeObj X n
  clear n f
  induction f' with
  | comp _ _ _ _ => apply Eq.trans <;> assumption
  | whiskerLeft _ _ ih => funext; apply congr_fun ih
  | whiskerRight _ _ ih => funext; apply congr_arg₂ _ rfl (congr_fun ih _)
  | @tensor W X Y Z _ _ ih₁ ih₂ =>
    funext n
    simp [congr_fun ih₁ n, congr_fun ih₂ (normalizeObj Y n)]
  | _ => funext; rfl

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