Users' Mathboxes Mathbox for Steven Nguyen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-prjcrv Structured version   Visualization version   GIF version

Definition df-prjcrv 40954
Description: Define the projective curve function. This takes a homogeneous polynomial and outputs the homogeneous coordinates where the polynomial evaluates to zero (the "zero set"). (In other words, scalar multiples are collapsed into the same projective point. See mhphf4 40760 and prjspvs 40934). (Contributed by SN, 23-Nov-2024.)
Assertion
Ref Expression
df-prjcrv ℙ𝕣𝕠𝕛Crv = (𝑛 ∈ ℕ0, 𝑘 ∈ Field ↦ (𝑓 ran ((0...𝑛) mHomP 𝑘) ↦ {𝑝 ∈ (𝑛ℙ𝕣𝕠𝕛n𝑘) ∣ ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g𝑘)}}))
Distinct variable group:   𝑘,𝑛,𝑓,𝑝

Detailed syntax breakdown of Definition df-prjcrv
StepHypRef Expression
1 cprjcrv 40953 . 2 class ℙ𝕣𝕠𝕛Crv
2 vn . . 3 setvar 𝑛
3 vk . . 3 setvar 𝑘
4 cn0 12413 . . 3 class 0
5 cfield 20186 . . 3 class Field
6 vf . . . 4 setvar 𝑓
7 cc0 11051 . . . . . . . 8 class 0
82cv 1540 . . . . . . . 8 class 𝑛
9 cfz 13424 . . . . . . . 8 class ...
107, 8, 9co 7357 . . . . . . 7 class (0...𝑛)
113cv 1540 . . . . . . 7 class 𝑘
12 cmhp 21519 . . . . . . 7 class mHomP
1310, 11, 12co 7357 . . . . . 6 class ((0...𝑛) mHomP 𝑘)
1413crn 5634 . . . . 5 class ran ((0...𝑛) mHomP 𝑘)
1514cuni 4865 . . . 4 class ran ((0...𝑛) mHomP 𝑘)
166cv 1540 . . . . . . . 8 class 𝑓
17 cevl 21481 . . . . . . . . 9 class eval
1810, 11, 17co 7357 . . . . . . . 8 class ((0...𝑛) eval 𝑘)
1916, 18cfv 6496 . . . . . . 7 class (((0...𝑛) eval 𝑘)‘𝑓)
20 vp . . . . . . . 8 setvar 𝑝
2120cv 1540 . . . . . . 7 class 𝑝
2219, 21cima 5636 . . . . . 6 class ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝)
23 c0g 17321 . . . . . . . 8 class 0g
2411, 23cfv 6496 . . . . . . 7 class (0g𝑘)
2524csn 4586 . . . . . 6 class {(0g𝑘)}
2622, 25wceq 1541 . . . . 5 wff ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g𝑘)}
27 cprjspn 40938 . . . . . 6 class ℙ𝕣𝕠𝕛n
288, 11, 27co 7357 . . . . 5 class (𝑛ℙ𝕣𝕠𝕛n𝑘)
2926, 20, 28crab 3407 . . . 4 class {𝑝 ∈ (𝑛ℙ𝕣𝕠𝕛n𝑘) ∣ ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g𝑘)}}
306, 15, 29cmpt 5188 . . 3 class (𝑓 ran ((0...𝑛) mHomP 𝑘) ↦ {𝑝 ∈ (𝑛ℙ𝕣𝕠𝕛n𝑘) ∣ ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g𝑘)}})
312, 3, 4, 5, 30cmpo 7359 . 2 class (𝑛 ∈ ℕ0, 𝑘 ∈ Field ↦ (𝑓 ran ((0...𝑛) mHomP 𝑘) ↦ {𝑝 ∈ (𝑛ℙ𝕣𝕠𝕛n𝑘) ∣ ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g𝑘)}}))
321, 31wceq 1541 1 wff ℙ𝕣𝕠𝕛Crv = (𝑛 ∈ ℕ0, 𝑘 ∈ Field ↦ (𝑓 ran ((0...𝑛) mHomP 𝑘) ↦ {𝑝 ∈ (𝑛ℙ𝕣𝕠𝕛n𝑘) ∣ ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g𝑘)}}))
Colors of variables: wff setvar class
This definition is referenced by:  prjcrvfval  40955
  Copyright terms: Public domain W3C validator