Images and finite-index overlattices of additive-group maps

This file models an image by the canonical AddMonoidHom.range, records the finite-index-overlattice predicate for two additive subgroups, and factors family values through chosen image inclusions. The terminology is motivated by relative numerical K-theory, but the public API uses only additive groups and homomorphisms; geometric base-change maps are consumers of this root.

Images and finite-index overlattices

@[reducible, inline]

abbrev DerivedAlgGeo.Algebra.RelativeNumerical.EtaImage {A : Type u_1} {V : Type u_3} [AddCommGroup A] [AddCommGroup V] (eta : A →+ V) : AddSubgroup V

The image group determined by an additive map η.

This is an abbreviation for the existing additive-subgroup range, so all subgroup, quotient, and finite-index API remains available without a parallel lattice hierarchy.

Equations

• DerivedAlgGeo.Algebra.RelativeNumerical.EtaImage eta = eta.range

def DerivedAlgGeo.Algebra.RelativeNumerical.etaClass {A : Type u_1} {V : Type u_3} [AddCommGroup A] [AddCommGroup V] (eta : A →+ V) : A →+ ↥(EtaImage eta)

A numerical class regarded as an element of the image of ηᵛ.

Equations

• DerivedAlgGeo.Algebra.RelativeNumerical.etaClass eta = eta.rangeRestrict

@[simp]

theorem DerivedAlgGeo.Algebra.RelativeNumerical.etaClass_coe {A : Type u_1} {V : Type u_3} [AddCommGroup A] [AddCommGroup V] (eta : A →+ V) (x : A) : ↑((etaClass eta) x) = eta x

def DerivedAlgGeo.Algebra.RelativeNumerical.IsFiniteIndexOverlattice {V : Type u_3} [AddCommGroup V] (base larger : AddSubgroup V) : Prop

larger is a finite-index overlattice of base inside their common ambient additive group. Containment and finite relative index are properties, not fields on a new carrier.

Equations

• DerivedAlgGeo.Algebra.RelativeNumerical.IsFiniteIndexOverlattice base larger = (base ≤ larger ∧ base.IsFiniteRelIndex larger)

def DerivedAlgGeo.Algebra.RelativeNumerical.specializationMap {A : Type u_1} {B : Type u_2} {V : Type u_3} [AddCommGroup A] [AddCommGroup B] [AddCommGroup V] (eta : A →+ V) (geometricEta : B →+ V) (h : eta.range ≤ geometricEta.range) : A →+ ↥(EtaImage geometricEta)

Transport a class through an additive map whose range lies in a chosen second range.

Equations

• DerivedAlgGeo.Algebra.RelativeNumerical.specializationMap eta geometricEta h = eta.codRestrict geometricEta.range ⋯

@[simp]

theorem DerivedAlgGeo.Algebra.RelativeNumerical.specializationMap_coe {A : Type u_1} {B : Type u_2} {V : Type u_3} [AddCommGroup A] [AddCommGroup B] [AddCommGroup V] (eta : A →+ V) (geometricEta : B →+ V) (h : eta.range ≤ geometricEta.range) (x : A) : ↑((specializationMap eta geometricEta h) x) = eta x

theorem DerivedAlgGeo.Algebra.RelativeNumerical.specializationMap_self {A : Type u_1} {V : Type u_3} [AddCommGroup A] [AddCommGroup V] (eta : A →+ V) : specializationMap eta eta ⋯ = etaClass eta

Admissible families

def DerivedAlgGeo.Algebra.RelativeNumerical.FamilyRelationSystem.ofEta {I : Type u} {K V₀ : I → Type v} [(i : I) → AddCommGroup (K i)] [(i : I) → AddCommGroup (V₀ i)] (geometricEta : (i : I) → K i →+ V₀ i) (Family : Type w) (Point : Family → Type w) (index : (F : Family) → Point F → I) (Source : (F : Family) → Point F → Type v) [(F : Family) → (t : Point F) → AddCommGroup (Source F t)] (eta : (F : Family) → (t : Point F) → Source F t →+ V₀ (index F t)) (hEta : ∀ (F : Family) (t : Point F), (eta F t).range ≤ (geometricEta (index F t)).range) (classValue : (F : Family) → (t : Point F) → Source F t) : FamilyRelationSystem fun (i : I) => ↥(EtaImage (geometricEta i))

Construct a family relation system from indexed additive maps.

For each index i, geometricEta i presents the target group as an image in V₀ i. At a point t of an admissible family, eta F t maps a source into the same ambient group; hEta is precisely its factorization through the chosen image. The resulting system is consumed by the saturated quotient in Basic. Geometric applications may instantiate these parameters with base-change maps, but no geometric vocabulary occurs in this root.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem DerivedAlgGeo.Algebra.RelativeNumerical.FamilyRelationSystem.ofEta_classValue_coe {I : Type u} {K V₀ : I → Type v} [(i : I) → AddCommGroup (K i)] [(i : I) → AddCommGroup (V₀ i)] (geometricEta : (i : I) → K i →+ V₀ i) (Family : Type w) (Point : Family → Type w) (index : (F : Family) → Point F → I) (Source : (F : Family) → Point F → Type v) [(F : Family) → (t : Point F) → AddCommGroup (Source F t)] (eta : (F : Family) → (t : Point F) → Source F t →+ V₀ (index F t)) (hEta : ∀ (F : Family) (t : Point F), (eta F t).range ≤ (geometricEta (index F t)).range) (classValue : (F : Family) → (t : Point F) → Source F t) (F : Family) (t : Point F) : ↑((ofEta geometricEta Family Point index Source eta hEta classValue).classValue F t) = (eta F t) (classValue F t)

Boundary tests

def DerivedAlgGeo.Algebra.RelativeNumerical.etaImageIdEquiv (A : Type u_4) [AddCommGroup A] : ↥(EtaImage (AddMonoidHom.id A)) ≃+ A

For the identity base-change map, the image construction recovers the original additive group.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem DerivedAlgGeo.Algebra.RelativeNumerical.etaImageIdEquiv_etaClass (A : Type u_4) [AddCommGroup A] (x : A) : (etaImageIdEquiv A) ((etaClass (AddMonoidHom.id A)) x) = x