ModuleFiniteDiagonal.lean
Nyll.SchemeTheory.RingTheory.Ramification.Unramified.FiniteDiagonal
6 declarations indexed from sourceView source ↗ Module documentation
The diagonal factor of a finite formally unramified algebra
For a finite formally unramified R-algebra S, the canonical separability element Algebra.FormallyUnramified.elem R S cuts out the diagonal component of S \otimes_R S. After inverting this element, multiplication identifies that component with S itself as an S-algebra.
The proof first derives the idempotence of the separability element from its defining switching and multiplication identities. It then uses the universal property of Localization.Away and proves bijectivity by exhibiting S, with the multiplication algebra structure, as a second localization away from the same element.
Imports2
- Mathlib.RingTheory.Localization.Away.Basic
- Mathlib.RingTheory.Unramified.Finite
Imported by2
Declarations
EtaleFundamentalGroups.mul_formallyUnramifiedElem_eq_lmul_tmul_one_mul
DocumentationMultiplication by the separability element turns every tensor into the left-factor image of its product.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
universe u v
variable {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S]
[Module.Finite R S] [Algebra.FormallyUnramified R S]
EtaleFundamentalGroups.formallyUnramifiedElem_isIdempotentElem
DocumentationThe canonical separability element of a finite formally unramified algebra is idempotent.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
universe u v
variable {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S]
[Module.Finite R S] [Algebra.FormallyUnramified R S]
EtaleFundamentalGroups.finiteUnramifiedDiagonalAwayMul
DocumentationMultiplication, extended across the Away localization at the separability element.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
universe u v
variable {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S]
[Module.Finite R S] [Algebra.FormallyUnramified R S]
EtaleFundamentalGroups.finiteUnramifiedDiagonalAwayMul_algebraMap
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
universe u v
variable {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S]
[Module.Finite R S] [Algebra.FormallyUnramified R S]
EtaleFundamentalGroups.finiteUnramifiedDiagonalAwayMul_bijective
DocumentationThe multiplication map from the diagonal Away factor is bijective.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
universe u v
variable {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S]
[Module.Finite R S] [Algebra.FormallyUnramified R S]
EtaleFundamentalGroups.finiteUnramifiedDiagonalAwayEquiv
DocumentationThe diagonal factor of S \otimes_R S selected by the canonical separability element is S itself.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
universe u v
variable {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S]
[Module.Finite R S] [Algebra.FormallyUnramified R S]