English
Second extensionality principle for total maps: equality of total maps is detected by their action on all summands.
Русский
Принцип второго экстенсивного сравнения для суммарных отображений: равенство суммарных отображений определяется их действием на все суммированные слагаемые.
LaTeX
$$$\\forall A, i_{12}, f,g : (K.total c_{12}).X i_{12} \\to A,\\; (\\forall i_1,i_2, hi,\\; ιTotal i_1 i_2 i_{12} hi \\circ f = ιTotal i_1 i_2 i_{12} hi \\circ g) \\Rightarrow f=g$$$
Lean4
@[reassoc (attr := simp)]
theorem d₂_mapMap (i₁ : I₁) (i₂ : I₂) (i₁₂ : I₁₂) :
K.d₂ c₁₂ i₁ i₂ i₁₂ ≫ GradedObject.mapMap (toGradedObjectMap φ) _ i₁₂ = (φ.f i₁).f i₂ ≫ L.d₂ c₁₂ i₁ i₂ i₁₂ :=
by
by_cases h : c₂.Rel i₂ (c₂.next i₂)
· simp [totalAux.d₂_eq' _ c₁₂ i₁ h]
· simp [d₂_eq_zero _ c₁₂ i₁ i₂ i₁₂ h]
