Morphisms of projective geometries

Defines isomorphisms of projective geometries as bijections preserving the collinearity relation.

class PG_Iso {G₁ : Type u_1} {G₂ : Type u_2} {ell₁ : G₁ → G₁ → G₁ → Prop} {ell₂ : G₂ → G₂ → G₂ → Prop} [Basic.ProjectiveGeometry G₁ ell₁] [Basic.ProjectiveGeometry G₂ ell₂] (f : G₁ → G₂) : Prop

An isomorphism of projective geometries is a bijective map f : G₁ → G₂ satisfying ell₁ a b c ↔ ell₂ (f a) (f b) (f c). When G₁ = G₂ one says that f is a collineation. (p. 27)

• bij : Function.Bijective f
• pres_col (a b c : G₁) : ell₁ a b c ↔ ell₂ (f a) (f b) (f c)