Cardinality of projective spaces

We compute the cardinality of ℙ k V if k is a finite field.

def Projectivization.equivQuotientOrbitRel (k : Type u_1) (V : Type u_2) [DivisionRing k] [AddCommGroup V] [Module k V] : Projectivization k V ≃ Quotient (MulAction.orbitRel kˣ { v : V // v ≠ 0 })

ℙ k V is equivalent to the quotient of the non-zero elements of V by kˣ.

noncomputable def Projectivization.nonZeroEquivProjectivizationProdUnits (k : Type u_1) (V : Type u_2) [DivisionRing k] [AddCommGroup V] [Module k V] : { v : V // v ≠ 0 } ≃ Projectivization k V × kˣ

The non-zero elements of V are equivalent to the product of ℙ k V with the units of k.

instance Projectivization.isEmpty_of_subsingleton (k : Type u_1) (V : Type u_2) [DivisionRing k] [AddCommGroup V] [Module k V] [Subsingleton V] : IsEmpty (Projectivization k V)

instance Projectivization.finite_of_finite (k : Type u_1) (V : Type u_2) [DivisionRing k] [AddCommGroup V] [Module k V] [Finite V] : Finite (Projectivization k V)

If V is a finite k-module and k is finite, ℙ k V is finite.

theorem Projectivization.finite_iff_of_finite (k : Type u_1) (V : Type u_2) [DivisionRing k] [AddCommGroup V] [Module k V] [Finite k] : Finite (Projectivization k V) ↔ Finite V

theorem Projectivization.card (k : Type u_1) (V : Type u_2) [DivisionRing k] [AddCommGroup V] [Module k V] : Nat.card V - 1 = Nat.card (Projectivization k V) * (Nat.card k - 1)

Fraction free cardinality formula for the points of ℙ k V if k and V are finite (for silly reasons the formula also holds when k and V are infinite). See Projectivization.card' and Projectivization.card'' for other spellings of the formula.

theorem Projectivization.card' (k : Type u_1) (V : Type u_2) [DivisionRing k] [AddCommGroup V] [Module k V] [Finite V] : Nat.card V = Nat.card (Projectivization k V) * (Nat.card k - 1) + 1

Cardinality formula for the points of ℙ k V if k and V are finite with less natural subtraction.

theorem Projectivization.card'' (k : Type u_1) (V : Type u_2) [Field k] [AddCommGroup V] [Module k V] [Finite k] : Nat.card (Projectivization k V) = (Nat.card V - 1) / (Nat.card k - 1)

Cardinality formula for the points of ℙ k V if k and V are finite expressed as a fraction.

theorem Projectivization.card_of_finrank (k : Type u_1) (V : Type u_2) [Field k] [AddCommGroup V] [Module k V] [Finite k] {n : ℕ} (h : Module.finrank k V = n) : Nat.card (Projectivization k V) = ∑ i ∈ Finset.range n, Nat.card k ^ i

theorem Projectivization.card_of_finrank_two (k : Type u_1) (V : Type u_2) [Field k] [AddCommGroup V] [Module k V] [Finite k] (h : Module.finrank k V = 2) : Nat.card (Projectivization k V) = Nat.card k + 1