Documentation

Mathlib.RingTheory.LocalProperties.Exactness

Local properties about linear maps #

In this file, we show that injectivity, surjectivity, bijectivity and exactness of linear maps are local properties. More precisely, we show that these can be checked at maximal ideals and on standard covers.

source
๐Ÿ“ coverage
theorem injective_of_isLocalized_maximal {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (Mโ‚š : (P : Ideal R) โ†’ [P.IsMaximal] โ†’ Type u_6) [(P : Ideal R) โ†’ [inst : P.IsMaximal] โ†’ AddCommMonoid (Mโ‚š P)] [(P : Ideal R) โ†’ [inst : P.IsMaximal] โ†’ Module R (Mโ‚š P)] (f : (P : Ideal R) โ†’ [inst : P.IsMaximal] โ†’ M โ†’โ‚—[R] Mโ‚š P) [โˆ€ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule.AtPrime P (f P)] (Nโ‚š : (P : Ideal R) โ†’ [P.IsMaximal] โ†’ Type u_7) [(P : Ideal R) โ†’ [inst : P.IsMaximal] โ†’ AddCommMonoid (Nโ‚š P)] [(P : Ideal R) โ†’ [inst : P.IsMaximal] โ†’ Module R (Nโ‚š P)] (g : (P : Ideal R) โ†’ [inst : P.IsMaximal] โ†’ N โ†’โ‚—[R] Nโ‚š P) [โˆ€ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule.AtPrime P (g P)] (F : M โ†’โ‚—[R] N) (H : โˆ€ (P : Ideal R) [inst : P.IsMaximal], Function.Injective โ‡‘((IsLocalizedModule.map P.primeCompl (f P) (g P)) F)) :
Function.Injective โ‡‘F
source
๐Ÿ“ coverage
theorem surjective_of_isLocalized_maximal {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (Mโ‚š : (P : Ideal R) โ†’ [P.IsMaximal] โ†’ Type u_6) [(P : Ideal R) โ†’ [inst : P.IsMaximal] โ†’ AddCommMonoid (Mโ‚š P)] [(P : Ideal R) โ†’ [inst : P.IsMaximal] โ†’ Module R (Mโ‚š P)] (f : (P : Ideal R) โ†’ [inst : P.IsMaximal] โ†’ M โ†’โ‚—[R] Mโ‚š P) [โˆ€ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule.AtPrime P (f P)] (Nโ‚š : (P : Ideal R) โ†’ [P.IsMaximal] โ†’ Type u_7) [(P : Ideal R) โ†’ [inst : P.IsMaximal] โ†’ AddCommMonoid (Nโ‚š P)] [(P : Ideal R) โ†’ [inst : P.IsMaximal] โ†’ Module R (Nโ‚š P)] (g : (P : Ideal R) โ†’ [inst : P.IsMaximal] โ†’ N โ†’โ‚—[R] Nโ‚š P) [โˆ€ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule.AtPrime P (g P)] (F : M โ†’โ‚—[R] N) (H : โˆ€ (P : Ideal R) [inst : P.IsMaximal], Function.Surjective โ‡‘((IsLocalizedModule.map P.primeCompl (f P) (g P)) F)) :
Function.Surjective โ‡‘F
source
๐Ÿ“ coverage
theorem bijective_of_isLocalized_maximal {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (Mโ‚š : (P : Ideal R) โ†’ [P.IsMaximal] โ†’ Type u_6) [(P : Ideal R) โ†’ [inst : P.IsMaximal] โ†’ AddCommMonoid (Mโ‚š P)] [(P : Ideal R) โ†’ [inst : P.IsMaximal] โ†’ Module R (Mโ‚š P)] (f : (P : Ideal R) โ†’ [inst : P.IsMaximal] โ†’ M โ†’โ‚—[R] Mโ‚š P) [โˆ€ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule.AtPrime P (f P)] (Nโ‚š : (P : Ideal R) โ†’ [P.IsMaximal] โ†’ Type u_7) [(P : Ideal R) โ†’ [inst : P.IsMaximal] โ†’ AddCommMonoid (Nโ‚š P)] [(P : Ideal R) โ†’ [inst : P.IsMaximal] โ†’ Module R (Nโ‚š P)] (g : (P : Ideal R) โ†’ [inst : P.IsMaximal] โ†’ N โ†’โ‚—[R] Nโ‚š P) [โˆ€ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule.AtPrime P (g P)] (F : M โ†’โ‚—[R] N) (H : โˆ€ (P : Ideal R) [inst : P.IsMaximal], Function.Bijective โ‡‘((IsLocalizedModule.map P.primeCompl (f P) (g P)) F)) :
Function.Bijective โ‡‘F
source
๐Ÿ“ coverage
theorem exact_of_isLocalized_maximal {R : Type u_1} {M : Type u_2} {N : Type u_3} {L : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid L] [Module R L] (Mโ‚š : (P : Ideal R) โ†’ [P.IsMaximal] โ†’ Type u_6) [(P : Ideal R) โ†’ [inst : P.IsMaximal] โ†’ AddCommMonoid (Mโ‚š P)] [(P : Ideal R) โ†’ [inst : P.IsMaximal] โ†’ Module R (Mโ‚š P)] (f : (P : Ideal R) โ†’ [inst : P.IsMaximal] โ†’ M โ†’โ‚—[R] Mโ‚š P) [โˆ€ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule.AtPrime P (f P)] (Nโ‚š : (P : Ideal R) โ†’ [P.IsMaximal] โ†’ Type u_7) [(P : Ideal R) โ†’ [inst : P.IsMaximal] โ†’ AddCommMonoid (Nโ‚š P)] [(P : Ideal R) โ†’ [inst : P.IsMaximal] โ†’ Module R (Nโ‚š P)] (g : (P : Ideal R) โ†’ [inst : P.IsMaximal] โ†’ N โ†’โ‚—[R] Nโ‚š P) [โˆ€ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule.AtPrime P (g P)] (Lโ‚š : (P : Ideal R) โ†’ [P.IsMaximal] โ†’ Type u_8) [(P : Ideal R) โ†’ [inst : P.IsMaximal] โ†’ AddCommMonoid (Lโ‚š P)] [(P : Ideal R) โ†’ [inst : P.IsMaximal] โ†’ Module R (Lโ‚š P)] (h : (P : Ideal R) โ†’ [inst : P.IsMaximal] โ†’ L โ†’โ‚—[R] Lโ‚š P) [โˆ€ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule.AtPrime P (h P)] (F : M โ†’โ‚—[R] N) (G : N โ†’โ‚—[R] L) (H : โˆ€ (J : Ideal R) [inst : J.IsMaximal], Function.Exact โ‡‘((IsLocalizedModule.map J.primeCompl (f J) (g J)) F) โ‡‘((IsLocalizedModule.map J.primeCompl (g J) (h J)) G)) :
Function.Exact โ‡‘F โ‡‘G
source
๐Ÿ“ coverage
theorem LinearIndependent.of_isLocalized_maximal {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (Rโ‚š : (P : Ideal R) โ†’ [P.IsMaximal] โ†’ Type u_5) [(P : Ideal R) โ†’ [inst : P.IsMaximal] โ†’ CommSemiring (Rโ‚š P)] [(P : Ideal R) โ†’ [inst : P.IsMaximal] โ†’ Algebra R (Rโ‚š P)] [โˆ€ (P : Ideal R) [inst : P.IsMaximal], IsLocalization.AtPrime (Rโ‚š P) P] (Mโ‚š : (P : Ideal R) โ†’ [P.IsMaximal] โ†’ Type u_6) [(P : Ideal R) โ†’ [inst : P.IsMaximal] โ†’ AddCommMonoid (Mโ‚š P)] [(P : Ideal R) โ†’ [inst : P.IsMaximal] โ†’ Module R (Mโ‚š P)] [(P : Ideal R) โ†’ [inst : P.IsMaximal] โ†’ Module (Rโ‚š P) (Mโ‚š P)] [โˆ€ (P : Ideal R) [inst : P.IsMaximal], IsScalarTower R (Rโ‚š P) (Mโ‚š P)] (f : (P : Ideal R) โ†’ [inst : P.IsMaximal] โ†’ M โ†’โ‚—[R] Mโ‚š P) [โˆ€ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule.AtPrime P (f P)] {ฮน : Type u_9} (v : ฮน โ†’ M) (H : โˆ€ (P : Ideal R) [inst : P.IsMaximal], LinearIndependent (Rโ‚š P) (โ‡‘(f P) โˆ˜ v)) :
LinearIndependent R v
source
๐Ÿ“ coverage
theorem injective_of_localized_maximal {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (f : M โ†’โ‚—[R] N) (h : โˆ€ (J : Ideal R) [inst : J.IsMaximal], Function.Injective โ‡‘((LocalizedModule.map J.primeCompl) f)) :
Function.Injective โ‡‘f
source
๐Ÿ“ coverage
theorem surjective_of_localized_maximal {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (f : M โ†’โ‚—[R] N) (h : โˆ€ (J : Ideal R) [inst : J.IsMaximal], Function.Surjective โ‡‘((LocalizedModule.map J.primeCompl) f)) :
Function.Surjective โ‡‘f
source
๐Ÿ“ coverage
theorem bijective_of_localized_maximal {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (f : M โ†’โ‚—[R] N) (h : โˆ€ (J : Ideal R) [inst : J.IsMaximal], Function.Bijective โ‡‘((LocalizedModule.map J.primeCompl) f)) :
Function.Bijective โ‡‘f
source
๐Ÿ“ coverage
theorem exact_of_localized_maximal {R : Type u_1} {M : Type u_2} {N : Type u_3} {L : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid L] [Module R L] (f : M โ†’โ‚—[R] N) (g : N โ†’โ‚—[R] L) (h : โˆ€ (J : Ideal R) [inst : J.IsMaximal], Function.Exact โ‡‘((LocalizedModule.map J.primeCompl) f) โ‡‘((LocalizedModule.map J.primeCompl) g)) :
Function.Exact โ‡‘f โ‡‘g
source
๐Ÿ“ coverage
theorem injective_of_isLocalized_span {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (s : Set R) (spn : Ideal.span s = โŠค) (Mโ‚š : โ†‘s โ†’ Type u_5) [(r : โ†‘s) โ†’ AddCommMonoid (Mโ‚š r)] [(r : โ†‘s) โ†’ Module R (Mโ‚š r)] (f : (r : โ†‘s) โ†’ M โ†’โ‚—[R] Mโ‚š r) [โˆ€ (r : โ†‘s), IsLocalizedModule.Away (โ†‘r) (f r)] (Nโ‚š : โ†‘s โ†’ Type u_6) [(r : โ†‘s) โ†’ AddCommMonoid (Nโ‚š r)] [(r : โ†‘s) โ†’ Module R (Nโ‚š r)] (g : (r : โ†‘s) โ†’ N โ†’โ‚—[R] Nโ‚š r) [โˆ€ (r : โ†‘s), IsLocalizedModule.Away (โ†‘r) (g r)] (F : M โ†’โ‚—[R] N) (H : โˆ€ (r : โ†‘s), Function.Injective โ‡‘((IsLocalizedModule.map (Submonoid.powers โ†‘r) (f r) (g r)) F)) :
Function.Injective โ‡‘F
source
๐Ÿ“ coverage
theorem surjective_of_isLocalized_span {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (s : Set R) (spn : Ideal.span s = โŠค) (Mโ‚š : โ†‘s โ†’ Type u_5) [(r : โ†‘s) โ†’ AddCommMonoid (Mโ‚š r)] [(r : โ†‘s) โ†’ Module R (Mโ‚š r)] (f : (r : โ†‘s) โ†’ M โ†’โ‚—[R] Mโ‚š r) [โˆ€ (r : โ†‘s), IsLocalizedModule.Away (โ†‘r) (f r)] (Nโ‚š : โ†‘s โ†’ Type u_6) [(r : โ†‘s) โ†’ AddCommMonoid (Nโ‚š r)] [(r : โ†‘s) โ†’ Module R (Nโ‚š r)] (g : (r : โ†‘s) โ†’ N โ†’โ‚—[R] Nโ‚š r) [โˆ€ (r : โ†‘s), IsLocalizedModule.Away (โ†‘r) (g r)] (F : M โ†’โ‚—[R] N) (H : โˆ€ (r : โ†‘s), Function.Surjective โ‡‘((IsLocalizedModule.map (Submonoid.powers โ†‘r) (f r) (g r)) F)) :
Function.Surjective โ‡‘F
source
๐Ÿ“ coverage
theorem bijective_of_isLocalized_span {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (s : Set R) (spn : Ideal.span s = โŠค) (Mโ‚š : โ†‘s โ†’ Type u_5) [(r : โ†‘s) โ†’ AddCommMonoid (Mโ‚š r)] [(r : โ†‘s) โ†’ Module R (Mโ‚š r)] (f : (r : โ†‘s) โ†’ M โ†’โ‚—[R] Mโ‚š r) [โˆ€ (r : โ†‘s), IsLocalizedModule.Away (โ†‘r) (f r)] (Nโ‚š : โ†‘s โ†’ Type u_6) [(r : โ†‘s) โ†’ AddCommMonoid (Nโ‚š r)] [(r : โ†‘s) โ†’ Module R (Nโ‚š r)] (g : (r : โ†‘s) โ†’ N โ†’โ‚—[R] Nโ‚š r) [โˆ€ (r : โ†‘s), IsLocalizedModule.Away (โ†‘r) (g r)] (F : M โ†’โ‚—[R] N) (H : โˆ€ (r : โ†‘s), Function.Bijective โ‡‘((IsLocalizedModule.map (Submonoid.powers โ†‘r) (f r) (g r)) F)) :
Function.Bijective โ‡‘F
source
๐Ÿ“ coverage
theorem exact_of_isLocalized_span {R : Type u_1} {M : Type u_2} {N : Type u_3} {L : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid L] [Module R L] (s : Set R) (spn : Ideal.span s = โŠค) (Mโ‚š : โ†‘s โ†’ Type u_5) [(r : โ†‘s) โ†’ AddCommMonoid (Mโ‚š r)] [(r : โ†‘s) โ†’ Module R (Mโ‚š r)] (f : (r : โ†‘s) โ†’ M โ†’โ‚—[R] Mโ‚š r) [โˆ€ (r : โ†‘s), IsLocalizedModule.Away (โ†‘r) (f r)] (Nโ‚š : โ†‘s โ†’ Type u_6) [(r : โ†‘s) โ†’ AddCommMonoid (Nโ‚š r)] [(r : โ†‘s) โ†’ Module R (Nโ‚š r)] (g : (r : โ†‘s) โ†’ N โ†’โ‚—[R] Nโ‚š r) [โˆ€ (r : โ†‘s), IsLocalizedModule.Away (โ†‘r) (g r)] (Lโ‚š : โ†‘s โ†’ Type u_7) [(r : โ†‘s) โ†’ AddCommMonoid (Lโ‚š r)] [(r : โ†‘s) โ†’ Module R (Lโ‚š r)] (h : (r : โ†‘s) โ†’ L โ†’โ‚—[R] Lโ‚š r) [โˆ€ (r : โ†‘s), IsLocalizedModule.Away (โ†‘r) (h r)] (F : M โ†’โ‚—[R] N) (G : N โ†’โ‚—[R] L) (H : โˆ€ (r : โ†‘s), Function.Exact โ‡‘((IsLocalizedModule.map (Submonoid.powers โ†‘r) (f r) (g r)) F) โ‡‘((IsLocalizedModule.map (Submonoid.powers โ†‘r) (g r) (h r)) G)) :
Function.Exact โ‡‘F โ‡‘G
source
๐Ÿ“ coverage
theorem injective_of_localized_span {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (s : Set R) (spn : Ideal.span s = โŠค) (f : M โ†’โ‚—[R] N) (h : โˆ€ (r : โ†‘s), Function.Injective โ‡‘((LocalizedModule.map (Submonoid.powers โ†‘r)) f)) :
Function.Injective โ‡‘f
source
๐Ÿ“ coverage
theorem surjective_of_localized_span {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (s : Set R) (spn : Ideal.span s = โŠค) (f : M โ†’โ‚—[R] N) (h : โˆ€ (r : โ†‘s), Function.Surjective โ‡‘((LocalizedModule.map (Submonoid.powers โ†‘r)) f)) :
Function.Surjective โ‡‘f
source
๐Ÿ“ coverage
theorem bijective_of_localized_span {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (s : Set R) (spn : Ideal.span s = โŠค) (f : M โ†’โ‚—[R] N) (h : โˆ€ (r : โ†‘s), Function.Bijective โ‡‘((LocalizedModule.map (Submonoid.powers โ†‘r)) f)) :
Function.Bijective โ‡‘f
source
๐Ÿ“ coverage
theorem exact_of_localized_span {R : Type u_1} {M : Type u_2} {N : Type u_3} {L : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid L] [Module R L] (s : Set R) (spn : Ideal.span s = โŠค) (f : M โ†’โ‚—[R] N) (g : N โ†’โ‚—[R] L) (h : โˆ€ (r : โ†‘s), Function.Exact โ‡‘((LocalizedModule.map (Submonoid.powers โ†‘r)) f) โ‡‘((LocalizedModule.map (Submonoid.powers โ†‘r)) g)) :
Function.Exact โ‡‘f โ‡‘g
source
๐Ÿ“ coverage
theorem IsLocalizedModule.map_linearMap_of_isLocalization {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] [Algebra R S] (Rโ‚š : Type u_5) (Sโ‚š : Type u_6) [CommSemiring Rโ‚š] [Algebra R Rโ‚š] [CommSemiring Sโ‚š] [Algebra S Sโ‚š] [Algebra R Sโ‚š] [IsScalarTower R S Sโ‚š] [Algebra Rโ‚š Sโ‚š] [IsScalarTower R Rโ‚š Sโ‚š] (p : Ideal R) [p.IsPrime] [IsLocalization.AtPrime Rโ‚š p] [IsLocalizedModule.AtPrime p โ†‘(IsScalarTower.toAlgHom R S Sโ‚š)] :
(map p.primeCompl (Algebra.linearMap R Rโ‚š) โ†‘(IsScalarTower.toAlgHom R S Sโ‚š)) (Algebra.linearMap R S) = โ†‘R (Algebra.linearMap Rโ‚š Sโ‚š)
source
๐Ÿ“ coverage
theorem injective_of_isLocalization_isMaximal {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] [Algebra R S] (Rโ‚š : (p : Ideal R) โ†’ [p.IsMaximal] โ†’ Type u_3) [(p : Ideal R) โ†’ [inst : p.IsMaximal] โ†’ CommSemiring (Rโ‚š p)] [(p : Ideal R) โ†’ [inst : p.IsMaximal] โ†’ Algebra R (Rโ‚š p)] (Sโ‚š : (p : Ideal R) โ†’ [p.IsMaximal] โ†’ Type u_4) [(p : Ideal R) โ†’ [inst : p.IsMaximal] โ†’ CommSemiring (Sโ‚š p)] [(p : Ideal R) โ†’ [inst : p.IsMaximal] โ†’ Algebra S (Sโ‚š p)] [(p : Ideal R) โ†’ [inst : p.IsMaximal] โ†’ Algebra (Rโ‚š p) (Sโ‚š p)] [(p : Ideal R) โ†’ [inst : p.IsMaximal] โ†’ Algebra R (Sโ‚š p)] [โˆ€ (p : Ideal R) [inst : p.IsMaximal], IsScalarTower R (Rโ‚š p) (Sโ‚š p)] [โˆ€ (p : Ideal R) [inst : p.IsMaximal], IsScalarTower R S (Sโ‚š p)] [โˆ€ (p : Ideal R) [inst : p.IsMaximal], IsLocalization.AtPrime (Rโ‚š p) p] [โˆ€ (p : Ideal R) [inst : p.IsMaximal], IsLocalizedModule.AtPrime p โ†‘(IsScalarTower.toAlgHom R S (Sโ‚š p))] (H : โˆ€ (p : Ideal R) [inst : p.IsMaximal], Function.Injective โ‡‘(algebraMap (Rโ‚š p) (Sโ‚š p))) :
Function.Injective โ‡‘(algebraMap R S)
source
๐Ÿ“ coverage
theorem surjective_of_isLocalization_isMaximal {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] [Algebra R S] (Rโ‚š : (p : Ideal R) โ†’ [p.IsMaximal] โ†’ Type u_3) [(p : Ideal R) โ†’ [inst : p.IsMaximal] โ†’ CommSemiring (Rโ‚š p)] [(p : Ideal R) โ†’ [inst : p.IsMaximal] โ†’ Algebra R (Rโ‚š p)] (Sโ‚š : (p : Ideal R) โ†’ [p.IsMaximal] โ†’ Type u_4) [(p : Ideal R) โ†’ [inst : p.IsMaximal] โ†’ CommSemiring (Sโ‚š p)] [(p : Ideal R) โ†’ [inst : p.IsMaximal] โ†’ Algebra S (Sโ‚š p)] [(p : Ideal R) โ†’ [inst : p.IsMaximal] โ†’ Algebra (Rโ‚š p) (Sโ‚š p)] [(p : Ideal R) โ†’ [inst : p.IsMaximal] โ†’ Algebra R (Sโ‚š p)] [โˆ€ (p : Ideal R) [inst : p.IsMaximal], IsScalarTower R (Rโ‚š p) (Sโ‚š p)] [โˆ€ (p : Ideal R) [inst : p.IsMaximal], IsScalarTower R S (Sโ‚š p)] [โˆ€ (p : Ideal R) [inst : p.IsMaximal], IsLocalization.AtPrime (Rโ‚š p) p] [โˆ€ (p : Ideal R) [inst : p.IsMaximal], IsLocalizedModule.AtPrime p โ†‘(IsScalarTower.toAlgHom R S (Sโ‚š p))] (H : โˆ€ (p : Ideal R) [inst : p.IsMaximal], Function.Surjective โ‡‘(algebraMap (Rโ‚š p) (Sโ‚š p))) :
Function.Surjective โ‡‘(algebraMap R S)
source
๐Ÿ“ coverage
theorem bijective_of_isLocalization_isMaximal {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] [Algebra R S] (Rโ‚š : (p : Ideal R) โ†’ [p.IsMaximal] โ†’ Type u_3) [(p : Ideal R) โ†’ [inst : p.IsMaximal] โ†’ CommSemiring (Rโ‚š p)] [(p : Ideal R) โ†’ [inst : p.IsMaximal] โ†’ Algebra R (Rโ‚š p)] (Sโ‚š : (p : Ideal R) โ†’ [p.IsMaximal] โ†’ Type u_4) [(p : Ideal R) โ†’ [inst : p.IsMaximal] โ†’ CommSemiring (Sโ‚š p)] [(p : Ideal R) โ†’ [inst : p.IsMaximal] โ†’ Algebra S (Sโ‚š p)] [(p : Ideal R) โ†’ [inst : p.IsMaximal] โ†’ Algebra (Rโ‚š p) (Sโ‚š p)] [(p : Ideal R) โ†’ [inst : p.IsMaximal] โ†’ Algebra R (Sโ‚š p)] [โˆ€ (p : Ideal R) [inst : p.IsMaximal], IsScalarTower R (Rโ‚š p) (Sโ‚š p)] [โˆ€ (p : Ideal R) [inst : p.IsMaximal], IsScalarTower R S (Sโ‚š p)] [โˆ€ (p : Ideal R) [inst : p.IsMaximal], IsLocalization.AtPrime (Rโ‚š p) p] [โˆ€ (p : Ideal R) [inst : p.IsMaximal], IsLocalizedModule.AtPrime p โ†‘(IsScalarTower.toAlgHom R S (Sโ‚š p))] (H : โˆ€ (p : Ideal R) [inst : p.IsMaximal], Function.Bijective โ‡‘(algebraMap (Rโ‚š p) (Sโ‚š p))) :
Function.Bijective โ‡‘(algebraMap R S)
source
๐Ÿ“ coverage
theorem injective_of_isLocalization_of_span_eq_top {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] {s : Set R} (hs : Ideal.span s = โŠค) (Rแตฃ : โ†‘s โ†’ Type u_3) [(r : โ†‘s) โ†’ CommSemiring (Rแตฃ r)] [(r : โ†‘s) โ†’ Algebra R (Rแตฃ r)] (Sแตฃ : โ†‘s โ†’ Type u_4) [(r : โ†‘s) โ†’ CommSemiring (Sแตฃ r)] [(r : โ†‘s) โ†’ Algebra S (Sแตฃ r)] (f : R โ†’+* S) [โˆ€ (r : โ†‘s), IsLocalization.Away (โ†‘r) (Rแตฃ r)] [โˆ€ (r : โ†‘s), IsLocalization.Away (f โ†‘r) (Sแตฃ r)] (h : โˆ€ (r : โ†‘s), Function.Injective โ‡‘(IsLocalization.Away.map (Rแตฃ r) (Sแตฃ r) f โ†‘r)) :
Function.Injective โ‡‘f
source
๐Ÿ“ coverage
theorem surjective_of_isLocalization_of_span_eq_top {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] {s : Set R} (hs : Ideal.span s = โŠค) (Rแตฃ : โ†‘s โ†’ Type u_3) [(r : โ†‘s) โ†’ CommSemiring (Rแตฃ r)] [(r : โ†‘s) โ†’ Algebra R (Rแตฃ r)] (Sแตฃ : โ†‘s โ†’ Type u_4) [(r : โ†‘s) โ†’ CommSemiring (Sแตฃ r)] [(r : โ†‘s) โ†’ Algebra S (Sแตฃ r)] (f : R โ†’+* S) [โˆ€ (r : โ†‘s), IsLocalization.Away (โ†‘r) (Rแตฃ r)] [โˆ€ (r : โ†‘s), IsLocalization.Away (f โ†‘r) (Sแตฃ r)] (h : โˆ€ (r : โ†‘s), Function.Surjective โ‡‘(IsLocalization.Away.map (Rแตฃ r) (Sแตฃ r) f โ†‘r)) :
Function.Surjective โ‡‘f
source
๐Ÿ“ coverage
theorem bijective_of_isLocalization_of_span_eq_top {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] {s : Set R} (hs : Ideal.span s = โŠค) (Rแตฃ : โ†‘s โ†’ Type u_3) [(r : โ†‘s) โ†’ CommSemiring (Rแตฃ r)] [(r : โ†‘s) โ†’ Algebra R (Rแตฃ r)] (Sแตฃ : โ†‘s โ†’ Type u_4) [(r : โ†‘s) โ†’ CommSemiring (Sแตฃ r)] [(r : โ†‘s) โ†’ Algebra S (Sแตฃ r)] (f : R โ†’+* S) [โˆ€ (r : โ†‘s), IsLocalization.Away (โ†‘r) (Rแตฃ r)] [โˆ€ (r : โ†‘s), IsLocalization.Away (f โ†‘r) (Sแตฃ r)] (h : โˆ€ (r : โ†‘s), Function.Bijective โ‡‘(IsLocalization.Away.map (Rแตฃ r) (Sแตฃ r) f โ†‘r)) :
Function.Bijective โ‡‘f