English
Equivalence is preserved under swapping two successive snocs, given appropriate maximality data and isomorphisms.
Русский
Эквивалентность сохраняется при обмене двух последовательных операций snoc, при наличии надлежащих максимумов и изоморфизмов.
LaTeX
$$$\\forall s\\; x_1\\; x_2\\; y_1\\; y_2,\\; \\text{... (technical Sigma conditions) ...} \\; \\Rightarrow \\; \\text{Equivalent} (\\text{snoc}(\\text{snoc } s x_1 y_1) ...) (\\text{snoc}(\\text{snoc } s x_2 y_2) ...).$$$
Lean4
theorem snoc_snoc_swap {s : CompositionSeries X} {x₁ x₂ y₁ y₂ : X} {hsat₁ : IsMaximal s.last x₁}
{hsat₂ : IsMaximal s.last x₂} {hsaty₁ : IsMaximal (snoc s x₁ hsat₁).last y₁}
{hsaty₂ : IsMaximal (snoc s x₂ hsat₂).last y₂} (hr₁ : Iso (s.last, x₁) (x₂, y₂)) (hr₂ : Iso (x₁, y₁) (s.last, x₂)) :
Equivalent (snoc (snoc s x₁ hsat₁) y₁ hsaty₁) (snoc (snoc s x₂ hsat₂) y₂ hsaty₂) :=
let e : Fin (s.length + 1 + 1) ≃ Fin (s.length + 1 + 1) := Equiv.swap (Fin.last _) (Fin.castSucc (Fin.last _))
have h1 : ∀ {i : Fin s.length}, (Fin.castSucc (Fin.castSucc i)) ≠ (Fin.castSucc (Fin.last _)) := by simp
have h2 : ∀ {i : Fin s.length}, (Fin.castSucc (Fin.castSucc i)) ≠ Fin.last _ := by simp
⟨e, by
intro i
dsimp only [e]
refine Fin.lastCases ?_ (fun i => ?_) i
· erw [Equiv.swap_apply_left, snoc_castSucc, show (snoc s x₁ hsat₁).toFun (Fin.last _) = x₁ from last_snoc _ _ _,
Fin.succ_last, show ((s.snoc x₁ hsat₁).snoc y₁ hsaty₁).toFun (Fin.last _) = y₁ from last_snoc _ _ _,
snoc_castSucc, snoc_castSucc, Fin.succ_castSucc, snoc_castSucc, Fin.succ_last,
show (s.snoc _ hsat₂).toFun (Fin.last _) = x₂ from last_snoc _ _ _]
exact hr₂
· refine Fin.lastCases ?_ (fun i => ?_) i
· erw [Equiv.swap_apply_right, snoc_castSucc, snoc_castSucc, snoc_castSucc, Fin.succ_castSucc, snoc_castSucc,
Fin.succ_last, last_snoc', last_snoc', last_snoc']
exact hr₁
· erw [Equiv.swap_apply_of_ne_of_ne h2 h1, snoc_castSucc, snoc_castSucc, snoc_castSucc, snoc_castSucc,
Fin.succ_castSucc, snoc_castSucc, Fin.succ_castSucc, snoc_castSucc, snoc_castSucc, snoc_castSucc]
exact (s.step i).iso_refl⟩