Socle families under algebra equivalence

An algebra equivalence transports a complete primitive-projective presentation label by label. This file records that transport before identifying the corresponding embedded socle ideals.

theorem MagnitudeConjecture.map_moduleSocle_le_of_semilinearEquiv {R : Type u₁} {T : Type u₂} [Ring R] [Ring T] {M : Type v₁} {N : Type v₂} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module T N] (σ : R ≃+* T) [RingHomInvPair σ.toRingHom σ.symm.toRingHom] [RingHomInvPair σ.symm.toRingHom σ.toRingHom] (e : M ≃ₛₗ[σ.toRingHom] N) : Submodule.map (↑e) (moduleSocle R M) ≤ moduleSocle T N

A semilinear equivalence over a ring equivalence carries the source socle into the target socle.

theorem MagnitudeConjecture.map_moduleSocle_eq_of_semilinearEquiv {R : Type u₁} {T : Type u₂} [Ring R] [Ring T] {M : Type v₁} {N : Type v₂} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module T N] (σ : R ≃+* T) [RingHomInvPair σ.toRingHom σ.symm.toRingHom] [RingHomInvPair σ.symm.toRingHom σ.toRingHom] (e : M ≃ₛₗ[σ.toRingHom] N) : Submodule.map (↑e) (moduleSocle R M) = moduleSocle T N

A semilinear equivalence over a ring equivalence carries the source socle exactly onto the target socle.

theorem MagnitudeConjecture.isUniserialModule_iff_of_semilinearEquiv {R : Type u₁} {T : Type u₂} [Ring R] [Ring T] {M : Type v₁} {N : Type v₂} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module T N] (σ : R ≃+* T) [RingHomInvPair σ.toRingHom σ.symm.toRingHom] [RingHomInvPair σ.symm.toRingHom σ.toRingHom] (e : M ≃ₛₗ[σ.toRingHom] N) : IsUniserialModule R M ↔ IsUniserialModule T N

Uniseriality is invariant under a semilinear equivalence whose scalar map is a ring equivalence.

def MagnitudeConjecture.RightModule.rightRegularMapAlgEquivSemilinearEquiv {k A B : Type u} [Field k] [Ring A] [Algebra k A] [Ring B] [Algebra k B] (f : A ≃ₐ[k] B) : let σ := (AlgEquiv.op f).toRingEquiv; A ≃ₛₗ[σ.toRingHom] B

Applying an algebra equivalence to the elements of the right regular module is semilinear over the induced equivalence of opposite rings.

@[simp]

theorem MagnitudeConjecture.RightModule.rightRegularMapAlgEquivSemilinearEquiv_apply {k A B : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] (f : A ≃ₐ[k] B) (x : A) : (rightRegularMapAlgEquivSemilinearEquiv f) x = f x

def MagnitudeConjecture.RightModule.rightIdealMapAlgEquivSemilinearEquiv {k A B : Type u} [Field k] [Ring A] [Algebra k A] [Ring B] [Algebra k B] (f : A ≃ₐ[k] B) (e : A) : let σ := (AlgEquiv.op f).toRingEquiv; ↥(rightIdeal e) ≃ₛₗ[σ.toRingHom] ↥(rightIdeal (f e))

Applying an algebra equivalence coefficientwise identifies the literal principal right ideals semilinearly over the opposite-ring equivalence.

@[simp]

theorem MagnitudeConjecture.RightModule.rightIdealMapAlgEquivSemilinearEquiv_apply_val {k A B : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] (f : A ≃ₐ[k] B) (e : A) (x : ↥(rightIdeal e)) : ↑((rightIdealMapAlgEquivSemilinearEquiv f e) x) = f ↑x

def MagnitudeConjecture.RightModule.fgModuleMapAlgEquivSemilinearEquiv {k A B : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [Ring B] [Algebra k B] [FiniteDimensional k B] (f : A ≃ₐ[k] B) (M : FinitelyGeneratedCategory A) : let σ := (AlgEquiv.op f).toRingEquiv; ↑M ≃ₛₗ[σ.toRingHom] ↑((fgModuleEquivalenceOfAlgEquiv f).functor.obj M)

The restriction-of-scalars image of a finitely generated right module has the same carrier, semilinearly identified over the opposite-ring equivalence.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.mapAlgEquivProjectiveLabelEquiv {k A B : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (f : A ≃ₐ[k] B) : S.ProjectiveLabel ≃ (S.mapAlgEquiv f).ProjectiveLabel

Projective labels of a transported skeleton correspond without changing their underlying finite label.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.mapAlgEquivProjectiveLabelEquiv_label {k A B : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (f : A ≃ₐ[k] B) (p : S.ProjectiveLabel) : ((S.mapAlgEquivProjectiveLabelEquiv f) p).label = p.label

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.fgObj_mapAlgEquiv_injective_iff {k A B : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (f : A ≃ₐ[k] B) (i : Fin S.n) : CategoryTheory.Injective ((S.mapAlgEquiv f).fgObj i) ↔ CategoryTheory.Injective (S.fgObj i)

Injectivity of a skeletal module is unchanged by transport through an algebra equivalence.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.fgObj_mapAlgEquiv_isUniserial_iff {k A B : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (f : A ≃ₐ[k] B) (i : Fin S.n) : IsUniserialModule Bᵐᵒᵖ ↑((S.mapAlgEquiv f).fgObj i) ↔ IsUniserialModule Aᵐᵒᵖ ↑(S.fgObj i)

Uniseriality of a skeletal module is unchanged by transport through an algebra equivalence.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.mapAlgEquiv {k A B : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (f : A ≃ₐ[k] B) : (S.mapAlgEquiv f).PrimitiveProjectivePresentation

Transport a complete primitive-projective presentation through an algebra equivalence.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.mapAlgEquiv_idempotent {k A B : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (f : A ≃ₐ[k] B) (p : S.ProjectiveLabel) : (P.mapAlgEquiv f).idempotent ((S.mapAlgEquivProjectiveLabelEquiv f) p) = f (P.idempotent p)

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.mapAlgEquivProjectiveLabel_injective_iff {k A B : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (f : A ≃ₐ[k] B) (p : S.ProjectiveLabel) : CategoryTheory.Injective ((S.mapAlgEquiv f).fgObj ((S.mapAlgEquivProjectiveLabelEquiv f) p).label) ↔ CategoryTheory.Injective (S.fgObj p.label)

The transported projective label is injective exactly when the original label is injective.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.mapAlgEquivProjectiveLabel_isUniserial_iff {k A B : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (f : A ≃ₐ[k] B) (p : S.ProjectiveLabel) : IsUniserialModule Bᵐᵒᵖ ↑((S.mapAlgEquiv f).fgObj ((S.mapAlgEquivProjectiveLabelEquiv f) p).label) ↔ IsUniserialModule Aᵐᵒᵖ ↑(S.fgObj p.label)

The transported projective label is uniserial exactly when the original label is uniserial.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.mem_primitiveProjectiveSocleSubmodule_mapAlgEquiv_iff {k A B : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (f : A ≃ₐ[k] B) (p : S.ProjectiveLabel) (x : A) : f x ∈ (P.mapAlgEquiv f).primitiveProjectiveSocleSubmodule ((S.mapAlgEquivProjectiveLabelEquiv f) p) ↔ x ∈ P.primitiveProjectiveSocleSubmodule p

Coefficientwise transport identifies the embedded socle of each primitive projective right ideal.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveProjectiveSocleIdeal_eq_comap_mapAlgEquiv {k A B : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (f : A ≃ₐ[k] B) (p : S.ProjectiveLabel) (hp : CategoryTheory.Injective (S.fgObj p.label)) : P.primitiveProjectiveSocleIdeal p hp = (TwoSidedIdeal.comap f) ((P.mapAlgEquiv f).primitiveProjectiveSocleIdeal ((S.mapAlgEquivProjectiveLabelEquiv f) p) ⋯)

Algebra equivalence carries each embedded primitive-projective socle ideal to the corresponding transported ideal.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.mapAlgEquivProjectiveLabels {k A B : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (f : A ≃ₐ[k] B) (T : Finset S.ProjectiveLabel) : Finset (S.mapAlgEquiv f).ProjectiveLabel

Transport a finite family of projective labels through an algebra equivalence.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.mem_mapAlgEquivProjectiveLabels {k A B : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (f : A ≃ₐ[k] B) (T : Finset S.ProjectiveLabel) (p : S.ProjectiveLabel) : (S.mapAlgEquivProjectiveLabelEquiv f) p ∈ mapAlgEquivProjectiveLabels S f T ↔ p ∈ T

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.mapAlgEquivProjectiveLabels_injective {k A B : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (f : A ≃ₐ[k] B) (T : Finset S.ProjectiveLabel) (hInjective : ∀ p ∈ T, CategoryTheory.Injective (S.fgObj p.label)) (q : (S.mapAlgEquiv f).ProjectiveLabel) : q ∈ mapAlgEquivProjectiveLabels S f T → CategoryTheory.Injective ((S.mapAlgEquiv f).fgObj q.label)

Injectivity data for a selected projective family transports label by label.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveProjectiveSocleFamilyIdeal_congr {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) {T U : Finset S.ProjectiveLabel} (hTU : T = U) (hT : ∀ p ∈ T, CategoryTheory.Injective (S.fgObj p.label)) (hU : ∀ p ∈ U, CategoryTheory.Injective (S.fgObj p.label)) : P.primitiveProjectiveSocleFamilyIdeal T hT = P.primitiveProjectiveSocleFamilyIdeal U hU

The simultaneous socle-family ideal depends on the selected finset, not on the proof term certifying injectivity of its members.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveProjectiveSocleFamilyIdeal_eq_comap_mapAlgEquiv {k A B : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (f : A ≃ₐ[k] B) (T : Finset S.ProjectiveLabel) (hInjective : ∀ p ∈ T, CategoryTheory.Injective (S.fgObj p.label)) : P.primitiveProjectiveSocleFamilyIdeal T hInjective = (TwoSidedIdeal.comap f) ((P.mapAlgEquiv f).primitiveProjectiveSocleFamilyIdeal (mapAlgEquivProjectiveLabels S f T) ⋯)

Algebra equivalence transports the simultaneous socle-family ideal.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveProjectiveSocleFamilyIdeal_ringCon_eq_comap_mapAlgEquiv {k A B : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (f : A ≃ₐ[k] B) (T : Finset S.ProjectiveLabel) (hInjective : ∀ p ∈ T, CategoryTheory.Injective (S.fgObj p.label)) : (P.primitiveProjectiveSocleFamilyIdeal T hInjective).ringCon = ((P.mapAlgEquiv f).primitiveProjectiveSocleFamilyIdeal (mapAlgEquivProjectiveLabels S f T) ⋯).ringCon.comap f

Ring congruences of the simultaneous socle-family quotients are transported by the ambient algebra equivalence.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveProjectiveSocleFamilyQuotientAlgEquiv {k A B : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (f : A ≃ₐ[k] B) (T : Finset S.ProjectiveLabel) (hInjective : ∀ p ∈ T, CategoryTheory.Injective (S.fgObj p.label)) : idealQuotientAlgebra (P.primitiveProjectiveSocleFamilyIdeal T hInjective) ≃ₐ[k] idealQuotientAlgebra ((P.mapAlgEquiv f).primitiveProjectiveSocleFamilyIdeal (mapAlgEquivProjectiveLabels S f T) ⋯)

Algebra equivalence transports the literal quotient by a simultaneous primitive-projective socle family.