Definition df-prjcrv

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 and prjspvs ). (Contributed by SN, 23-Nov-2024)

	Ref	Expression
Assertion	df-prjcrv	⊢ ℙ𝕣𝕠𝕛Crv = ( 𝑛 ∈ ℕ0 , 𝑘 ∈ Field ↦ ( 𝑓 ∈ ∪ ran ( ( 0 ... 𝑛 ) mHomP 𝑘 ) ↦ { 𝑝 ∈ ( 𝑛 ℙ𝕣𝕠𝕛n 𝑘 ) ∣ ( ( ( ( 0 ... 𝑛 ) eval 𝑘 ) ‘ 𝑓 ) “ 𝑝 ) = { ( 0g ‘ 𝑘 ) } } ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cprjcrv	⊢ ℙ𝕣𝕠𝕛Crv
1		vn	⊢ 𝑛
2		cn0	⊢ ℕ0
3		vk	⊢ 𝑘
4		cfield	⊢ Field
5		vf	⊢ 𝑓
6		cc0	⊢ 0
7		cfz	⊢ ...
8	1	cv	⊢ 𝑛
9	6 8 7	co	⊢ ( 0 ... 𝑛 )
10		cmhp	⊢ mHomP
11	3	cv	⊢ 𝑘
12	9 11 10	co	⊢ ( ( 0 ... 𝑛 ) mHomP 𝑘 )
13	12	crn	⊢ ran ( ( 0 ... 𝑛 ) mHomP 𝑘 )
14	13	cuni	⊢ ∪ ran ( ( 0 ... 𝑛 ) mHomP 𝑘 )
15		vp	⊢ 𝑝
16		cprjspn	⊢ ℙ𝕣𝕠𝕛n
17	8 11 16	co	⊢ ( 𝑛 ℙ𝕣𝕠𝕛n 𝑘 )
18		cevl	⊢ eval
19	9 11 18	co	⊢ ( ( 0 ... 𝑛 ) eval 𝑘 )
20	5	cv	⊢ 𝑓
21	20 19	cfv	⊢ ( ( ( 0 ... 𝑛 ) eval 𝑘 ) ‘ 𝑓 )
22	15	cv	⊢ 𝑝
23	21 22	cima	⊢ ( ( ( ( 0 ... 𝑛 ) eval 𝑘 ) ‘ 𝑓 ) “ 𝑝 )
24		c0g	⊢ 0g
25	11 24	cfv	⊢ ( 0g ‘ 𝑘 )
26	25	csn	⊢ { ( 0g ‘ 𝑘 ) }
27	23 26	wceq	⊢ ( ( ( ( 0 ... 𝑛 ) eval 𝑘 ) ‘ 𝑓 ) “ 𝑝 ) = { ( 0g ‘ 𝑘 ) }
28	27 15 17	crab	⊢ { 𝑝 ∈ ( 𝑛 ℙ𝕣𝕠𝕛n 𝑘 ) ∣ ( ( ( ( 0 ... 𝑛 ) eval 𝑘 ) ‘ 𝑓 ) “ 𝑝 ) = { ( 0g ‘ 𝑘 ) } }
29	5 14 28	cmpt	⊢ ( 𝑓 ∈ ∪ ran ( ( 0 ... 𝑛 ) mHomP 𝑘 ) ↦ { 𝑝 ∈ ( 𝑛 ℙ𝕣𝕠𝕛n 𝑘 ) ∣ ( ( ( ( 0 ... 𝑛 ) eval 𝑘 ) ‘ 𝑓 ) “ 𝑝 ) = { ( 0g ‘ 𝑘 ) } } )
30	1 3 2 4 29	cmpo	⊢ ( 𝑛 ∈ ℕ0 , 𝑘 ∈ Field ↦ ( 𝑓 ∈ ∪ ran ( ( 0 ... 𝑛 ) mHomP 𝑘 ) ↦ { 𝑝 ∈ ( 𝑛 ℙ𝕣𝕠𝕛n 𝑘 ) ∣ ( ( ( ( 0 ... 𝑛 ) eval 𝑘 ) ‘ 𝑓 ) “ 𝑝 ) = { ( 0g ‘ 𝑘 ) } } ) )
31	0 30	wceq	⊢ ℙ𝕣𝕠𝕛Crv = ( 𝑛 ∈ ℕ0 , 𝑘 ∈ Field ↦ ( 𝑓 ∈ ∪ ran ( ( 0 ... 𝑛 ) mHomP 𝑘 ) ↦ { 𝑝 ∈ ( 𝑛 ℙ𝕣𝕠𝕛n 𝑘 ) ∣ ( ( ( ( 0 ... 𝑛 ) eval 𝑘 ) ‘ 𝑓 ) “ 𝑝 ) = { ( 0g ‘ 𝑘 ) } } ) )