ModuleCommAlgIdealTameProperties.lean
Nyll.EtaleFundamentalGroups.Inertia.CommAlgIdealTameProperties
2 declarations indexed from sourceView source ↗ Module documentation
Positivity and invertibility of intrinsic tame orders
Proves positivity of the intrinsic finite tame order and its invertibility in the original local coefficient ring under the stated hypotheses.
Declarations
EtaleFundamentalGroups.Inertia.commAlgIdealTameOrder_pos
DocumentationPositivity for the intrinsic actual finite normalization action.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace EtaleFundamentalGroups.Inertia
universe u v
variable (A : Type u) [CommRing A] (B : CommAlgCat.{v} A)
[IsDedekindDomain B] [Finite (B ≃ₐ[A] B)]
(Q : Ideal B) [Q.IsPrime] (hQ : Q ≠ ⊥)
EtaleFundamentalGroups.Inertia.commAlgIdealTameOrder_isUnit
DocumentationBase invertibility for the intrinsic actual coefficient automorphisms.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace EtaleFundamentalGroups.Inertia
universe u v
variable (A : Type u) [CommRing A] (B : CommAlgCat.{v} A)
[IsDedekindDomain B] [Finite (B ≃ₐ[A] B)]
(Q : Ideal B) [Q.IsPrime] (hQ : Q ≠ ⊥)