Modulebijective_appTop_of_universallyClosed_of_geometricallyReduced_of_geometricallyConnected.lean
Nyll.AlgebraicCurves.Geometry.Curves.bijective_appTop_of_universallyClosed_of_geometricallyReduced_of_geometricallyConnected
6 declarations indexed from sourceView source ↗ Module documentation
bijective app Top of universally Closed of geometrically Reduced of geometrically
Connected
Imports15
- Mathlib.Algebra.Category.Ring.Constructions
- Mathlib.AlgebraicGeometry.Properties
- Mathlib.AlgebraicGeometry.Geometrically.Connected
- Mathlib.AlgebraicGeometry.Geometrically.Reduced
- Mathlib.AlgebraicGeometry.Morphisms.Flat
- Mathlib.AlgebraicGeometry.Morphisms.Proper
- Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
- Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
- Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
- Mathlib.RingTheory.Artinian.Module
- Mathlib.RingTheory.Artinian.Ring
- Mathlib.RingTheory.RingHom.Integral
- Mathlib.RingTheory.TensorProduct.Free
- Mathlib.Tactic.ByContra
- Mathlib.Tactic.Ext
Imported by4
Declarations
AlgebraicCurves.Geometry.Curves.Proofs.bijective_appTop_of_universallyClosed_of_geometricallyReduced_of_geometricallyConnected.SolFieldCaseH0.subsingleton_maximalSpectrum_of_idem
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace bijective_appTop_of_universallyClosed_of_geometricallyReduced_of_geometricallyConnected
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits TopologicalSpace Opposite
universe u
namespace SolFieldCaseH0
section Algebra
variable {K A : Type*} [Field K] [CommRing A] [Algebra K A]
AlgebraicCurves.Geometry.Curves.Proofs.bijective_appTop_of_universallyClosed_of_geometricallyReduced_of_geometricallyConnected.SolFieldCaseH0.isField_of_isReduced_of_isIntegral_of_idem
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace bijective_appTop_of_universallyClosed_of_geometricallyReduced_of_geometricallyConnected
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits TopologicalSpace Opposite
universe u
namespace SolFieldCaseH0
section Algebra
variable {K A : Type*} [Field K] [CommRing A] [Algebra K A]
AlgebraicCurves.Geometry.Curves.Proofs.bijective_appTop_of_universallyClosed_of_geometricallyReduced_of_geometricallyConnected.SolFieldCaseH0.idem_trivial_of_connectedSpace
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace bijective_appTop_of_universallyClosed_of_geometricallyReduced_of_geometricallyConnected
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits TopologicalSpace Opposite
universe u
namespace SolFieldCaseH0
section Idem
AlgebraicCurves.Geometry.Curves.Proofs.bijective_appTop_of_universallyClosed_of_geometricallyReduced_of_geometricallyConnected.SolFieldCaseH0.nontrivial_sections_top
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace bijective_appTop_of_universallyClosed_of_geometricallyReduced_of_geometricallyConnected
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits TopologicalSpace Opposite
universe u
namespace SolFieldCaseH0
AlgebraicCurves.Geometry.Curves.Proofs.bijective_appTop_of_universallyClosed_of_geometricallyReduced_of_geometricallyConnected.SolFieldCaseH0.main
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace bijective_appTop_of_universallyClosed_of_geometricallyReduced_of_geometricallyConnected
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits TopologicalSpace Opposite
universe u
namespace SolFieldCaseH0
section Main
open TensorProduct
variable {K : Type u} [Field K] {X : Scheme.{u}} (f : X ⟶ Spec (.of K))
[UniversallyClosed f] [GeometricallyReduced f] [GeometricallyConnected f]
AlgebraicGeometry.bijective_appTop_of_universallyClosed_of_geometricallyReduced_of_geometricallyConnected
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicGeometry
universe u
open _root_.AlgebraicCurves.Geometry.Curves.Proofs in
open bijective_appTop_of_universallyClosed_of_geometricallyReduced_of_geometricallyConnected in
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits TopologicalSpace Opposite in