instProjectivePlaneProjectivizationForallFinOfNatNatOfDecidableEq

English

Derangements on a field-constructed projective plane are invariant under field-equivalent projectivizations; there is an explicit equivalence between these derangements induced by the dual and the Field structure.

Русский

Деранджменты на плоскости, построенной через поле, инвариантны относительно эквивалентности полей; существует явное соответствие, индуцируемое двойственностью и структурой поля.

LaTeX

$$$\text{derangements}(P,L) \cong \text{derangements}(P,L)^{{\text{dual}}}$ (via Dual and Field isomorphisms)$$

Lean4

noncomputable instance [DecidableEq K] : ProjectivePlane (ℙ K (Fin 3 → K)) (ℙ K (Fin 3 → K)) :=
  { mkPoint := by
      intro v w _
      exact cross v w
    mkPoint_ax := fun h ↦ ⟨cross_orthogonal_left h, cross_orthogonal_right h⟩
    mkLine := by
      intro v w _
      exact cross v w
    mkLine_ax := fun h ↦ ⟨orthogonal_cross_left h, orthogonal_cross_right h⟩
    exists_config := by
      refine
          ⟨mk K ![0, 1, 1] ?_, mk K ![1, 0, 0] ?_, mk K ![1, 0, 1] ?_, mk K ![1, 0, 0] ?_, mk K ![0, 1, 0] ?_,
            mk K ![0, 0, 1] ?_, ?_⟩ <;>
        simp [mem_iff, orthogonal_mk] }

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