Orientation-reversing symmetries of a common curve

Definition

Esgk_SelfCurveReversingSymmetryFamily

by mysticflounder · Oct 16, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebraic-geometrygeometry

For prepared incidence data supported on a single curve, this selects the orientation-reversing members of its finite family of curve-preserving isometries.

Definition code

-- Extracted dependency interfaces and their necessary proofs.
import Definitions.Def_Esgk_PachDeZeeuwQuadraticDegree
import Definitions.Def_Esgk_RichnessLevels
import Definitions.Def_Esgk_SelfCurveCompleteSymmetryFamily
import Definitions.Def_LeanFormalizations_PachDeZeeuw_Basic
import Definitions.Def_LeanFormalizations_PachDeZeeuw_CurveInterface
import Mathlib

/-
Copyright (c) 2026 Adam McKenna. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Adam McKenna
-/


namespace Esgk

open PachDeZeeuw


noncomputable def selfCurveReversingCarrierSymmetries
    {d : ℕ} {X : PreparedBipartiteInput d}
    (hself : SelfCurvePreparedInput X) : Finset (Point2 ≃ᵢ Point2) := by
  classical
  exact (selfCurveCarrierSymmetries hself).filter fun g ↦ ¬ IsDirect g


end Esgk

View graph