English
Extending ordered finpartitions of Fin n bijects with ordered finpartitions of Fin (n+1).
Русский
Расширение упорядоченных финразби́вок Fin n устанавливает биекцию с упорядоченными финразби́вками Fin (n+1).
LaTeX
$$extendEquiv(n) : ((c : OrderedFinpartition n) × Option (Fin c.length)) ≃ OrderedFinpartition (n+1)$$
Lean4
/-- Extending the ordered partitions of `Fin n` bijects with the ordered partitions
of `Fin (n+1)`. -/
@[simps apply]
def extendEquiv (n : ℕ) : ((c : OrderedFinpartition n) × Option (Fin c.length)) ≃ OrderedFinpartition (n + 1)
where
toFun c := c.1.extend c.2
invFun c := if h : range (c.emb 0) = {0} then ⟨c.eraseLeft h, none⟩ else ⟨c.eraseMiddle h, some (c.index 0)⟩
left_inv := by
rintro ⟨c, o⟩
match o with
| none =>
simp only [extend, range_extendLeft_zero, ↓reduceDIte, Sigma.mk.inj_iff, heq_eq_eq, and_true]
rfl
|
some
i =>
simp only [extend, range_emb_extendMiddle_ne_singleton_zero, ↓reduceDIte, Sigma.mk.inj_iff, heq_eq_eq, and_true,
eraseMiddle, index_extendMiddle_zero]
ext
· rfl
· simp only [heq_eq_eq, index_extendMiddle_zero]
ext j
rcases eq_or_ne i j with rfl | hij
· simp [extendMiddle]
· simp [hij.symm, extendMiddle]
· refine HEq.symm (hfunext rfl ?_)
simp only [heq_eq_eq, forall_eq']
intro a
rcases eq_or_ne a i with rfl | hij
· refine (Fin.heq_fun_iff ?_).mpr ?_
· rw [index_extendMiddle_zero]
simp [extendMiddle]
· simp [extendMiddle]
· refine (Fin.heq_fun_iff ?_).mpr ?_
· rw [index_extendMiddle_zero]
simp [extendMiddle]
· simp [extendMiddle, hij]
right_inv
c := by
by_cases h : range (c.emb 0) = {0}
· have A : c.length - 1 + 1 = c.length := Nat.sub_add_cancel (c.length_pos (Nat.zero_lt_succ n))
dsimp only
rw [dif_pos h]
simp only [extend, extendLeft, eraseLeft]
ext
· exact A
· refine (Fin.heq_fun_iff A).mpr (fun i ↦ ?_)
induction i using Fin.induction with
| zero => change 1 = c.partSize 0; simp [c.partSize_eq_one_of_range_emb_eq_singleton h]
| succ i => simp only [cons_succ, val_succ]; rfl
· refine hfunext (congrArg Fin A) ?_
simp only
intro i i' h'
have : i' = Fin.cast A i := eq_of_val_eq (by apply val_eq_val_of_heq h'.symm)
subst this
refine (Fin.heq_fun_iff ?_).mpr ?_
·
induction i using Fin.induction with
| zero => simp [c.partSize_eq_one_of_range_emb_eq_singleton h]
| succ i => simp
· intro j
induction i using Fin.induction with
| zero =>
simp only [cases_zero, cast_zero, val_eq_zero]
exact (apply_eq_of_range_eq_singleton h _).symm
| succ i => simp
· dsimp only
rw [dif_neg h]
have B : c.partSize (c.index 0) - 1 + 1 = c.partSize (c.index 0) :=
Nat.sub_add_cancel (c.partSize_pos (c.index 0))
simp only [extend, extendMiddle, eraseMiddle, ↓reduceDIte]
ext
· rfl
· simp only [update_self, update_idem, heq_eq_eq, update_eq_self_iff, B]
· refine hfunext rfl ?_
simp only [heq_eq_eq, forall_eq']
intro i
refine ((Fin.heq_fun_iff ?_).mpr ?_).symm
· simp only [update_self, B, update_idem, update_eq_self]
· intro j
rcases eq_or_ne i (c.index 0) with rfl | hi
· simp only [↓reduceDIte, comp_apply]
rcases eq_or_ne j 0 with rfl | hj
· simpa using c.emb_zero
· let j' := Fin.pred (j.cast B.symm) (by simpa using hj)
have : j = (succ j').cast B := by simp [j']
simp only [this, coe_cast, val_succ, cast_mk, cases_succ', comp_apply, succ_mk, succ_pred]
rfl
· simp [hi]
