snoc_snoc_swap — Mathlib

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⟩

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