English
There is a natural isomorphism between dual versions of antisymmetrization and antisymmetrization of duals, respecting order structure and embeddings.
Русский
Существует естественная изоморфия между дуальными версиями антисимметризации и антисимметризацией двойственного, сохраняющая порядок и вложения.
LaTeX
$$$\\text{dualAntisymmetrization} : (\\text{Antisymmetrization}(α))^{\\mathrm{op}} \\simeq_o \\text{Antisymmetrization}(α^{\\mathrm{op}})$$$
Lean4
/-- The antisymmetrization of a product preorder is order isomorphic
to the product of antisymmetrizations. -/
def prodEquiv : Antisymmetrization (α × β) (· ≤ ·) ≃o Antisymmetrization α (· ≤ ·) × Antisymmetrization β (· ≤ ·)
where
toFun :=
Quotient.lift (fun ab ↦ (⟦ab.1⟧, ⟦ab.2⟧)) fun ab₁ ab₂ h ↦
Prod.ext (Quotient.sound ⟨h.1.1, h.2.1⟩) (Quotient.sound ⟨h.1.2, h.2.2⟩)
invFun :=
Function.uncurry <|
Quotient.lift₂ (fun a b ↦ ⟦(a, b)⟧) fun a₁ b₁ a₂ b₂ h₁ h₂ ↦ Quotient.sound ⟨⟨h₁.1, h₂.1⟩, h₁.2, h₂.2⟩
left_inv := by rintro ⟨_⟩; rfl
right_inv := by rintro ⟨⟨_⟩, ⟨_⟩⟩; rfl
map_rel_iff' := by rintro ⟨_⟩ ⟨_⟩; rfl
