ModuleKaehlerRankOne_of_transcendental.lean
Nyll.AlgebraicCurves.Differentials.KaehlerRankOne_of_transcendental
7 declarations indexed from sourceView source ↗ Module documentation
Differentials, residues, and divisor correspondences
Singleton bases for polynomial and rational-function differentials and their separable field extensions.
Imports9
- Mathlib.FieldTheory.RatFunc.AsPolynomial
- Mathlib.RingTheory.Etale.Field
- Mathlib.RingTheory.Etale.Kaehler
- Mathlib.RingTheory.Kaehler.Polynomial
- Mathlib.LinearAlgebra.TensorProduct.Basis
- Mathlib.LinearAlgebra.Dimension.StrongRankCondition
- Mathlib.RingTheory.Henselian
- Mathlib.RingTheory.RegularLocalRing.Defs
- Mathlib.RingTheory.SimpleRing.Principal
Imported by3
Declarations
AlgebraicCurves.Differentials.Proofs.KaehlerRankOne_of_transcendental.S12Kaehler.kaehlerPolynomialBasis
DocumentationThe singleton basis of polynomial Kähler differentials obtained from the polynomial differential equivalence.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.KaehlerRankOne_of_transcendental
noncomputable section
open IntermediateField Polynomial TensorProduct Module
namespace S12Kaehler
variable (K : Type*) [Field K]
AlgebraicCurves.Differentials.Proofs.KaehlerRankOne_of_transcendental.S12Kaehler.instFormallyEtalePolynomialRatFunc
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.KaehlerRankOne_of_transcendental
noncomputable section
open IntermediateField Polynomial TensorProduct Module
namespace S12Kaehler
variable (K : Type*) [Field K]
AlgebraicCurves.Differentials.Proofs.KaehlerRankOne_of_transcendental.S12Kaehler.kaehlerRatFuncBasis
DocumentationThe singleton basis of rational-function differentials obtained by formally étale base change.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.KaehlerRankOne_of_transcendental
noncomputable section
open IntermediateField Polynomial TensorProduct Module
namespace S12Kaehler
variable (K : Type*) [Field K]
AlgebraicCurves.Differentials.Proofs.KaehlerRankOne_of_transcendental.S12Kaehler.kaehlerOfRatFuncTowerBasis
DocumentationThe singleton differential basis transported along a separable rational-function-field tower.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.KaehlerRankOne_of_transcendental
noncomputable section
open IntermediateField Polynomial TensorProduct Module
namespace S12Kaehler
variable (K : Type*) [Field K]
variable {F : Type*} [Field F] [Algebra K F]
AlgebraicCurves.Differentials.Proofs.KaehlerRankOne_of_transcendental.S12Kaehler.kaehlerRankOne_of_ratFuncTower
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.KaehlerRankOne_of_transcendental
noncomputable section
open IntermediateField Polynomial TensorProduct Module
namespace S12Kaehler
variable (K : Type*) [Field K]
variable {F : Type*} [Field F] [Algebra K F]
AlgebraicCurves.Differentials.Proofs.KaehlerRankOne_of_transcendental.S12Kaehler.kaehlerRankOne_of_transcendental
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.KaehlerRankOne_of_transcendental
noncomputable section
open IntermediateField Polynomial TensorProduct Module
namespace S12Kaehler
variable (K : Type*) [Field K]
variable {F : Type*} [Field F] [Algebra K F]
variable {K}
AlgebraicCurve.kaehlerRankOne_of_transcendental
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.KaehlerRankOne_of_transcendental