Relative numerical quotients of families of additive groups

Given a family of additive commutative groups, this file forms their direct sum and quotients by the saturation of a supplied relation set. It also packages relation sets generated by values of an arbitrary family at pairs of points. Every declaration is algebraic: a geometric application must supply its fibre groups, admissible families, and specialization classes separately.

@[reducible, inline]

abbrev DerivedAlgGeo.Algebra.RelativeNumerical.FiberSum {I : Type u} (K : I → Type v) [(i : I) → AddCommGroup (K i)] : Type (max v u)

The direct sum of the numerical groups attached to the fibres.

Equations

• DerivedAlgGeo.Algebra.RelativeNumerical.FiberSum K = DirectSum I fun (i : I) => K i

noncomputable def DerivedAlgGeo.Algebra.RelativeNumerical.fiberInclusion {I : Type u} (K : I → Type v) [(i : I) → AddCommGroup (K i)] (i : I) : K i →+ FiberSum K

The canonical inclusion of one fibre group into the direct sum. The classical choice of decidable equality on the index type is confined here.

Equations

• DerivedAlgGeo.Algebra.RelativeNumerical.fiberInclusion K i = DirectSum.of K i

noncomputable def DerivedAlgGeo.Algebra.RelativeNumerical.fiberwiseHom {I : Type u} (K : I → Type v) [(i : I) → AddCommGroup (K i)] {B : Type u_1} [AddCommGroup B] (f : (i : I) → K i →+ B) : FiberSum K →+ B

The homomorphism from the fibre sum induced by a family of homomorphisms.

Equations

• DerivedAlgGeo.Algebra.RelativeNumerical.fiberwiseHom K f = DirectSum.toAddMonoid f

@[simp]

theorem DerivedAlgGeo.Algebra.RelativeNumerical.fiberwiseHom_fiberInclusion {I : Type u} (K : I → Type v) [(i : I) → AddCommGroup (K i)] {B : Type u_1} [AddCommGroup B] (f : (i : I) → K i →+ B) (i : I) (x : K i) : (fiberwiseHom K f) ((fiberInclusion K i) x) = (f i) x

def DerivedAlgGeo.Algebra.RelativeNumerical.relationSubgroup {I : Type u} (K : I → Type v) [(i : I) → AddCommGroup (K i)] (relations : Set (FiberSum K)) : AddSubgroup (FiberSum K)

The subgroup generated by the supplied family relations.

Equations

• DerivedAlgGeo.Algebra.RelativeNumerical.relationSubgroup K relations = AddSubgroup.closure relations

@[reducible, inline]

abbrev DerivedAlgGeo.Algebra.RelativeNumerical.Group {I : Type u} (K : I → Type v) [(i : I) → AddCommGroup (K i)] (relations : Set (FiberSum K)) : Type (max u v)

The saturated quotient determined by a collection of family relations.

Equations

• DerivedAlgGeo.Algebra.RelativeNumerical.Group K relations = (DerivedAlgGeo.Algebra.RelativeNumerical.relationSubgroup K relations).SaturatedQuotient

noncomputable def DerivedAlgGeo.Algebra.RelativeNumerical.of {I : Type u} (K : I → Type v) [(i : I) → AddCommGroup (K i)] (relations : Set (FiberSum K)) (i : I) : K i →+ Group K relations

The class of an element of one fibre group in the relative quotient.

Equations

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

theorem DerivedAlgGeo.Algebra.RelativeNumerical.of_apply {I : Type u} (K : I → Type v) [(i : I) → AddCommGroup (K i)] (relations : Set (FiberSum K)) (i : I) (x : K i) : (of K relations i) x = (relationSubgroup K relations).saturatedQuotientMk ((fiberInclusion K i) x)

@[simp]

theorem DerivedAlgGeo.Algebra.RelativeNumerical.relation_eq_zero {I : Type u} (K : I → Type v) [(i : I) → AddCommGroup (K i)] (relations : Set (FiberSum K)) {r : FiberSum K} (hr : r ∈ relations) : (relationSubgroup K relations).saturatedQuotientMk r = 0

Every specified family relation vanishes in the quotient.

theorem DerivedAlgGeo.Algebra.RelativeNumerical.of_eq_of {I : Type u} (K : I → Type v) [(i : I) → AddCommGroup (K i)] (relations : Set (FiberSum K)) {i j : I} {x : K i} {y : K j} (h : (fiberInclusion K i) x - (fiberInclusion K j) y ∈ relations) : (of K relations i) x = (of K relations j) y

Two indexed classes agree when their difference is one of the specified family relations.

noncomputable def DerivedAlgGeo.Algebra.RelativeNumerical.lift {I : Type u} (K : I → Type v) [(i : I) → AddCommGroup (K i)] {B : Type u_1} [AddCommGroup B] [IsAddTorsionFree B] (relations : Set (FiberSum K)) (f : (i : I) → K i →+ B) (hrelations : ∀ r ∈ relations, (fiberwiseHom K f) r = 0) : Group K relations →+ B

A family of maps to a torsion-free group descends when it kills every family relation.

Equations

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

@[simp]

theorem DerivedAlgGeo.Algebra.RelativeNumerical.lift_of {I : Type u} (K : I → Type v) [(i : I) → AddCommGroup (K i)] {B : Type u_1} [AddCommGroup B] [IsAddTorsionFree B] (relations : Set (FiberSum K)) (f : (i : I) → K i →+ B) (hrelations : ∀ r ∈ relations, (fiberwiseHom K f) r = 0) (i : I) (x : K i) : (lift K relations f hrelations) ((of K relations i) x) = (f i) x

def DerivedAlgGeo.Algebra.RelativeNumerical.map {I : Type u} (K : I → Type v) [(i : I) → AddCommGroup (K i)] {J : Type u_1} (L : J → Type u_2) [(j : J) → AddCommGroup (L j)] (sourceRelations : Set (FiberSum K)) (targetRelations : Set (FiberSum L)) (f : FiberSum K →+ FiberSum L) (hf : relationSubgroup K sourceRelations ≤ AddSubgroup.comap f (relationSubgroup L targetRelations)) : Group K sourceRelations →+ Group L targetRelations

A homomorphism of fibre sums which carries the generated relation subgroup into another induces a homomorphism of relative quotients.

Equations

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

@[simp]

theorem DerivedAlgGeo.Algebra.RelativeNumerical.map_mk {I : Type u} (K : I → Type v) [(i : I) → AddCommGroup (K i)] {J : Type u_1} (L : J → Type u_2) [(j : J) → AddCommGroup (L j)] (sourceRelations : Set (FiberSum K)) (targetRelations : Set (FiberSum L)) (f : FiberSum K →+ FiberSum L) (hf : relationSubgroup K sourceRelations ≤ AddSubgroup.comap f (relationSubgroup L targetRelations)) (x : FiberSum K) : (map K L sourceRelations targetRelations f hf) ((relationSubgroup K sourceRelations).saturatedQuotientMk x) = (relationSubgroup L targetRelations).saturatedQuotientMk (f x)

def DerivedAlgGeo.Algebra.RelativeNumerical.mapOfRelations {I : Type u} (K : I → Type v) [(i : I) → AddCommGroup (K i)] {J : Type u_1} (L : J → Type u_2) [(j : J) → AddCommGroup (L j)] (sourceRelations : Set (FiberSum K)) (targetRelations : Set (FiberSum L)) (f : FiberSum K →+ FiberSum L) (hf : ∀ r ∈ sourceRelations, f r ∈ relationSubgroup L targetRelations) : Group K sourceRelations →+ Group L targetRelations

It is enough to check preservation on the specified generating relations.

Equations

• DerivedAlgGeo.Algebra.RelativeNumerical.mapOfRelations K L sourceRelations targetRelations f hf = DerivedAlgGeo.Algebra.RelativeNumerical.map K L sourceRelations targetRelations f ⋯

@[simp]

theorem DerivedAlgGeo.Algebra.RelativeNumerical.map_id {I : Type u} (K : I → Type v) [(i : I) → AddCommGroup (K i)] (relations : Set (FiberSum K)) : map K K relations relations (AddMonoidHom.id (FiberSum K)) ⋯ = AddMonoidHom.id (Group K relations)

theorem DerivedAlgGeo.Algebra.RelativeNumerical.map_comp {I : Type u} (K : I → Type v) [(i : I) → AddCommGroup (K i)] {J : Type u_1} {M : Type u_2} (L : J → Type u_3) (N : M → Type u_4) [(j : J) → AddCommGroup (L j)] [(m : M) → AddCommGroup (N m)] (sourceRelations : Set (FiberSum K)) (middleRelations : Set (FiberSum L)) (targetRelations : Set (FiberSum N)) (f : FiberSum K →+ FiberSum L) (g : FiberSum L →+ FiberSum N) (hf : relationSubgroup K sourceRelations ≤ AddSubgroup.comap f (relationSubgroup L middleRelations)) (hg : relationSubgroup L middleRelations ≤ AddSubgroup.comap g (relationSubgroup N targetRelations)) : (map L N middleRelations targetRelations g hg).comp (map K L sourceRelations middleRelations f hf) = map K N sourceRelations targetRelations (g.comp f) ⋯

Induced relative-quotient maps preserve composition.

theorem DerivedAlgGeo.Algebra.RelativeNumerical.hom_ext {I : Type u} (K : I → Type v) [(i : I) → AddCommGroup (K i)] {B : Type u_1} [AddCommGroup B] (relations : Set (FiberSum K)) {f g : Group K relations →+ B} (h : ∀ (i : I), f.comp (of K relations i) = g.comp (of K relations i)) : f = g

Maps out of the relative quotient are determined by their values on every fibre group.

theorem DerivedAlgGeo.Algebra.RelativeNumerical.hom_ext_iff {I : Type u} {K : I → Type v} [(i : I) → AddCommGroup (K i)] {B : Type u_1} [AddCommGroup B] {relations : Set (FiberSum K)} {f g : Group K relations →+ B} : f = g ↔ ∀ (i : I), f.comp (of K relations i) = g.comp (of K relations i)

Relations generated by admissible families

structure DerivedAlgGeo.Algebra.RelativeNumerical.FamilyRelationSystem {I : Type u} (K : I → Type v) : Type (max (max u v) (w + 1))

The statement-layer data from which connected-family relations are made.

Family is intended to contain only the admissible families for an application. Consequently, application-specific admissibility conditions do not appear as inert fields here: a consumer proves them when it constructs an inhabitant of Family.

The value classValue F t is the class of the fibre at t, already transported to the numerical group indexed by index F t. Thus the same root also applies to other comparison problems whose families and point types are unrelated to any particular geometric objects.

• Family : Type w

  Admissible families whose point classes must agree.

• Point : self.Family → Type w

  The points at which an admissible family can be restricted.

• index (F : self.Family) : self.Point F → I

  The base fibre containing a point of a family.

• classValue (F : self.Family) (t : self.Point F) : K (self.index F t)

  The transported numerical class of the family at a point.

noncomputable def DerivedAlgGeo.Algebra.RelativeNumerical.FamilyRelationSystem.relation {I : Type u} (K : I → Type v) [(i : I) → AddCommGroup (K i)] (D : FamilyRelationSystem K) (F : D.Family) (t₁ t₂ : D.Point F) : FiberSum K

The difference of the two transported classes of one admissible family.

Equations

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

def DerivedAlgGeo.Algebra.RelativeNumerical.FamilyRelationSystem.relations {I : Type u} (K : I → Type v) [(i : I) → AddCommGroup (K i)] (D : FamilyRelationSystem K) : Set (FiberSum K)

All relations generated by pairs of points in one admissible family.

Equations

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

@[simp]

theorem DerivedAlgGeo.Algebra.RelativeNumerical.FamilyRelationSystem.relation_mem {I : Type u} (K : I → Type v) [(i : I) → AddCommGroup (K i)] (D : FamilyRelationSystem K) (F : D.Family) (t₁ t₂ : D.Point F) : relation K D F t₁ t₂ ∈ relations K D

@[reducible, inline]

abbrev DerivedAlgGeo.Algebra.RelativeNumerical.FamilyRelationSystem.RelativeGroup {I : Type u} (K : I → Type v) [(i : I) → AddCommGroup (K i)] (D : FamilyRelationSystem K) : Type (max u v)

The relative saturated quotient generated by the admissible families.

Equations

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

noncomputable def DerivedAlgGeo.Algebra.RelativeNumerical.FamilyRelationSystem.pointClass {I : Type u} (K : I → Type v) [(i : I) → AddCommGroup (K i)] (D : FamilyRelationSystem K) (F : D.Family) (t : D.Point F) : RelativeGroup K D

The class of one point of an admissible family in the relative group.

Equations

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

theorem DerivedAlgGeo.Algebra.RelativeNumerical.FamilyRelationSystem.pointClass_eq {I : Type u} (K : I → Type v) [(i : I) → AddCommGroup (K i)] (D : FamilyRelationSystem K) (F : D.Family) (t₁ t₂ : D.Point F) : pointClass K D F t₁ = pointClass K D F t₂

The class of an admissible family is independent of the chosen point.

noncomputable def DerivedAlgGeo.Algebra.RelativeNumerical.FamilyRelationSystem.lift {I : Type u} (K : I → Type v) [(i : I) → AddCommGroup (K i)] (D : FamilyRelationSystem K) {B : Type u_1} [AddCommGroup B] [IsAddTorsionFree B] (f : (i : I) → K i →+ B) (hfamily : ∀ (F : D.Family) (t₁ t₂ : D.Point F), (f (D.index F t₁)) (D.classValue F t₁) = (f (D.index F t₂)) (D.classValue F t₂)) : RelativeGroup K D →+ B

Fibrewise maps that are constant on every admissible family descend to the family-generated relative group.

Equations

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

@[simp]

theorem DerivedAlgGeo.Algebra.RelativeNumerical.FamilyRelationSystem.lift_pointClass {I : Type u} (K : I → Type v) [(i : I) → AddCommGroup (K i)] (D : FamilyRelationSystem K) {B : Type u_1} [AddCommGroup B] [IsAddTorsionFree B] (f : (i : I) → K i →+ B) (hfamily : ∀ (F : D.Family) (t₁ t₂ : D.Point F), (f (D.index F t₁)) (D.classValue F t₁) = (f (D.index F t₂)) (D.classValue F t₂)) (F : D.Family) (t : D.Point F) : (lift K D f hfamily) (pointClass K D F t) = (f (D.index F t)) (D.classValue F t)

noncomputable def DerivedAlgGeo.Algebra.RelativeNumerical.singletonFold (A : Type u_1) [AddCommGroup A] [IsAddTorsionFree A] : Group (fun (x : PUnit.{u_2 + 1}) => A) ∅ →+ A

For a one-point base, the relative quotient with no relations maps back to the unique fibre group.

Equations

• DerivedAlgGeo.Algebra.RelativeNumerical.singletonFold A = DerivedAlgGeo.Algebra.RelativeNumerical.lift (fun (x : PUnit.{?u.1 + 1}) => A) ∅ (fun (x : PUnit.{?u.1 + 1}) => AddMonoidHom.id A) ⋯

@[simp]

theorem DerivedAlgGeo.Algebra.RelativeNumerical.singletonFold_of (A : Type u_1) [AddCommGroup A] [IsAddTorsionFree A] (x : A) : (singletonFold A) ((of (fun (x : PUnit.{u_2 + 1}) => A) ∅ PUnit.unit) x) = x

noncomputable def DerivedAlgGeo.Algebra.RelativeNumerical.singletonEquiv (A : Type u_1) [AddCommGroup A] [IsAddTorsionFree A] : Group (fun (x : PUnit.{u_2 + 1}) => A) ∅ ≃+ A

The relative construction over one point, with no family relations, agrees with its unique torsion-free indexed group.

Equations

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

@[simp]

theorem DerivedAlgGeo.Algebra.RelativeNumerical.singletonEquiv_of (A : Type u_1) [AddCommGroup A] [IsAddTorsionFree A] (x : A) : (singletonEquiv A) ((of (fun (x : PUnit.{u_2 + 1}) => A) ∅ PUnit.unit) x) = x