ModuleSubalgebraNormalizationTower.lean
Nyll.SchemeTheory.Normalization.SubalgebraNormalizationTower
3 declarations indexed from sourceView source ↗ Module documentation
Maps in subalgebra normalization towers
Constructs the ring map between normalizations of nested subalgebras. It proves compatibility with the ambient inclusion and injectivity of the tower map.
Declarations
SchemeTheory.subalgebraNormalizationTowerRingMap
DocumentationThe actual map between nested native subalgebra normalizations.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace SchemeTheory
universe u v
variable {A : Type u} {L : Type v}
[CommRing A] [CommRing L] [Algebra A L]
SchemeTheory.subalgebraNormalizationTowerRingMap_comp
DocumentationThe normalization tower is the literal triangle of subtype inclusions.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace SchemeTheory
universe u v
variable {A : Type u} {L : Type v}
[CommRing A] [CommRing L] [Algebra A L]
SchemeTheory.subalgebraNormalizationTowerRingMap_injective
DocumentationThe tower map is injective because its composite is the native ambient inclusion.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace SchemeTheory
universe u v
variable {A : Type u} {L : Type v}
[CommRing A] [CommRing L] [Algebra A L]