Subspaces and subgeometries

Defines subspaces of an axiomatic projective geometry and the induced projective subgeometry structure on a closed subset.

class Structure.ProjectiveSubgeometry {G : Type u_1} {ell : G → G → G → Prop} (G' : Set G) : Type u_1

A projective subgeometry: a subset G' carrying a collinearity relation ell' that is the restriction of ell and is itself a projective geometry.

• ell' : ↑G' → ↑G' → ↑G' → Prop

  The collinearity relation on the subset G'.

• restriction (a b c : ↑G') : ell' ell a b c = ell ↑a ↑b ↑c
• inst : Basic.ProjectiveGeometry (↑G') (ell' ell)

theorem Structure.subspace_l1 {G : Type u_1} {ell : G → G → G → Prop} [PG : Basic.ProjectiveGeometry G ell] (E : Set G) (ell' : ↑E → ↑E → ↑E → Prop) (restriction : ∀ (a b c : ↑E), ell' a b c = ell ↑a ↑b ↑c) (a b : ↑E) : ell' a b a

theorem Structure.subspace_l2 {G : Type u_1} {ell : G → G → G → Prop} [PG : Basic.ProjectiveGeometry G ell] (E : Set G) (ell' : ↑E → ↑E → ↑E → Prop) (restriction : ∀ (a b c : ↑E), ell' a b c = ell ↑a ↑b ↑c) (a b p q : ↑E) (apq_col : ell' a p q) (bpq_col : ell' b p q) (pq_neq : p ≠ q) : ell' a b p

class Structure.Subspace {G : Type u_1} {ell : G → G → G → Prop} [DecidableEq G] (E : Set G) : Prop

A subspace of a projective geometry: a subset E closed under the line operator, i.e. containing the whole line a ⋆ b whenever a, b ∈ E.

• closure (a b : G) : a ∈ E → b ∈ E → Basic.star ell a b ⊆ E

@[implicit_reducible]

instance Structure.instProjectiveSubgeometry {G : Type u_1} {ell : G → G → G → Prop} [PG : Basic.ProjectiveGeometry G ell] [DecidableEq G] {E : Set G} [S : Subspace E] : ProjectiveSubgeometry E

Equations

• Structure.instProjectiveSubgeometry = { ell' := fun (a b c : ↑E) => E.restrict (E.restrict (E.restrict ell a) b) c, restriction := ⋯, inst := ⋯ }

instance Structure.instSubspaceStar {G : Type u_1} {ell : G → G → G → Prop} [PG : Basic.ProjectiveGeometry G ell] [DecidableEq G] (a b : G) : Subspace (Basic.star ell a b)

def Structure.galaxy {G : Type u_1} {ell : G → G → G → Prop} [DecidableEq G] (b c a : G) : Set G

The galaxy generated by a and the line b ⋆ c: the union of all lines a ⋆ x with x ranging over b ⋆ c (the plane through a and that line).

Equations

• Structure.galaxy b c a = ⋃₀ {x : Set G | ∃ x_1 ∈ Basic.star ell b c, Basic.star ell a x_1 = x}

instance Structure.instSubspaceGalaxy {G : Type u_1} {ell : G → G → G → Prop} [PG : Basic.ProjectiveGeometry G ell] [DecidableEq G] (b c x₁ : G) : Subspace (galaxy b c x₁)