Projectivizations as projective geometries

Proves that Mathlib projectivizations satisfy the projective-geometry axioms for the dependence-based collinearity relation.

theorem rep_comp_3 {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] (X Y Z : Projectivization K V) : Projectivization.rep ∘ ![X, Y, Z] = ![X.rep, Y.rep, Z.rep]

theorem rep_comp_2 {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] (X Y : Projectivization K V) : Projectivization.rep ∘ ![X, Y] = ![X.rep, Y.rep]

theorem lin_dep_aab {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] (a b : V) : ¬LinearIndependent K ![a, a, b]

theorem lin_dep_aba {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] (a b : V) : ¬LinearIndependent K ![a, b, a]

theorem lin_dep_abb {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] (a b : V) : ¬LinearIndependent K ![a, b, b]

theorem lin_dep_imp_span {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] (a b c : V) (bc_indep : LinearIndependent K ![b, c]) (abc_dep : ¬LinearIndependent K ![a, b, c]) : a ∈ Submodule.span K {b, c}

theorem mem_span_pair_imp_dep {K : Type u_2} {V : Type u_1} [DivisionRing K] [AddCommGroup V] [Module K V] (a b c : V) (a_mem : a ∈ Submodule.span K {b, c}) : ¬LinearIndependent K ![a, b, c]

theorem l2_rep {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] (a b p q : V) (apq_dep : ¬LinearIndependent K ![a, p, q]) (bpq_dep : ¬LinearIndependent K ![b, p, q]) (pq_indep : LinearIndependent K ![p, q]) : ¬LinearIndependent K ![a, b, p]

instance finiteDimensional_span_pair {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] (x y : V) : FiniteDimensional K ↥(Submodule.span K {x, y})

theorem finrank_span_pair_le {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] (x y : V) : Module.finrank K ↥(Submodule.span K {x, y}) ≤ 2

theorem finrank_span_pair_indep {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] (x y : V) (xy_indep : LinearIndependent K ![x, y]) : Module.finrank K ↥(Submodule.span K {x, y}) = 2

theorem finrank_span_pair_dep {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] (x y : V) (xy_dep : ¬LinearIndependent K ![x, y]) : Module.finrank K ↥(Submodule.span K {x, y}) ≤ 1

theorem l3_inter_ne_bot {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] (a b c d p : V) (pab_dep : ¬LinearIndependent K ![p, a, b]) (pcd_dep : ¬LinearIndependent K ![p, c, d]) (p_ne : p ≠ 0) (ac_indep : LinearIndependent K ![a, c]) (bd_indep : LinearIndependent K ![b, d]) : Submodule.span K {a, c} ⊓ Submodule.span K {b, d} ≠ ⊥

instance instProjectiveGeometryProjectivizationNotIndependentFinSuccOfNatNatVecConsVecEmpty {K : Type u_2} {V : Type u_1} [DivisionRing K] [AddCommGroup V] [Module K V] : Basic.ProjectiveGeometry (Projectivization K V) fun (X Y Z : Projectivization K V) => ¬Projectivization.Independent ![X, Y, Z]