cardinality of projective space over finite field

Stream: Is there code for X?

[Christian Merten]

Do we have the cardinality of docs#Projectivization of a finite module over a finite field?

[Adam Topaz]

probably not

[Christian Merten]

(more precisely: I need to know that there are exactly $q + 1$ one-dimensional subspaces of $\mathbb{F}_q^2$.)

[Johan Commelin]

I hacked together a start

import Mathlib

variable (k : Type*) [Field k] [Finite k]

open scoped LinearAlgebra.Projectivization

lemma Nat.sq_sub_one (n : ℕ) : n ^ 2 - 1 = (n + 1) * (n - 1) := by
  rw [mul_comm, Nat.sub_mul, Nat.one_mul, Nat.mul_add, Nat.mul_one, Nat.sub_add_eq,
    Nat.add_sub_cancel, Nat.pow_two]

lemma Projectivization.card_eq : Nat.card (ℙ k (Fin 2 → k)) = Nat.card k + 1 := by
  classical
  have : Fintype k := .ofFinite k
  have : Fintype { v : Fin 2 → k // v ≠ 0 } := .ofFinite _
  have : Fintype (ℙ k (Fin 2 → k)) := Quotient.fintype _
  rw [Nat.card_eq_fintype_card, Nat.card_eq_fintype_card]
  have aux : ∀ x : ℙ k (Fin 2 → k),
      (Finset.univ.filter (fun v ↦ mk' k v = x)).card = Fintype.card k - 1 := by
    intro x
    rw [← Fintype.card_subtype]
    suffices { v // mk' k v = x } ≃ kˣ by
      rw [Fintype.card_congr this, Fintype.card_units]
    refine ⟨?_, ?_, ?_, ?_⟩
    · intro v
      have hv := v.2
      rw [mk'_eq_mk] at hv
      have := (mk_eq_mk_iff k v.1.1 x.rep v.1.2 x.rep_nonzero).mp
      simp only [ne_eq, mk'_eq_mk, hv, mk_rep, true_implies] at this
      exact Classical.choose this
    · intro u
      let v := u • x.rep
      refine ⟨⟨v, ?_⟩, ?_⟩
      · sorry
      · simp
        sorry
    · intro v
      have hv := v.2
      rw [mk'_eq_mk] at hv
      have := (mk_eq_mk_iff k v.1.1 x.rep v.1.2 x.rep_nonzero).mp
      simp only [ne_eq, mk'_eq_mk, hv, mk_rep, true_implies] at this
      ext : 2
      exact Classical.choose_spec this
    · intro u
      sorry
  have := Finset.card_eq_sum_card_fiberwise
    (β := ℙ k (Fin 2 → k)) (f := mk' _) (s := .univ) (t := .univ) (fun _ _ ↦ Finset.mem_univ _)
  simp_rw [Finset.card_univ, aux] at this
  simp only [Fintype.card_subtype_compl, Fintype.card_pi, Finset.prod_const, Finset.card_univ,
    Fintype.card_fin, Fintype.card_ofSubsingleton, Finset.sum_const, smul_eq_mul] at this
  rw [Nat.sq_sub_one] at this
  refine Nat.mul_right_cancel ?_ this.symm
  have : 1 < Fintype.card k := Fintype.one_lt_card
  omega

[Notification Bot]

Junyan Xu has marked this topic as resolved.

[Notification Bot]

Junyan Xu has marked this topic as unresolved.

[Adam Topaz]

I think a nice way to break this up would be to construct a bijection between (P k V) x k^x and the nonzero elements of V.

[Christian Merten]

Thanks! I came up with this:

import Mathlib.LinearAlgebra.Projectivization.Basic

section

variable (α β : Type*) [Group α] [MulAction α β] (b : β)

variable {α} in
def QuotientGroup.congr' {s t : Subgroup α} (h : s = t) :
    α ⧸ s ≃ α ⧸ t :=
  Quotient.congr (Equiv.refl _) (fun a b ↦ by rw [h]; rfl)

variable {α} in
def QuotientGroup.bot {s : Subgroup α} (h : s = ⊥) :
    α ⧸ s ≃ α :=
  (QuotientGroup.congr' h).trans (QuotientGroup.quotientBot).toEquiv

noncomputable
def MulAction.selfEquivOrbitsQuotientProd'
    {φ : Quotient (MulAction.orbitRel α β) → β} (hφ : Function.LeftInverse Quotient.mk'' φ)
    (h : ∀ b : β, stabilizer α b = ⊥) :
    β ≃ Quotient (MulAction.orbitRel α β) × α :=
  let e := MulAction.selfEquivSigmaOrbitsQuotientStabilizer' α β hφ
  e.trans <|
    (Equiv.sigmaCongrRight <| fun _ ↦ QuotientGroup.bot (h _)).trans <| Equiv.sigmaEquivProd _ _

noncomputable
def MulAction.selfEquivOrbitsQuotientProd
    (h : ∀ b : β, stabilizer α b = ⊥) :
    β ≃ Quotient (MulAction.orbitRel α β) × α :=
  MulAction.selfEquivOrbitsQuotientProd' α β Quotient.out_eq' h

end

variable (k V : Type*) [Field k] [AddCommGroup V] [Module k V]

open LinearAlgebra.Projectivization

instance : SMul kˣ { v : V // v ≠ 0 } where
  smul a v := ⟨a • v, by
    simp only [ne_eq, Set.mem_setOf_eq, Units.smul_def, smul_eq_zero, a.ne_zero, false_or]
    exact v.property⟩

@[simp]
lemma smul_coe (a : kˣ) (v : { v : V // v ≠ 0 }) :
    (a • v).val = a • v.val :=
  rfl

instance : MulAction kˣ { v : V // v ≠ 0 } where
  one_smul v := by ext; simp
  mul_smul a b x := by ext; simp [mul_smul]

lemma orbitRel_iff (x y : { v : V // v ≠ 0 }) :
    (MulAction.orbitRel kˣ { v // v ≠ 0 }).Rel x y ↔
      (MulAction.orbitRel kˣ V).Rel x.val y.val :=
  ⟨by rintro ⟨a, rfl⟩; exact ⟨a, by simp⟩, by intro ⟨a, ha⟩; exact ⟨a, by ext; simpa⟩⟩

lemma orbitRel_comap_eq_orbitRel :
    (MulAction.orbitRel kˣ V).comap (↑) = MulAction.orbitRel kˣ { v : V // v ≠ 0 } := by
  ext x y
  rw [Setoid.comap_rel, orbitRel_iff]

def equivQuotientOrbitRel : ℙ k V ≃ Quotient (MulAction.orbitRel kˣ { v : V // v ≠ 0 }) :=
  Quotient.congr (Equiv.refl _) (fun x y ↦ (orbitRel_iff k V x y).symm)

lemma stabilizer_eq_bot (x : { v : V // v ≠ 0 }) : MulAction.stabilizer kˣ x = ⊥ := by
  rw [eq_bot_iff]
  intro g (hg : g • x = x)
  ext
  rw [Subtype.ext_iff] at hg
  simp only [ne_eq, smul_coe, Units.smul_def] at hg
  rw [← sub_eq_zero, ← smul_eq_zero_iff_left x.property]
  simp [sub_smul, hg]

noncomputable
def nonZeroEquivProjectivizationProdUnits : { v : V // v ≠ 0 } ≃ ℙ k V × kˣ :=
  let e := MulAction.selfEquivOrbitsQuotientProd _ _ (stabilizer_eq_bot k V)
  e.trans (Equiv.prodCongrLeft (fun _ ↦ (equivQuotientOrbitRel k V).symm))

instance [Finite k] [Finite V] : Finite (ℙ k V) :=
  have : Finite (ℙ k V × kˣ) := Finite.of_equiv _ (nonZeroEquivProjectivizationProdUnits k V)
  Finite.prod_left kˣ

lemma card [Finite k] [Finite V] :
    Nat.card V - 1 = Nat.card (ℙ k V) * (Nat.card k - 1) := by
  classical
  haveI : Fintype V := Fintype.ofFinite V
  haveI : Fintype (ℙ k V) := Fintype.ofFinite (ℙ k V)
  haveI : Fintype k := Fintype.ofFinite k
  have hV : Fintype.card { v : V // v ≠ 0 } = Fintype.card V - 1 := by simp
  simp_rw [← Fintype.card_eq_nat_card, ← Fintype.card_units (α := k), ← hV]
  rw [Fintype.card_congr (nonZeroEquivProjectivizationProdUnits k V), Fintype.card_prod]

[Christian Merten]

I am wondering if docs#Projectivization should be defined as Quotient (MulAction.orbitRel kˣ { v : V // v ≠ 0 }).

[Antoine Chambert-Loir]

This is more or less how it is defined once everything is unfolded, isn't it?

[Christian Merten]

Yes, up to

lemma orbitRel_iff (x y : { v : V // v ≠ 0 }) :
    (MulAction.orbitRel kˣ { v // v ≠ 0 }).Rel x y ↔
      (MulAction.orbitRel kˣ V).Rel x.val y.val :=
  ⟨by rintro ⟨a, rfl⟩; exact ⟨a, by simp⟩, by intro ⟨a, ha⟩; exact ⟨a, by ext; simpa⟩⟩

[Antoine Chambert-Loir]

I'm not a specialist of this part, but that looks like mathlib needs a general purpose lemma of the kind you're needing.

[Christian Merten]

This general purpose lemma is probably docs#SubMulAction.orbitRel_of_subMul