This file records the opening datum of abstract valuation theory and the residue and ramification indices attached to inclusions of abstract fields. As in, a field is represented contravariantly by a closed subgroup of the ambient profinite group.
The multiplicative presentation of ℤ̂; multiplication here is addition in the profinite integers.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe uabbrev ZHatMul : Type 0The degree datum on a topological group: a continuous surjection d : G → ℤ̂. Profinite hypotheses belong to the ambient group and are requested only by results that use them; they are not duplicated as proof fields inside this datum.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe ustructure DegreeData (G : Type*) [Group G] [TopologicalSpace G] where
/-- The continuous degree homomorphism to the profinite integers. -/
degree : G →ₜ* ZHatMul
/-- The degree homomorphism is surjective. -/
degree_surjective : Function.Surjective degreeThe distinguished base field, represented contravariantly by the full ambient group.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]def baseField (G : Type u) [Group G] [TopologicalSpace G] : ClosedSubgroup G where
toSubgroup := ⊤
isClosed' := isClosed_univThe distinguished base field is represented by the full ambient subgroup.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]theorem baseField_toSubgroup (G : Type u) [Group G] [TopologicalSpace G] :
(baseField G).toSubgroup = ⊤Every abstract field lies over the distinguished base field.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]theorem le_baseField (K : ClosedSubgroup G) :
K.toSubgroup ≤ (baseField G).toSubgroupThe inertia group I = ker d, including its closedness.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeDatadef inertia (D : DegreeData G) : ClosedSubgroup G where
toSubgroup := D.degree.toMonoidHom.ker
isClosed' := by
change IsClosed {g : G | (D.degree g).toAdd = 0}
exact isClosed_eq D.degree.continuous_toFun continuous_constAn element is inertial exactly when its degree is the multiplicative identity.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeDatatheorem mem_inertia_iff (D : DegreeData G) (g : G) :
g ∈ D.inertia ↔ D.degree g = 1The restriction of d to the subgroup representing an abstract field.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeDatadef restrictedDegree (D : DegreeData G) (K : ClosedSubgroup G) :
K.toSubgroup →ₜ* ZHatMul where
toMonoidHom := D.degree.toMonoidHom.comp K.toSubgroup.subtype
continuous_toFun := D.degree.continuous_toFun.comp continuous_subtype_valThe restricted degree map evaluates through the underlying ambient element.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeDatatheorem restrictedDegree_apply (D : DegreeData G) (K : ClosedSubgroup G)
(k : K.toSubgroup) : D.restrictedDegree K k = D.degree k.1The image d(G_K) in ℤ̂.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeDatadef fieldImage (D : DegreeData G) (K : ClosedSubgroup G) : Subgroup ZHatMulThe field's degree image is the image of its subgroup under the ambient degree map.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeDatatheorem fieldImage_eq_map (D : DegreeData G) (K : ClosedSubgroup G) :
D.fieldImage K = K.toSubgroup.map D.degree.toMonoidHomThe inertia group I_K = G_K ∩ I over K.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeDatadef fieldInertia (D : DegreeData G) (K : ClosedSubgroup G) : ClosedSubgroup GField inertia consists of field elements whose ambient degree is one.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeDatatheorem mem_fieldInertia_iff (D : DegreeData G) (K : ClosedSubgroup G) (g : G) :
g ∈ D.fieldInertia K ↔ g ∈ K ∧ D.degree g = 1I_K viewed inside G_K; equivalently, the kernel of d|G_K.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeDatadef fieldInertiaWithin (D : DegreeData G) (K : ClosedSubgroup G) :
Subgroup K.toSubgroupThe degree kernel defining inertia inside a field subgroup is normal.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeDatainstance fieldInertiaWithin_normal (D : DegreeData G) (K : ClosedSubgroup G) :
(D.fieldInertiaWithin K).NormalMembership in internal field inertia is equivalent to having ambient degree one.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeDatatheorem mem_fieldInertiaWithin_iff (D : DegreeData G) (K : ClosedSubgroup G)
(k : K.toSubgroup) : k ∈ D.fieldInertiaWithin K ↔ D.degree k.1 = 1The absolute residue degree as the cardinality of the actual quotient of ZHat by the degree image.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeDatadef residueDegreeCardinal (D : DegreeData G)
(K : ClosedSubgroup G) : CardinalThe actual quotient whose cardinality is the absolute residue degree.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeDatadef residueQuotient (D : DegreeData G) (K : ClosedSubgroup G) : TypeThe cardinal residue degree is the cardinality of the concrete residue quotient.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeDatatheorem residueDegreeCardinal_eq_mk_residueQuotient
(D : DegreeData G) (K : ClosedSubgroup G) :
D.residueDegreeCardinal K = Cardinal.mk (D.residueQuotient K)The distinguished base field has absolute residue degree one, without passing through a natural-valued subgroup index.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeDatatheorem residueDegreeCardinal_baseField (D : DegreeData G) :
D.residueDegreeCardinal (baseField G) = 1An abstract field together with finiteness of its actual degree-image quotient. Its numerical residue degree is therefore genuinely positive.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeDatastructure FiniteResidueAbstractField (D : DegreeData G) where
/-- The closed subgroup representing the abstract field. -/
field : ClosedSubgroup G
/-- The field's residue quotient is finite. -/
finiteResidueQuotient : Finite (D.residueQuotient field)Bundle a field at the boundary where its actual residue quotient is known to be finite.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace FiniteResidueAbstractField
variable {D : DegreeData G}def ofField (D : DegreeData G) (K : ClosedSubgroup G)
[hfinite : Finite (D.residueQuotient K)] :
FiniteResidueAbstractField D where
field := K
finiteResidueQuotient := hfiniteThe underlying subgroup.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace FiniteResidueAbstractField
variable {D : DegreeData G}def toSubgroup (K : FiniteResidueAbstractField D) : Subgroup GA finite-residue abstract field supplies finiteness of its residue quotient.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace FiniteResidueAbstractField
variable {D : DegreeData G}instance (K : FiniteResidueAbstractField D) :
Finite (D.residueQuotient K.field)The positive absolute residue degree.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace FiniteResidueAbstractField
variable {D : DegreeData G}def residueDegree (K : FiniteResidueAbstractField D) : ℕ+The natural value of the positive residue degree is the quotient's Nat.card.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace FiniteResidueAbstractField
variable {D : DegreeData G}theorem residueDegree_coe (K : FiniteResidueAbstractField D) :
(K.residueDegree : ℕ) = Nat.card (D.residueQuotient K.field)Cardinal-to-positive-natural specialization at the finite boundary.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace FiniteResidueAbstractField
variable {D : DegreeData G}theorem residueDegreeCardinal_eq_coe
(K : FiniteResidueAbstractField D) :
D.residueDegreeCardinal K.field = ((K.residueDegree : ℕ) : Cardinal)An abstract field extension, including the containment which makes the notation L / K meaningful in the closed-subgroup model. Keeping this proof in the object prevents predicates for extensions from being formed for unrelated closed subgroups.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeDatastructure AbstractExtension (G : Type*) [Group G] [TopologicalSpace G] where
/-- The closed subgroup contravariantly representing the extension field. -/
field : ClosedSubgroup G
/-- The closed subgroup contravariantly representing the base field. -/
base : ClosedSubgroup G
/-- Contravariance turns the field inclusion into this subgroup inclusion. -/
below : field.toSubgroup ≤ base.toSubgroupThe subgroup of the base group represented by the extension field. This projection packages the proof-dependent subgroupOf construction behind the extension object.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace AbstractExtensiondef subgroup (E : AbstractExtension G) : Subgroup E.base.toSubgroupThe actual relative coset space of an abstract extension.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace AbstractExtensiondef quotient (E : AbstractExtension G) : Type uThe honest cardinal degree of an arbitrary abstract extension. Unlike the raw natural-valued subgroup index, this does not encode infinity as zero.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace AbstractExtensiondef degreeCardinal (E : AbstractExtension G) : CardinalThe cardinal degree of an abstract extension is the cardinality of its coset space.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace AbstractExtensiontheorem degreeCardinal_eq_mk_quotient (E : AbstractExtension G) :
E.degreeCardinal = Cardinal.mk E.quotientThe relative residue degree of an arbitrary abstract extension, as the cardinality of the actual coset type of degree images. This is the canonical general API: an infinite residue degree remains an infinite cardinal.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace AbstractExtensiondef relativeResidueDegreeCardinal
(E : AbstractExtension G) (D : DegreeData G) : CardinalThe relative ramification index of an arbitrary abstract extension, as the cardinality of the actual coset type inside the degree kernel. In particular, infinity is not encoded as zero.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace AbstractExtensiondef relativeRamificationIndexCardinal
(E : AbstractExtension G) (D : DegreeData G) : CardinalThe cardinal-valued fundamental identity for an arbitrary abstract extension. The residue cardinal is lifted from the universe of ZHat; no finiteness assumption or infinite-index convention is involved.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace AbstractExtensiontheorem degreeCardinal_eq_relativeResidueDegreeCardinal_mul_relativeRamificationIndexCardinal
(E : AbstractExtension G) (D : DegreeData G) :
E.degreeCardinal =
Cardinal.lift.{u} (E.relativeResidueDegreeCardinal D) *
E.relativeRamificationIndexCardinal DCardinal Frobenius residue-degree compatibility: the relative residue cardinal times the absolute residue cardinal of the base is the absolute residue cardinal of the extension field.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace AbstractExtensiontheorem relativeResidueDegreeCardinal_mul_residueDegreeCardinal
(E : AbstractExtension G) (D : DegreeData G) :
E.relativeResidueDegreeCardinal D * D.residueDegreeCardinal E.base =
D.residueDegreeCardinal E.fieldA composable tower of abstract extensions, represented by three closed subgroups and the two adjacent containments.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace AbstractExtensionstructure Tower (G : Type*) [Group G] [TopologicalSpace G] where
/-- The closed subgroup representing the top field. -/
top : ClosedSubgroup G
/-- The closed subgroup representing the middle field. -/
middle : ClosedSubgroup G
/-- The closed subgroup representing the base field. -/
base : ClosedSubgroup G
/-- Contravariant containment for the top-to-middle extension. -/
top_le_middle : top.toSubgroup ≤ middle.toSubgroup
/-- Contravariant containment for the middle-to-base extension. -/
middle_le_base : middle.toSubgroup ≤ base.toSubgroupThe upper extension in a tower.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace AbstractExtension
namespace Tower
variable (T : Tower G)def topExtension : AbstractExtension G where
field := T.top
base := T.middle
below := T.top_le_middleThe lower extension in a tower.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace AbstractExtension
namespace Tower
variable (T : Tower G)def baseExtension : AbstractExtension G where
field := T.middle
base := T.base
below := T.middle_le_baseThe composite extension in a tower.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace AbstractExtension
namespace Tower
variable (T : Tower G)def totalExtension : AbstractExtension G where
field := T.top
base := T.base
below := T.top_le_middle.trans T.middle_le_baseCardinal degrees multiply in an arbitrary abstract-extension tower.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace AbstractExtension
namespace Tower
variable (T : Tower G)theorem degreeCardinal_mul :
T.topExtension.degreeCardinal * T.baseExtension.degreeCardinal =
T.totalExtension.degreeCardinalCardinal residue degrees multiply in an arbitrary abstract-extension tower.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace AbstractExtension
namespace Tower
variable (T : Tower G)theorem relativeResidueDegreeCardinal_mul (D : DegreeData G) :
T.topExtension.relativeResidueDegreeCardinal D *
T.baseExtension.relativeResidueDegreeCardinal D =
T.totalExtension.relativeResidueDegreeCardinal DCardinal ramification indices multiply in an arbitrary abstract-extension tower.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace AbstractExtension
namespace Tower
variable (T : Tower G)theorem relativeRamificationIndexCardinal_mul (D : DegreeData G) :
T.topExtension.relativeRamificationIndexCardinal D *
T.baseExtension.relativeRamificationIndexCardinal D =
T.totalExtension.relativeRamificationIndexCardinal DAn abstract extension is unramified when the inertia subgroup of its base is already contained in the subgroup representing its field. This containment is the definition; it does not pass through a natural-valued index that would encode an infinite index as zero.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace AbstractExtensiondef IsUnramified (E : AbstractExtension G) (D : DegreeData G) : PropAn abstract extension is totally ramified when the degree image of its base is contained in the degree image of its field.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace AbstractExtensiondef IsTotallyRamified (E : AbstractExtension G) (D : DegreeData G) : PropAn extension is unramified exactly when the inertia subgroup of its base is contained in the subgroup representing its field. The containment needed to form the extension is carried by E.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace AbstractExtensiontheorem isUnramified_iff_inertia_le (E : AbstractExtension G) (D : DegreeData G) :
E.IsUnramified D ↔
E.base.toSubgroup ⊓ D.degree.toMonoidHom.ker ≤ E.field.toSubgroupAn extension is totally ramified exactly when the degree image of its base is contained in the degree image of its field.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace AbstractExtensiontheorem isTotallyRamified_iff_image_le (E : AbstractExtension G) (D : DegreeData G) :
E.IsTotallyRamified D ↔
E.base.toSubgroup.map D.degree.toMonoidHom ≤
E.field.toSubgroup.map D.degree.toMonoidHomAn unramified extension has cardinal ramification index one.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace AbstractExtensiontheorem relativeRamificationIndexCardinal_eq_one_of_isUnramified
(E : AbstractExtension G) (D : DegreeData G) (hE : E.IsUnramified D) :
E.relativeRamificationIndexCardinal D = 1A totally ramified extension has cardinal residue degree one.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace AbstractExtensiontheorem relativeResidueDegreeCardinal_eq_one_of_isTotallyRamified
(E : AbstractExtension G) (D : DegreeData G)
(hE : E.IsTotallyRamified D) :
E.relativeResidueDegreeCardinal D = 1For an unramified extension, its cardinal degree is its lifted residue degree.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace AbstractExtensiontheorem degreeCardinal_eq_lift_relativeResidueDegreeCardinal_of_isUnramified
(E : AbstractExtension G) (D : DegreeData G) (hE : E.IsUnramified D) :
E.degreeCardinal =
Cardinal.lift.{u} (E.relativeResidueDegreeCardinal D)For a totally ramified extension, its cardinal degree is its ramification cardinal.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace AbstractExtensiontheorem degreeCardinal_eq_relativeRamificationIndexCardinal_of_isTotallyRamified
(E : AbstractExtension G) (D : DegreeData G)
(hE : E.IsTotallyRamified D) :
E.degreeCardinal = E.relativeRamificationIndexCardinal DA (not necessarily finite) Galois extension above K. Normality and the inclusion of the upper field are carried by the object, while no finiteness assumption is introduced.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeDatastructure GaloisSubextension (K : ClosedSubgroup G) where
/-- The closed subgroup representing the top field. -/
field : ClosedSubgroup G
/-- The top-field subgroup is contained in the base-field subgroup. -/
below : field.toSubgroup ≤ K.toSubgroup
/-- The relative subgroup is normal in the base-field subgroup. -/
normal : (extensionSubgroup K field below).NormalForget normality while retaining the underlying abstract extension.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace GaloisSubextension
variable {K : ClosedSubgroup G}def toAbstractExtension (L : GaloisSubextension K) :
DegreeData.AbstractExtension G where
field := L.field
base := K
below := L.belowThe actual quotient represented by a Galois subextension. This is a named object boundary rather than a transparent abbreviation.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace GaloisSubextension
variable {K : ClosedSubgroup G}def extensionQuotient (L : GaloisSubextension K) : Type uStructural unramifiedness of a Galois subextension.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace GaloisSubextension
variable {K : ClosedSubgroup G}def IsUnramified (L : GaloisSubextension K) (D : DegreeData G) : PropStructural total ramification of a Galois subextension.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace GaloisSubextension
variable {K : ClosedSubgroup G}def IsTotallyRamified (L : GaloisSubextension K) (D : DegreeData G) : PropA Galois subextension has a normal subgroup inside its base subgroup.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace GaloisSubextension
variable {K : ClosedSubgroup G}instance extensionSubgroup_normalInstance (L : GaloisSubextension K) :
(extensionSubgroup K L.field L.below).NormalThe group structure transported across the named quotient boundary.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace GaloisSubextension
variable {K : ClosedSubgroup G}instance extensionQuotient_groupInstance (L : GaloisSubextension K) :
Group L.extensionQuotientComparison with the quotient presentation used by the underlying group library.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace GaloisSubextension
variable {K : ClosedSubgroup G}def extensionQuotientMulEquiv (L : GaloisSubextension K) :
L.extensionQuotient ≃*
(K.toSubgroup ⧸ extensionSubgroup K L.field L.below)The canonical quotient projection for a Galois subextension.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace GaloisSubextension
variable {K : ClosedSubgroup G}def extensionQuotientMk (L : GaloisSubextension K) :
K.toSubgroup →* L.extensionQuotientThe named quotient projection agrees with QuotientGroup.mk under the comparison equivalence.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace GaloisSubextension
variable {K : ClosedSubgroup G}theorem extensionQuotientMk_apply (L : GaloisSubextension K)
(k : K.toSubgroup) :
L.extensionQuotientMulEquiv (L.extensionQuotientMk k) =
(QuotientGroup.mk k :
K.toSubgroup ⧸ extensionSubgroup K L.field L.below)Eliminate a Galois quotient without exposing a chosen representative.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace GaloisSubextension
variable {K : ClosedSubgroup G}theorem extensionQuotient_inductionOn
(L : GaloisSubextension K) {motive : L.extensionQuotient → Prop}
(q : L.extensionQuotient)
(mk : ∀ k : K.toSubgroup, motive (L.extensionQuotientMk k)) :
motive qUnramifiedness is the canonical inertia-containment condition.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace GaloisSubextension
variable {K : ClosedSubgroup G}theorem isUnramified_iff_inertia_le (L : GaloisSubextension K)
(D : DegreeData G) :
L.IsUnramified D ↔
K.toSubgroup ⊓ D.degree.toMonoidHom.ker ≤ L.field.toSubgroupTotal ramification is the canonical equality of degree images.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace GaloisSubextension
variable {K : ClosedSubgroup G}theorem isTotallyRamified_iff_image_le (L : GaloisSubextension K)
(D : DegreeData G) :
L.IsTotallyRamified D ↔
K.toSubgroup.map D.degree.toMonoidHom ≤
L.field.toSubgroup.map D.degree.toMonoidHomA finite abstract extension. Finiteness is carried by the extension object, so its public numerical invariants can be positive naturals rather than using the raw subgroup-index convention in which an infinite index is encoded as 0.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeDatastructure FiniteAbstractExtension (G : Type*) [Group G] [TopologicalSpace G]
extends AbstractExtension G where
/-- The relative quotient of the base subgroup by the extension subgroup is finite. -/
finiteQuotient :
Finite
(toAbstractExtension.base.toSubgroup ⧸
extensionSubgroup toAbstractExtension.base toAbstractExtension.field
toAbstractExtension.below)The subgroup of the base represented by a finite extension.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace FiniteAbstractExtension
variable (E : FiniteAbstractExtension G)def subgroup : Subgroup E.base.toSubgroupThe finite extension's actual relative coset space.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace FiniteAbstractExtension
variable (E : FiniteAbstractExtension G)def quotient : Type uBundle an inclusion once its actual relative coset type is known to be finite. This is the canonical boundary from subgroup data to the finite extension API; numerical invariants are obtained only from the resulting object.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace FiniteAbstractExtension
variable (E : FiniteAbstractExtension G)def ofInclusion (field base : ClosedSubgroup G)
(below : field.toSubgroup ≤ base.toSubgroup)
[hfinite : Finite
(base.toSubgroup ⧸ extensionSubgroup base field below)] :
FiniteAbstractExtension G where
field := field
base := base
below := below
finiteQuotient := hfiniteThe field endpoint of an extension bundled from an inclusion is the supplied field.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace FiniteAbstractExtension
variable (E : FiniteAbstractExtension G)theorem ofInclusion_field (field base : ClosedSubgroup G)
(below : field.toSubgroup ≤ base.toSubgroup)
[Finite (base.toSubgroup ⧸ extensionSubgroup base field below)] :
(ofInclusion field base below).field = fieldThe base endpoint of an extension bundled from an inclusion is the supplied base.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace FiniteAbstractExtension
variable (E : FiniteAbstractExtension G)theorem ofInclusion_base (field base : ClosedSubgroup G)
(below : field.toSubgroup ≤ base.toSubgroup)
[Finite (base.toSubgroup ⧸ extensionSubgroup base field below)] :
(ofInclusion field base below).base = baseThe unramified predicate for a finite extension is the predicate on its underlying abstract extension.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace FiniteAbstractExtension
variable (E : FiniteAbstractExtension G)def IsUnramified (D : DegreeData G) : PropThe totally ramified predicate for a finite extension is the predicate on its underlying abstract extension.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace FiniteAbstractExtension
variable (E : FiniteAbstractExtension G)def IsTotallyRamified (D : DegreeData G) : PropFinite-extension unramifiedness is exactly unramifiedness of the underlying abstract extension.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace FiniteAbstractExtension
variable (E : FiniteAbstractExtension G)theorem isUnramified_iff (D : DegreeData G) :
E.IsUnramified D ↔ E.toAbstractExtension.IsUnramified DFinite-extension total ramification is inherited from the underlying abstract extension.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace FiniteAbstractExtension
variable (E : FiniteAbstractExtension G)theorem isTotallyRamified_iff (D : DegreeData G) :
E.IsTotallyRamified D ↔ E.toAbstractExtension.IsTotallyRamified DFinite unramified extensions satisfy the same inertia-containment characterization as their underlying abstract extensions.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace FiniteAbstractExtension
variable (E : FiniteAbstractExtension G)theorem isUnramified_iff_inertia_le (D : DegreeData G) :
E.IsUnramified D ↔
E.base.toSubgroup ⊓ D.degree.toMonoidHom.ker ≤ E.field.toSubgroupFinite totally ramified extensions satisfy the same degree-image characterization as their underlying abstract extensions.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace FiniteAbstractExtension
variable (E : FiniteAbstractExtension G)theorem isTotallyRamified_iff_image_le (D : DegreeData G) :
E.IsTotallyRamified D ↔
E.base.toSubgroup.map D.degree.toMonoidHom ≤
E.field.toSubgroup.map D.degree.toMonoidHomThe coset space carried by a finite abstract extension is finite.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace FiniteAbstractExtension
variable (E : FiniteAbstractExtension G)instance quotientFinite :
Finite E.quotientThe finite instance in the concrete quotient presentation used by norm maps.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace FiniteAbstractExtension
variable (E : FiniteAbstractExtension G)instance representedQuotientFinite :
Finite
(E.base.toSubgroup ⧸
extensionSubgroup E.base E.field E.below)Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace FiniteAbstractExtension
variable (E : FiniteAbstractExtension G)theorem degreeCardinal_lt_aleph0 :
E.toAbstractExtension.degreeCardinal < Cardinal.aleph0Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace FiniteAbstractExtension
variable (E : FiniteAbstractExtension G)theorem relativeDegreeCardinals_lt_aleph0 (D : DegreeData G) :
Cardinal.lift.{u}
(E.toAbstractExtension.relativeResidueDegreeCardinal D) <
Cardinal.aleph0 ∧
E.toAbstractExtension.relativeRamificationIndexCardinal D <
Cardinal.aleph0Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace FiniteAbstractExtension
variable (E : FiniteAbstractExtension G)theorem relativeResidueDegreeCardinal_lt_aleph0
(D : DegreeData G) :
E.toAbstractExtension.relativeResidueDegreeCardinal D <
Cardinal.aleph0Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace FiniteAbstractExtension
variable (E : FiniteAbstractExtension G)theorem relativeRamificationIndexCardinal_lt_aleph0
(D : DegreeData G) :
E.toAbstractExtension.relativeRamificationIndexCardinal D <
Cardinal.aleph0The residue coset type of a finite extension is finite. This is derived from the cardinal fundamental identity, rather than from a natural-valued index whose infinite case would be represented by zero.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace FiniteAbstractExtension
variable (E : FiniteAbstractExtension G)instance residueQuotientFinite (D : DegreeData G) :
Finite
(↥(E.base.toSubgroup.map D.degree.toMonoidHom) ⧸
(E.field.toSubgroup.map D.degree.toMonoidHom).subgroupOf
(E.base.toSubgroup.map D.degree.toMonoidHom))The inertia coset type of a finite extension is finite. As for the residue quotient, this is a consequence of the cardinal fundamental identity.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace FiniteAbstractExtension
variable (E : FiniteAbstractExtension G)instance ramificationQuotientFinite (D : DegreeData G) :
Finite
(↥(E.base.toSubgroup ⊓ D.degree.toMonoidHom.ker) ⧸
(E.field.toSubgroup ⊓ D.degree.toMonoidHom.ker).subgroupOf
(E.base.toSubgroup ⊓ D.degree.toMonoidHom.ker))The positive degree of a finite abstract extension.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace FiniteAbstractExtension
variable (E : FiniteAbstractExtension G)def degree : ℕ+The positive relative residue degree of a finite abstract extension.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace FiniteAbstractExtension
variable (E : FiniteAbstractExtension G)def residueDegree (D : DegreeData G) : ℕ+The positive relative ramification index of a finite abstract extension.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace FiniteAbstractExtension
variable (E : FiniteAbstractExtension G)def ramificationIndex (D : DegreeData G) : ℕ+The natural value of the positive extension degree is the cardinality of its quotient.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace FiniteAbstractExtension
variable (E : FiniteAbstractExtension G)theorem degree_coe :
(E.degree : ℕ) = Nat.card E.quotientThe positive residue degree coerces to the cardinality of the mapped-subgroup quotient.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace FiniteAbstractExtension
variable (E : FiniteAbstractExtension G)theorem residueDegree_coe (D : DegreeData G) :
(E.residueDegree D : ℕ) =
Nat.card
(↥(E.base.toSubgroup.map D.degree.toMonoidHom) ⧸
(E.field.toSubgroup.map D.degree.toMonoidHom).subgroupOf
(E.base.toSubgroup.map D.degree.toMonoidHom))The positive ramification index coerces to the cardinality of the inertia quotient.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace FiniteAbstractExtension
variable (E : FiniteAbstractExtension G)theorem ramificationIndex_coe (D : DegreeData G) :
(E.ramificationIndex D : ℕ) =
Nat.card
(↥(E.base.toSubgroup ⊓ D.degree.toMonoidHom.ker) ⧸
(E.field.toSubgroup ⊓ D.degree.toMonoidHom.ker).subgroupOf
(E.base.toSubgroup ⊓ D.degree.toMonoidHom.ker))The underlying subgroup index of a finite extension is the natural coercion of its positive degree. This theorem is a finite-only bridge, not a general natural-valued degree definition.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace FiniteAbstractExtension
variable (E : FiniteAbstractExtension G)theorem relIndex_eq_degree :
E.field.toSubgroup.relIndex E.base.toSubgroup = (E.degree : ℕ)The index of the represented extension subgroup is the finite extension degree.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace FiniteAbstractExtension
variable (E : FiniteAbstractExtension G)theorem extensionSubgroup_index_eq_degree :
(extensionSubgroup E.base E.field E.below).index = (E.degree : ℕ)The relative index of the mapped field subgroups is the positive residue degree of a finite extension.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace FiniteAbstractExtension
variable (E : FiniteAbstractExtension G)theorem mapped_relIndex_eq_residueDegree (D : DegreeData G) :
(E.field.toSubgroup.map D.degree.toMonoidHom).relIndex
(E.base.toSubgroup.map D.degree.toMonoidHom) =
(E.residueDegree D : ℕ)The relative index inside the degree kernel is the positive ramification index of a finite extension.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace FiniteAbstractExtension
variable (E : FiniteAbstractExtension G)theorem inertia_relIndex_eq_ramificationIndex (D : DegreeData G) :
(E.field.toSubgroup ⊓ D.degree.toMonoidHom.ker).relIndex
(E.base.toSubgroup ⊓ D.degree.toMonoidHom.ker) =
(E.ramificationIndex D : ℕ)The finite fundamental identity, stated only in terms of the positive invariants carried by a finite extension object.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace FiniteAbstractExtension
variable (E : FiniteAbstractExtension G)theorem degree_eq_residueDegree_mul_ramificationIndex (D : DegreeData G) :
(E.degree : ℕ) =
(E.residueDegree D : ℕ) * (E.ramificationIndex D : ℕ)An unramified finite extension has ramification index one.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace FiniteAbstractExtension
variable (E : FiniteAbstractExtension G)theorem ramificationIndex_eq_one_of_isUnramified (D : DegreeData G)
(hE : E.IsUnramified D) :
(E.ramificationIndex D : ℕ) = 1A totally ramified finite extension has residue degree one.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace FiniteAbstractExtension
variable (E : FiniteAbstractExtension G)theorem residueDegree_eq_one_of_isTotallyRamified (D : DegreeData G)
(hE : E.IsTotallyRamified D) :
(E.residueDegree D : ℕ) = 1A finite extension has residue degree one exactly when it is totally ramified. This keeps callers on the structural predicate API instead of unfolding the image-index implementation.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace FiniteAbstractExtension
variable (E : FiniteAbstractExtension G)theorem isTotallyRamified_iff_residueDegree_eq_one (D : DegreeData G) :
E.IsTotallyRamified D ↔ (E.residueDegree D : ℕ) = 1Converse form convenient for constructing the structural predicate from the positive finite invariant.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace FiniteAbstractExtension
variable (E : FiniteAbstractExtension G)theorem isTotallyRamified_of_residueDegree_eq_one (D : DegreeData G)
(h : (E.residueDegree D : ℕ) = 1) : E.IsTotallyRamified DIn an unramified finite extension, residue degree equals extension degree.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace FiniteAbstractExtension
variable (E : FiniteAbstractExtension G)theorem residueDegree_eq_degree_of_isUnramified (D : DegreeData G)
(hE : E.IsUnramified D) :
(E.residueDegree D : ℕ) = (E.degree : ℕ)In a totally ramified finite extension, ramification index equals extension degree.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace FiniteAbstractExtension
variable (E : FiniteAbstractExtension G)theorem ramificationIndex_eq_degree_of_isTotallyRamified (D : DegreeData G)
(hE : E.IsTotallyRamified D) :
(E.ramificationIndex D : ℕ) = (E.degree : ℕ)For a finite extension, its cardinal-valued degree is the cardinal cast of its positive natural degree.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace FiniteAbstractExtension
variable (E : FiniteAbstractExtension G)theorem degreeCardinal_eq_coe :
E.toAbstractExtension.degreeCardinal =
((E.degree : ℕ) : Cardinal)For a finite extension, the cardinal-valued relative residue degree is the cardinal cast of the positive natural residue degree.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace FiniteAbstractExtension
variable (E : FiniteAbstractExtension G)theorem relativeResidueDegreeCardinal_eq_coe (D : DegreeData G) :
E.toAbstractExtension.relativeResidueDegreeCardinal D =
((E.residueDegree D : ℕ) : Cardinal)For a finite extension, the cardinal-valued relative ramification index is the cardinal cast of the positive natural ramification index.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace FiniteAbstractExtension
variable (E : FiniteAbstractExtension G)theorem relativeRamificationIndexCardinal_eq_coe (D : DegreeData G) :
E.toAbstractExtension.relativeRamificationIndexCardinal D =
((E.ramificationIndex D : ℕ) : Cardinal)A finite composable tower of abstract extensions. The two adjacent finite quotient proofs belong to the tower object, so downstream norm and degree laws do not thread subgroup containments and finiteness instances as independent arguments.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeDatastructure FiniteTower (G : Type*) [Group G] [TopologicalSpace G]
extends AbstractExtension.Tower G where
/-- The quotient for the top-to-middle extension is finite. -/
finiteTopQuotient : Finite toTower.topExtension.quotient
/-- The quotient for the middle-to-base extension is finite. -/
finiteBaseQuotient : Finite toTower.baseExtension.quotientThe upper relative quotient in a finite tower is finite.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace FiniteTower
variable (T : FiniteTower G)instance topQuotientFinite :
Finite (T.middle.toSubgroup ⧸
extensionSubgroup T.middle T.top T.top_le_middle)The lower relative quotient in a finite tower is finite.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace FiniteTower
variable (T : FiniteTower G)instance baseQuotientFinite :
Finite (T.base.toSubgroup ⧸
extensionSubgroup T.base T.middle T.middle_le_base)The upper finite extension represented by a finite tower.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace FiniteTower
variable (T : FiniteTower G)def topExtension : FiniteAbstractExtension G where
toAbstractExtension := T.toTower.topExtension
finiteQuotient := T.finiteTopQuotientThe lower finite extension represented by a finite tower.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace FiniteTower
variable (T : FiniteTower G)def baseExtension : FiniteAbstractExtension G where
toAbstractExtension := T.toTower.baseExtension
finiteQuotient := T.finiteBaseQuotientIf the relative residue quotient over a field with finite absolute residue quotient is finite, then the upper field also has finite absolute residue quotient. This is the minimal honest boundary constructor: it uses the actual quotient types and the cardinal tower identity.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace FiniteResidueAbstractField
variable {D : DegreeData G}def ofRelativeInclusion (D : DegreeData G)
(field : ClosedSubgroup G) (base : FiniteResidueAbstractField D)
(below : field.toSubgroup ≤ base.field.toSubgroup)
[finiteRelativeResidueQuotient : Finite
(↥(base.field.toSubgroup.map D.degree.toMonoidHom) ⧸
(field.toSubgroup.map D.degree.toMonoidHom).subgroupOf
(base.field.toSubgroup.map D.degree.toMonoidHom))] :
FiniteResidueAbstractField D where
field := field
finiteResidueQuotient := by
apply Cardinal.lt_aleph0_iff_finite.mp
rw [← D.residueDegreeCardinal_eq_mk_residueQuotient]
let E : AbstractExtension G := {
field := field
base := base.field
below := below
}
rw [← E.relativeResidueDegreeCardinal_mul_residueDegreeCardinal D]
apply Cardinal.mul_lt_aleph0_iff.mpr
exact Or.inr (Or.inr ⟨by
change Cardinal.mk
(↥(base.field.toSubgroup.map D.degree.toMonoidHom) ⧸
(field.toSubgroup.map D.degree.toMonoidHom).subgroupOf
(base.field.toSubgroup.map D.degree.toMonoidHom)) <
Cardinal.aleph0
exact Cardinal.lt_aleph0_of_finite _, by
rw [D.residueDegreeCardinal_eq_mk_residueQuotient]
exact Cardinal.lt_aleph0_of_finite _⟩)A finite extension whose base and field both carry their honest finite absolute residue quotients. The proof-dependent relative quotient is stored once in the object and exposed through toFiniteAbstractExtension.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeDatastructure FiniteResidueAbstractExtension (D : DegreeData G) where
/-- The top endpoint with its finite residue quotient. -/
field : FiniteResidueAbstractField D
/-- The base endpoint with its finite residue quotient. -/
base : FiniteResidueAbstractField D
/-- The top-field subgroup is contained in the base-field subgroup. -/
below : field.field.toSubgroup ≤ base.field.toSubgroup
/-- The relative extension quotient is finite. -/
finiteQuotient :
Finite
(base.field.toSubgroup ⧸
extensionSubgroup base.field field.field below)Enrich a finite extension of a field with finite absolute residue quotient with the corresponding honest residue data on its upper endpoint. Finiteness of the upper absolute residue quotient is deduced from the cardinal-valued tower identity, which is the source of truth for arbitrary-index data.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace FiniteResidueAbstractExtension
variable {D : DegreeData G}def ofInclusion (D : DegreeData G)
(field : ClosedSubgroup G) (base : FiniteResidueAbstractField D)
(below : field.toSubgroup ≤ base.field.toSubgroup)
[finiteQuotient : Finite
(base.field.toSubgroup ⧸
extensionSubgroup base.field field below)] :
FiniteResidueAbstractExtension D where
field := {
field := field
finiteResidueQuotient := by
apply Cardinal.lt_aleph0_iff_finite.mp
rw [← D.residueDegreeCardinal_eq_mk_residueQuotient]
let E : FiniteAbstractExtension G := {
field := field
base := base.field
below := below
finiteQuotient := finiteQuotient
}
rw [← E.toAbstractExtension.relativeResidueDegreeCardinal_mul_residueDegreeCardinal D]
apply Cardinal.mul_lt_aleph0_iff.mpr
exact Or.inr (Or.inr ⟨E.relativeResidueDegreeCardinal_lt_aleph0 D, by
rw [D.residueDegreeCardinal_eq_mk_residueQuotient]
exact Cardinal.lt_aleph0_of_finite (D.residueQuotient base.field)⟩) }
base := base
below := below
finiteQuotient := finiteQuotientForget only the endpoint residue-finiteness data.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace FiniteResidueAbstractExtension
variable {D : DegreeData G}def toFiniteAbstractExtension (E : FiniteResidueAbstractExtension D) :
FiniteAbstractExtension G where
field := E.field.field
base := E.base.field
below := E.below
finiteQuotient := E.finiteQuotientA finite-residue extension supplies finiteness of its represented relative quotient.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace FiniteResidueAbstractExtension
variable {D : DegreeData G}instance (E : FiniteResidueAbstractExtension D) :
Finite
(E.base.field.toSubgroup ⧸
extensionSubgroup E.base.field E.field.field E.below)The positive relative degree.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace FiniteResidueAbstractExtension
variable {D : DegreeData G}def degree (E : FiniteResidueAbstractExtension D) : ℕ+The positive relative residue degree.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace FiniteResidueAbstractExtension
variable {D : DegreeData G}def residueDegree (E : FiniteResidueAbstractExtension D) : ℕ+The positive relative ramification index.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace FiniteResidueAbstractExtension
variable {D : DegreeData G}def ramificationIndex
(E : FiniteResidueAbstractExtension D) : ℕ+The residue-enriched extension degree agrees with the underlying finite-extension degree.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace FiniteResidueAbstractExtension
variable {D : DegreeData G}theorem degree_coe (E : FiniteResidueAbstractExtension D) :
(E.degree : ℕ) = (E.toFiniteAbstractExtension.degree : ℕ)The residue-enriched residue degree agrees with the underlying finite-extension invariant.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace FiniteResidueAbstractExtension
variable {D : DegreeData G}theorem residueDegree_coe (E : FiniteResidueAbstractExtension D) :
(E.residueDegree : ℕ) =
(E.toFiniteAbstractExtension.residueDegree D : ℕ)The residue-enriched ramification index agrees with the underlying finite-extension invariant.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace FiniteResidueAbstractExtension
variable {D : DegreeData G}theorem ramificationIndex_coe
(E : FiniteResidueAbstractExtension D) :
(E.ramificationIndex : ℕ) =
(E.toFiniteAbstractExtension.ramificationIndex D : ℕ)An abstract field finite over the distinguished base field.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]structure FiniteAbstractField (G : Type u) [Group G] [TopologicalSpace G] where
/-- The closed subgroup representing the abstract field. -/
field : ClosedSubgroup G
/-- The field has finite degree over the distinguished base. -/
finite : Finite ((baseField G).toSubgroup ⧸
extensionSubgroup (baseField G) field (le_baseField field))A finite abstract field is determined by its underlying closed subgroup; the finiteness component is proof-irrelevant.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace FiniteAbstractFieldtheorem eq_of_field_eq (K L : FiniteAbstractField G)
(h : K.field = L.field) : K = LThe distinguished base field, bundled with its trivial finite quotient.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace FiniteAbstractFielddef base (G : Type u) [Group G] [TopologicalSpace G] :
FiniteAbstractField G where
field := baseField G
finite := by
let : (extensionSubgroup (baseField G) (baseField G)
(le_baseField (baseField G))).Normal := by
rw [show extensionSubgroup (baseField G) (baseField G)
(le_baseField (baseField G)) = ⊤ by
ext x
exact Iff.rfl]
infer_instance
let : Subsingleton
((baseField G).toSubgroup ⧸
extensionSubgroup (baseField G) (baseField G)
(le_baseField (baseField G))) := by
constructor
intro x y
refine Quotient.inductionOn₂' x y ?_
intro a b
apply QuotientGroup.eq_iff_div_mem.mpr
exact Subgroup.mem_top _
infer_instanceRegard a finite abstract field as its finite extension of the distinguished base field.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace FiniteAbstractFielddef toFiniteAbstractExtension (K : FiniteAbstractField G) :
DegreeData.FiniteAbstractExtension G where
field := K.field
base := baseField G
below := le_baseField K.field
finiteQuotient := K.finiteA finite abstract field supplies finiteness of its quotient over the distinguished base.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace FiniteAbstractFieldinstance (K : FiniteAbstractField G) :
Finite ((baseField G).toSubgroup ⧸
extensionSubgroup (baseField G) K.field (le_baseField K.field))A finite field over the distinguished base has a finite absolute residue quotient. This is derived from the finite relative quotient and the surjectivity of the ambient degree map.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace FiniteAbstractFielddef toFiniteResidueAbstractField
(K : FiniteAbstractField G) (D : DegreeData G) :
DegreeData.FiniteResidueAbstractField D where
field := K.field
finiteResidueQuotient := by
apply Cardinal.lt_aleph0_iff_finite.mp
change
intersectionIndexCardinal (D.fieldImage K.field)
(⊤ : Subgroup ZHatMul) < Cardinal.aleph0
rw [D.fieldImage_eq_map]
have htop :
(baseField G).toSubgroup.map D.degree.toMonoidHom = ⊤ := by
rw [baseField_toSubgroup]
exact Subgroup.map_top_of_surjective _ D.degree_surjective
rw [← htop]
simpa only [FiniteAbstractField.toFiniteAbstractExtension,
DegreeData.AbstractExtension.relativeResidueDegreeCardinal, relativeIndexCardinal] using
K.toFiniteAbstractExtension.relativeResidueDegreeCardinal_lt_aleph0 DThe positive absolute residue degree of a field finite over the distinguished base.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace FiniteAbstractFielddef residueDegree (K : FiniteAbstractField G)
(D : DegreeData G) : ℕ+Positive-natural specialization of the base-field residue degree.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace FiniteAbstractFieldtheorem base_residueDegree (D : DegreeData G) :
(FiniteAbstractField.base G).residueDegree D = 1The field residue degree is inherited from its finite-residue-field enrichment.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace FiniteAbstractFieldtheorem residueDegree_coe (K : FiniteAbstractField G)
(D : DegreeData G) :
(K.residueDegree D : ℕ) =
((K.toFiniteResidueAbstractField D).residueDegree : ℕ)A finite extension between two fields that are themselves finite over the distinguished base. Both endpoint finiteness proofs and the relative quotient belong to the object.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]structure FiniteAbstractFieldExtension (G : Type u)
[Group G] [TopologicalSpace G] where
/-- The top endpoint, finite over the distinguished base. -/
field : FiniteAbstractField G
/-- The base endpoint, finite over the distinguished base. -/
base : FiniteAbstractField G
/-- The top-field subgroup is contained in the base-field subgroup. -/
below : field.field.toSubgroup ≤ base.field.toSubgroup
/-- The relative extension quotient is finite. -/
finiteQuotient :
Finite
(base.field.toSubgroup ⧸
extensionSubgroup base.field field.field below)Canonically bundle a finite relative extension of a field already finite over the distinguished base. Finiteness of the upper field follows from the actual quotient tower.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace FiniteAbstractFieldExtensiondef ofInclusion (field : ClosedSubgroup G)
(base : FiniteAbstractField G)
(below : field.toSubgroup ≤ base.field.toSubgroup)
[finiteQuotient : Finite
(base.field.toSubgroup ⧸
extensionSubgroup base.field field below)] :
FiniteAbstractFieldExtension G where
field := {
field := field
finite := by
apply Cardinal.lt_aleph0_iff_finite.mp
let T : DegreeData.AbstractExtension.Tower G := {
top := field
middle := base.field
base := baseField G
top_le_middle := below
middle_le_base := le_baseField base.field }
change T.totalExtension.degreeCardinal < Cardinal.aleph0
rw [← T.degreeCardinal_mul]
apply Cardinal.mul_lt_aleph0
· change Cardinal.mk
(base.field.toSubgroup ⧸
extensionSubgroup base.field field below) < Cardinal.aleph0
exact Cardinal.lt_aleph0_of_finite _
· change Cardinal.mk
((baseField G).toSubgroup ⧸
extensionSubgroup (baseField G) base.field
(le_baseField base.field)) < Cardinal.aleph0
exact Cardinal.lt_aleph0_of_finite _ }
base := base
below := below
finiteQuotient := finiteQuotientForget endpoint finiteness over the distinguished base.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace FiniteAbstractFieldExtensiondef toFiniteAbstractExtension (E : FiniteAbstractFieldExtension G) :
DegreeData.FiniteAbstractExtension G where
field := E.field.field
base := E.base.field
below := E.below
finiteQuotient := E.finiteQuotientStructural unramifiedness of the represented relative extension.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace FiniteAbstractFieldExtensiondef IsUnramified (E : FiniteAbstractFieldExtension G) (D : DegreeData G) : PropStructural total ramification of the represented relative extension.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace FiniteAbstractFieldExtensiondef IsTotallyRamified (E : FiniteAbstractFieldExtension G)
(D : DegreeData G) : PropThe positive relative degree.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace FiniteAbstractFieldExtensiondef degree (E : FiniteAbstractFieldExtension G) : ℕ+The positive relative residue degree.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace FiniteAbstractFieldExtensiondef residueDegree (E : FiniteAbstractFieldExtension G)
(D : DegreeData G) : ℕ+The positive relative ramification index.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace FiniteAbstractFieldExtensiondef ramificationIndex (E : FiniteAbstractFieldExtension G)
(D : DegreeData G) : ℕ+In an unramified finite field extension, the positive relative residue degree is the positive extension degree.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace FiniteAbstractFieldExtensiontheorem residueDegree_eq_degree_of_isUnramified
(E : FiniteAbstractFieldExtension G) (D : DegreeData G)
(hE : E.IsUnramified D) :
(E.residueDegree D : ℕ) = (E.degree : ℕ)A finite abstract field extension supplies finiteness of its relative quotient.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace FiniteAbstractFieldExtensioninstance (E : FiniteAbstractFieldExtension G) :
Finite
(E.base.field.toSubgroup ⧸
extensionSubgroup E.base.field E.field.field E.below)Canonically enrich both endpoints with their finite residue quotients.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open CyclicCohomology
noncomputable section
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace FiniteAbstractFieldExtensiondef toFiniteResidueAbstractExtension
(E : FiniteAbstractFieldExtension G) (D : DegreeData G) :
DegreeData.FiniteResidueAbstractExtension D where
field := E.field.toFiniteResidueAbstractField D
base := E.base.toFiniteResidueAbstractField D
below := E.below
finiteQuotient := E.finiteQuotient