← all areas

Namespace TwoChartCech 37 theorems

— 19 · Cover 7 · GrothendieckComplex 1 · Mumford 6 · Sections 4

directly in TwoChartCech 19

• A finite free two-term model for ker d after every base change TwoChartCech.exists_twoTermComplex_kerMapBaseChange_bijective 0 below · cited by 3 · depth 15
• Finiteness of ker(d⊗ A) after base change TwoChartCech.finite_ker_baseChange_of_finite_ker_of_finite_coker 2 below · cited by 1 · depth 15
• Projective kernel from constant fibre dimension via a free model TwoChartCech.projective_ker_of_isReduced_of_kerMapBaseChange_bijective 1 below · cited by 2 · depth 15
• Two glued lines: h⁰ ≤ 1 at multidegree (0,0) TwoChartCech.finrank_H0_gluedLinesSections_zero_zero_le_one 0 below · cited by 2 · depth 16
• Euler characteristic n+m+2-s for two glued lines TwoChartCech.finrank_H0_sub_finrank_H1_gluedLinesSections 1 below · cited by 7 · depth 16
• Local constancy of the fibrewise Euler characteristic TwoChartCech.isLocallyConstant_fibreEulerChar 4 below · cited by 4 · depth 16
• Invertible sections on glued lines are the model ones TwoChartCech.exists_linearEquiv_gluedLinesSections_of_invertible 6 below · cited by 1 · depth 17
• Invertible sections on the glued-lines cover are the explicit model TwoChartCech.exists_semilinearEquiv_gluedLinesSections_of_invertible 6 below · cited by 1 · depth 17
• Čech cohomology of glued lines in multidegree (s-1,0) TwoChartCech.finrank_H0_gluedLinesSections_eq_one_and_subsingleton_H1 0 below · cited by 4 · depth 17
• Glued line bundle trivial iff n=m=0 and λ constant TwoChartCech.gluedLinesSections_nonempty_linearEquiv_structureSheaf_iff 0 below · cited by 1 · depth 17
• Upper semicontinuity of ker dimension for a two-term complex TwoChartCech.isClosed_setOf_le_finrank_ker_baseChange 5 below · cited by 5 · depth 17
• Existence of the h⁰-family of a flat two-term complex TwoChartCech.exists_fibreH0Family 3 below · cited by 1 · depth 18
• Invertible modules over the glued-lines chart ring are node twists TwoChartCech.exists_linearEquiv_gluedLinesM0_of_invertible 2 below · cited by 2 · depth 18
• Invertible modules over the glued-lines chart ring A₁ TwoChartCech.exists_linearEquiv_gluedLinesM1_of_invertible 2 below · cited by 2 · depth 18
• Invariance of dimker(d⊗ K) under field extension TwoChartCech.finrank_ker_baseChange_eq_of_field_extension 0 below · cited by 3 · depth 18
• Snake fragment: ker d_E=0 makes ker d_S finite TwoChartCech.kerMap_injective_of_H0_eq_zero 0 below · cited by 1 · depth 18
• Glued lines: h⁰ = n+1-s in bidegree (n,m), m<0 TwoChartCech.finrank_H0_gluedLinesSections_of_sub_one_le_of_neg 0 below · cited by 2 · depth 19
• Transitivity of base change on kernels of a linear map TwoChartCech.nonempty_kerBaseChangeTowerEquiv 0 below · cited by 1 · depth 19
• Lower bound h⁰ ≥ (n+1)⁺ + (m+1)⁺ - s TwoChartCech.toNat_add_toNat_le_finrank_H0_gluedLinesSections_add 2 below · cited by 2 · depth 19

TwoChartCech.Cover 7

• Lifting idempotents mod p with stable p-torsion in Čech H¹ TwoChartCech.Cover.exists_overlap_eq_sub_mem_span_of_H1_torsion_stable 0 below · cited by 2 · depth 16
• Chart residue pairing equals the function-field Serre pairing TwoChartCech.Cover.serrePairingInt_eq_serrePairing 0 below · cited by 2 · depth 25
• Laurent-chart residue equals the Kähler residue term at v TwoChartCech.Cover.LaurentChart.residue_eq_kaehlerResidueTerm 4 below · cited by 2 · depth 26
• Residues along Laurent charts commute with base change TwoChartCech.Cover.LaurentChart.residue_mapOfRingHom 0 below · cited by 1 · depth 26
• Residue vanishes on forms pulled back from the first chart TwoChartCech.Cover.LaurentChart.residue_r0 0 below · cited by 1 · depth 26
• Vanishing of chart residue sums from the residue theorem TwoChartCech.Cover.sum_residue_eq_zero_of_residueTheorem 0 below · cited by 1 · depth 26
• Čech H¹ and principal units of a square-zero thickening TwoChartCech.Cover.squareZeroUnit_cohomologous_iff_and_exists 0 below · cited by 1 · depth 27

TwoChartCech.GrothendieckComplex 1

• Existence of a Grothendieck complex over a Noetherian local ring TwoChartCech.GrothendieckComplex.nonempty_of_isLocalRing 0 below · cited by 2 · depth 16

TwoChartCech.Mumford 6

• Cohomology and base change in degree 0 over a Noetherian base TwoChartCech.Mumford.projective_ker_of_fibre_surjective 5 below · cited by 4 · depth 15
• Mumford truncation computes coker(d⊗ A) for all A TwoChartCech.Mumford.bijective_cokerMapBaseChange 0 below · cited by 2 · depth 16
• Mumford truncation computes ker(d⊗ A) after any base change TwoChartCech.Mumford.bijective_kerMapBaseChange 0 below · cited by 4 · depth 16
• Finite generation of Mumford's degree-zero truncation term K⁰ TwoChartCech.Mumford.finite_K0 0 below · cited by 4 · depth 16
• Projectivity of Mumford's truncation term K⁰ TwoChartCech.Mumford.projective_K0 2 below · cited by 1 · depth 16
• Flatness of the Mumford truncation term K⁰ TwoChartCech.Mumford.flat_K0 0 below · cited by 3 · depth 17

TwoChartCech.Sections 4

• Finiteness of Čech H⁰ for chart-finite two-chart data TwoChartCech.Sections.finite_H0_of_chartFinite 2 below · cited by 2 · depth 17
• Finiteness of Čech H¹ for chart-finite two-chart data TwoChartCech.Sections.finite_H1_of_chartFinite 0 below · cited by 3 · depth 17
• Transport of two-chart Čech H⁰ and H¹ along equivalences TwoChartCech.Sections.nonempty_linearEquiv_H0_and_H1_of_linearEquiv 0 below · cited by 7 · depth 17
• Finiteness of two-chart Čech H¹ for submodules of F TwoChartCech.Sections.finite_H1_ofSubmodules_of_forall_exists_pow_mul_mem 0 below · cited by 1 · depth 28