GeometricallyIrreducible_geometricallyConnected.lean
Nyll.AlgebraicCurves.Geometry.Curves.GeometricallyIrreducible_geometricallyConnected
0 declarations indexed from sourceView source ↗
Module documentation
Geometric irreducibility implies geometric connectedness
The public theorem GeometricallyIrreducible.geometricallyConnected is owned by SchemeTheory and remains available through this existing import path.
Imported by14
- Nyll.AlgebraicCurves.Geometry.AbelianSchemes.Theorems.AbelianSchemePropertyBundle_geometricallyIntegral
- Nyll.AlgebraicCurves.Geometry.AbelianSchemes.Theorems.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
- Nyll.AlgebraicCurves.Geometry.Curves.All
- Nyll.JacobianVarieties.Albanese.AlbaneseChartGlue
- Nyll.JacobianVarieties.Albanese.LineBundleSumInvariance
- Nyll.JacobianVarieties.Albanese.LinearPencilSums
- Nyll.JacobianVarieties.Albanese.SeparableAlbaneseChartGlue
- Nyll.JacobianVarieties.JacobianChallenge
- Nyll.JacobianVarieties.Picard.IsProper_and_geometricallyConnected_of_representsRelSubPic_algEquivZeroCut_of_finiteMapData
- Nyll.JacobianVarieties.Picard.RelativeGroupLaw_endDegree_nsmul_idPoint_eq_pow_of_natCast_ne_zero
- Nyll.JacobianVarieties.Picard.RelativeGroupLaw_exists_polynomial_eval_eq_endDegree_zpow_mul_of_abelianSchemePropertyBundle
- Nyll.JacobianVarieties.Picard.UnpointedAbelJacobi
- Nyll.JacobianVarieties.Picard.UnpointedAlbanese
- Nyll.JacobianVarieties.Picard.UnpointedJacobian
This module has no indexed declarations. Its imports and full source are available here.