Transporting graded-module localizations along equal denominators

The equivalences in this file change only the name of an equal power submonoid. They are generic graded-module localization operations; Čech complexes consume them when comparing product and monomial denominators.

noncomputable def GradedModule.DegreeZeroLocalization.powersCongr {ι : Type u_1} {A : Type u_2} {M : Type u_3} {σA : Type u_4} {σM : Type u_5} [AddCommMonoid ι] [DecidableEq ι] [CommRing A] [AddCommGroup M] [Module A M] [SetLike σA A] [AddSubgroupClass σA A] [SetLike σM M] [AddSubgroupClass σM M] {𝒜 : ι → σA} {𝓜 : ι → σM} [GradedRing 𝒜] [SetLike.GradedSMul 𝒜 𝓜] {f g : A} (h : f = g) : ↥(DegreeZeroLocalization 𝒜 𝓜 (Submonoid.powers f)) ≃+ ↥(DegreeZeroLocalization 𝒜 𝓜 (Submonoid.powers g))

Transport a degree-zero localization along an equality of denominators. The element never moves; only the name of its type does.

Equations

• GradedModule.DegreeZeroLocalization.powersCongr h = h ▸ AddEquiv.refl ↥(GradedModule.DegreeZeroLocalization 𝒜 𝓜 (Submonoid.powers f))

theorem GradedModule.DegreeZeroLocalization.powersCongr_awayMk {ι : Type u_1} {A : Type u_2} {M : Type u_3} {σA : Type u_4} {σM : Type u_5} [AddCommMonoid ι] [DecidableEq ι] [CommRing A] [AddCommGroup M] [Module A M] [SetLike σA A] [AddSubgroupClass σA A] [SetLike σM M] [AddSubgroupClass σM M] {𝒜 : ι → σA} {𝓜 : ι → σM} [GradedRing 𝒜] [SetLike.GradedSMul 𝒜 𝓜] {f g : A} (h : f = g) {e : ι} (hf : f ∈ 𝒜 e) (hg : g ∈ 𝒜 e) (n : ℕ) (m : M) (hm : m ∈ 𝓜 (n • e)) : (powersCongr h) (awayMk hf n m hm) = awayMk hg n m hm

theorem GradedModule.DegreeZeroLocalization.powersCongr_trans {ι : Type u_1} {A : Type u_2} {M : Type u_3} {σA : Type u_4} {σM : Type u_5} [AddCommMonoid ι] [DecidableEq ι] [CommRing A] [AddCommGroup M] [Module A M] [SetLike σA A] [AddSubgroupClass σA A] [SetLike σM M] [AddSubgroupClass σM M] {𝒜 : ι → σA} {𝓜 : ι → σM} [GradedRing 𝒜] [SetLike.GradedSMul 𝒜 𝓜] {f g l : A} (h₁ : f = g) (h₂ : g = l) (z : ↥(DegreeZeroLocalization 𝒜 𝓜 (Submonoid.powers f))) : (powersCongr h₂) ((powersCongr h₁) z) = (powersCongr ⋯) z

theorem GradedModule.DegreeZeroLocalization.powersCongr_symm_apply_apply {ι : Type u_1} {A : Type u_2} {M : Type u_3} {σA : Type u_4} {σM : Type u_5} [AddCommMonoid ι] [DecidableEq ι] [CommRing A] [AddCommGroup M] [Module A M] [SetLike σA A] [AddSubgroupClass σA A] [SetLike σM M] [AddSubgroupClass σM M] {𝒜 : ι → σA} {𝓜 : ι → σM} [GradedRing 𝒜] [SetLike.GradedSMul 𝒜 𝓜] {f g : A} (h : f = g) (z : ↥(DegreeZeroLocalization 𝒜 𝓜 (Submonoid.powers f))) : (powersCongr h).symm ((powersCongr h) z) = z

theorem GradedModule.DegreeZeroLocalization.powersCongr_symm_trans {ι : Type u_1} {A : Type u_2} {M : Type u_3} {σA : Type u_4} {σM : Type u_5} [AddCommMonoid ι] [DecidableEq ι] [CommRing A] [AddCommGroup M] [Module A M] [SetLike σA A] [AddSubgroupClass σA A] [SetLike σM M] [AddSubgroupClass σM M] {𝒜 : ι → σA} {𝓜 : ι → σM} [GradedRing 𝒜] [SetLike.GradedSMul 𝒜 𝓜] {f g l : A} (h₀ : f = g) (e₁ : f = l) (h₁ : g = l) (u : ↥(DegreeZeroLocalization 𝒜 𝓜 (Submonoid.powers g))) : (powersCongr e₁) ((powersCongr h₀).symm u) = (powersCongr h₁) u

Absorb an inverse transport into a forward one.

theorem GradedModule.DegreeZeroLocalization.powersCongr_faceMap {ι : Type u_1} {A : Type u_2} {M : Type u_3} {σA : Type u_4} {σM : Type u_5} [AddCommMonoid ι] [DecidableEq ι] [CommRing A] [AddCommGroup M] [Module A M] [SetLike σA A] [AddSubgroupClass σA A] [SetLike σM M] [AddSubgroupClass σM M] {𝒜 : ι → σA} {𝓜 : ι → σM} [GradedRing 𝒜] [SetLike.GradedSMul 𝒜 𝓜] {g₁ g₁' g₂ g₂' w w' : A} {e : ι} (e₁ : g₁ = g₁') (e₂ : g₂ = g₂') (e₃ : w = w') (hw : w ∈ 𝒜 e) (hw' : w' ∈ 𝒜 e) (hgw : g₁ * w ∈ Submonoid.powers g₂) (hgw' : g₁' * w' ∈ Submonoid.powers g₂') (hg : g₁ * w = g₂) (hg' : g₁' * w' = g₂') (z : ↥(DegreeZeroLocalization 𝒜 𝓜 (Submonoid.powers g₁))) : (powersCongr e₂) ((faceMap hw hgw hg) z) = (faceMap hw' hgw' hg') ((powersCongr e₁) z)

Transport a face map along equalities of both denominators and of the multiplier.