English
If a ≠ b are order embeddings, then pairingDual applied to ιMulti(f∘a) and ιMulti(x∘b) equals 0.
Русский
Если a ≠ b — взаимно включающие отображения, то pairingDual(ιMulti(f∘a), ιMulti(x∘b)) = 0.
LaTeX
$$$ pairingDual\ R\ M\ n (ιMulti\ _\ _ (f \circ a)) (ιMulti\ _\ _ (x \circ b)) = 0 $$$
Lean4
theorem pairingDual_apply_apply_eq_one_zero (a b : Fin n ↪o ι) (h : a ≠ b) :
pairingDual R M n (ιMulti _ _ (f ∘ a)) (ιMulti _ _ (x ∘ b)) = 0 :=
by
simp only [pairingDual_ιMulti_ιMulti, Function.comp_apply, Matrix.det_apply]
refine Finset.sum_eq_zero (fun σ _ ↦ ?_)
simp only [Matrix.of_apply, smul_eq_iff_eq_inv_smul, smul_zero]
by_contra h'
apply h
have : a = b ∘ σ := by
ext i
by_contra hi
exact h' (Finset.prod_eq_zero (i := i) (by simp) (h₀ hi))
have hσ : Monotone σ := fun i j hij ↦ by
have h'' := congr_fun this
dsimp at h''
rw [← a.map_rel_iff] at hij
simpa only [← b.map_rel_iff, ← h'']
have hσ' : Monotone σ.symm := fun i j hij ↦
by
obtain ⟨i, rfl⟩ := σ.surjective i
obtain ⟨j, rfl⟩ := σ.surjective j
simp only [Equiv.symm_apply_apply]
by_contra! h
obtain rfl : i = j := σ.injective (le_antisymm hij (hσ h.le))
simp only [lt_self_iff_false] at h
obtain rfl : σ = 1 := by
ext i : 1
exact DFunLike.congr_fun (Subsingleton.elim (σ.toOrderIso hσ hσ') (OrderIso.refl _)) i
ext
apply congr_fun this
