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 41454
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 41254 and prjspvs 41434). (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 41453 . 2 class ℙ𝕣𝕠𝕛Crv
2 vn . . 3 setvar 𝑛
3 vk . . 3 setvar 𝑘
4 cn0 12474 . . 3 class 0
5 cfield 20362 . . 3 class Field
6 vf . . . 4 setvar 𝑓
7 cc0 11112 . . . . . . . 8 class 0
82cv 1540 . . . . . . . 8 class 𝑛
9 cfz 13486 . . . . . . . 8 class ...
107, 8, 9co 7411 . . . . . . 7 class (0...𝑛)
113cv 1540 . . . . . . 7 class 𝑘
12 cmhp 21678 . . . . . . 7 class mHomP
1310, 11, 12co 7411 . . . . . 6 class ((0...𝑛) mHomP 𝑘)
1413crn 5677 . . . . 5 class ran ((0...𝑛) mHomP 𝑘)
1514cuni 4908 . . . 4 class ran ((0...𝑛) mHomP 𝑘)
166cv 1540 . . . . . . . 8 class 𝑓
17 cevl 21640 . . . . . . . . 9 class eval
1810, 11, 17co 7411 . . . . . . . 8 class ((0...𝑛) eval 𝑘)
1916, 18cfv 6543 . . . . . . 7 class (((0...𝑛) eval 𝑘)‘𝑓)
20 vp . . . . . . . 8 setvar 𝑝
2120cv 1540 . . . . . . 7 class 𝑝
2219, 21cima 5679 . . . . . 6 class ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝)
23 c0g 17387 . . . . . . . 8 class 0g
2411, 23cfv 6543 . . . . . . 7 class (0g𝑘)
2524csn 4628 . . . . . 6 class {(0g𝑘)}
2622, 25wceq 1541 . . . . 5 wff ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g𝑘)}
27 cprjspn 41438 . . . . . 6 class ℙ𝕣𝕠𝕛n
288, 11, 27co 7411 . . . . 5 class (𝑛ℙ𝕣𝕠𝕛n𝑘)
2926, 20, 28crab 3432 . . . 4 class {𝑝 ∈ (𝑛ℙ𝕣𝕠𝕛n𝑘) ∣ ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g𝑘)}}
306, 15, 29cmpt 5231 . . 3 class (𝑓 ran ((0...𝑛) mHomP 𝑘) ↦ {𝑝 ∈ (𝑛ℙ𝕣𝕠𝕛n𝑘) ∣ ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g𝑘)}})
312, 3, 4, 5, 30cmpo 7413 . 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  41455
  Copyright terms: Public domain W3C validator