ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>J : Type v<VAR>CategoryTheory.SmallCategory J<VAR>F : J ⥤ RingCat<VAR>x y : RingCat.Colimits.Prequotient F<GOAL>Quot.mk Setoid.r (x.mul y) = Quot.mk Setoid.r x * Quot.mk Setoid.r y
<VAR>J : Type v<VAR>CategoryTheory.SmallCategory J<VAR>F : J ⥤ RingCat<VAR>j j' : J<VAR>f : j ⟶ j'<GOAL>F.map f ≫ RingCat.Colimits.coconeMorphism F j' = RingCat.Colimits.coconeMorphism F j
<VAR>J : Type v<VAR>CategoryTheory.SmallCategory J<VAR>F : J ⥤ RingCat<VAR>j j' : J<VAR>f : j ⟶ j'<VAR>x : ↑(F.obj j)<GOAL>(RingCat.Colimits.coconeMorphism F j') ((F.map f) x) = (RingCat.Colimits.coconeMorphism F j) x
<VAR>J : Type v<VAR>CategoryTheory.SmallCategory J<VAR>F : J ⥤ CommRingCat<GOAL>Quot.mk Setoid.r CommRingCat.Colimits.Prequotient.zero = 0
<VAR>J : Type v<VAR>CategoryTheory.SmallCategory J<VAR>F : J ⥤ CommRingCat<GOAL>Quot.mk Setoid.r CommRingCat.Colimits.Prequotient.one = 1
<VAR>J : Type v<VAR>CategoryTheory.SmallCategory J<VAR>F : J ⥤ CommRingCat<VAR>x : CommRingCat.Colimits.Prequotient F<GOAL>Quot.mk Setoid.r x.neg = -Quot.mk Setoid.r x
<VAR>J : Type v<VAR>CategoryTheory.SmallCategory J<VAR>F : J ⥤ CommRingCat<VAR>x y : CommRingCat.Colimits.Prequotient F<GOAL>Quot.mk Setoid.r (x.add y) = Quot.mk Setoid.r x + Quot.mk Setoid.r y
<VAR>J : Type v<VAR>CategoryTheory.SmallCategory J<VAR>F : J ⥤ CommRingCat<VAR>x y : CommRingCat.Colimits.Prequotient F<GOAL>Quot.mk Setoid.r (x.mul y) = Quot.mk Setoid.r x * Quot.mk Setoid.r y
<VAR>J : Type v<VAR>CategoryTheory.SmallCategory J<VAR>F : J ⥤ CommRingCat<VAR>j j' : J<VAR>f : j ⟶ j'<GOAL>F.map f ≫ CommRingCat.Colimits.coconeMorphism F j' = CommRingCat.Colimits.coconeMorphism F j
<VAR>J : Type v<VAR>CategoryTheory.SmallCategory J<VAR>F : J ⥤ CommRingCat<VAR>j j' : J<VAR>f : j ⟶ j'<VAR>x : ↑(F.obj j)<GOAL>(CommRingCat.Colimits.coconeMorphism F j') ((F.map f) x) = (CommRingCat.Colimits.coconeMorphism F j) x
<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>F : J ⥤ AddCommGrp<GOAL>Quot.mk Setoid.r AddCommGrp.Colimits.Prequotient.zero = 0
<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>F : J ⥤ AddCommGrp<VAR>x : AddCommGrp.Colimits.Prequotient F<GOAL>Quot.mk Setoid.r x.neg = -Quot.mk Setoid.r x
<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>F : J ⥤ AddCommGrp<VAR>x y : AddCommGrp.Colimits.Prequotient F<GOAL>Quot.mk Setoid.r (x.add y) = Quot.mk Setoid.r x + Quot.mk Setoid.r y
<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>F : J ⥤ AddCommGrp<VAR>j j' : J<VAR>f : j ⟶ j'<GOAL>F.map f ≫ AddCommGrp.Colimits.coconeMorphism F j' = AddCommGrp.Colimits.coconeMorphism F j
<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>F : J ⥤ AddCommGrp<VAR>j j' : J<VAR>f : j ⟶ j'<VAR>x : ↑(F.obj j)<GOAL>(AddCommGrp.Colimits.coconeMorphism F j') ((F.map f) x) = (AddCommGrp.Colimits.coconeMorphism F j) x
<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>F : J ⥤ AddCommGrp<GOAL>CategoryTheory.Limits.HasColimit F
<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<GOAL>CategoryTheory.Limits.HasColimitsOfShape J AddCommGrp
<GOAL>CategoryTheory.Limits.HasColimitsOfSize.{v, u, max (max u v) w, max (max (u + 1) (v + 1)) (w + 1)} AddCommGrp
<VAR>α : Type u<GOAL>↑(AddCommGrp.free.obj α) = FreeAbelianGroup α
<VAR>α β : Type u<VAR>f : α → β<VAR>x : FreeAbelianGroup α<GOAL>(AddCommGrp.free.map f) x = f <$> x
<GOAL>∀ {X Y : MonCat} (f : X ⟶ Y), MonCat.units.map f = Grp.ofHom (Units.map f)
<VAR>R : MonCat<GOAL>MonCat.units.obj R = Grp.of (↑R)ˣ
<GOAL>∀ {X Y : CommMonCat} (f : X ⟶ Y), CommMonCat.units.map f = CommGrp.ofHom (Units.map f)
<VAR>R : CommMonCat<GOAL>CommMonCat.units.obj R = CommGrp.of (↑R)ˣ
<VAR>x y : PUnit.{1}<GOAL>x * y = PUnit.unit
<VAR>x y : PUnit.{1}<GOAL>x + y = PUnit.unit
<VAR>x y : PUnit.{1}<GOAL>x - y = PUnit.unit
<VAR>x y : PUnit.{1}<GOAL>x / y = PUnit.unit
<VAR>x : PUnit.{1}<GOAL>x⁻¹ = PUnit.unit
<VAR>x : PUnit.{1}<GOAL>-x = PUnit.unit
<VAR>x y : PUnit.{u_1 + 1}<GOAL>gcd x y = PUnit.unit
<VAR>x y : PUnit.{u_1 + 1}<GOAL>lcm x y = PUnit.unit
<VAR>x : PUnit.{u_1 + 1}<GOAL>normUnit x = 1
<VAR>R : Type u_3<VAR>y : PUnit.{u_4 + 1}<VAR>r : R<GOAL>r +ᵥ y = PUnit.unit
<VAR>R : Type u_3<VAR>y : PUnit.{u_4 + 1}<VAR>r : R<GOAL>r • y = PUnit.unit
<VAR>ιA : Type u_1<VAR>ιM : Type u_3<VAR>A : ιA → Type u_4<VAR>M : ιM → Type u_5<VAR>VAdd ιA ιM<VAR>GradedMonoid.GSMul A M<VAR>i : ιA<VAR>j : ιM<VAR>a : A i<VAR>b : M j<GOAL>GradedMonoid.mk i a • GradedMonoid.mk j b = GradedMonoid.mk (i +ᵥ j) (GradedMonoid.GSMul.smul a b)
<VAR>ιA : Type u_1<VAR>ιM : Type u_3<VAR>A : ιA → Type u_4<VAR>M : ιM → Type u_5<VAR>AddMonoid ιA<VAR>VAdd ιA ιM<VAR>GradedMonoid.GMonoid A<VAR>self : GradedMonoid.GMulAction A M<VAR>a a' : GradedMonoid A<VAR>b : GradedMonoid M<GOAL>(a * a') • b = a • a' • b
<VAR>ιA : Type u_1<VAR>ιM : Type u_3<VAR>A : ιA → Type u_4<VAR>M : ιM → Type u_5<VAR>AddMonoid ιA<VAR>VAdd ιA ιM<VAR>GradedMonoid.GMonoid A<VAR>self : GradedMonoid.GMulAction A M<VAR>b : GradedMonoid M<GOAL>1 • b = b
<VAR>ιA : Type u_1<VAR>ιB : Type u_2<VAR>S : Type u_5<VAR>R : Type u_6<VAR>N : Type u_7<VAR>M : Type u_8<VAR>SetLike S R<VAR>SetLike N M<VAR>SMul R M<VAR>VAdd ιA ιB<VAR>A : ιA → S<VAR>B : ιB → N<VAR>self : SetLike.GradedSMul A B<VAR>i : ιA<VAR>j : ιB<VAR>ai : R<VAR>bj : M<GOAL>ai ∈ A i → bj ∈ B j → ai • bj ∈ B (i +ᵥ j)
<VAR>ιA : Type u_1<VAR>ιB : Type u_2<VAR>S : Type u_5<VAR>R : Type u_6<VAR>N : Type u_7<VAR>M : Type u_8<VAR>SetLike S R<VAR>SetLike N M<VAR>SMul R M<VAR>VAdd ιA ιB<VAR>A : ιA → S<VAR>B : ιB → N<VAR>SetLike.GradedSMul A B<VAR>i : ιA<VAR>j : ιB<VAR>x : ↥(A i)<VAR>y : ↥(B j)<GOAL>↑(GradedMonoid.GSMul.smul x y) = ↑x • ↑y
<VAR>ιA : Type u_1<VAR>ιB : Type u_2<VAR>S : Type u_4<VAR>R : Type u_5<VAR>N : Type u_6<VAR>M : Type u_7<VAR>SetLike S R<VAR>SetLike N M<VAR>VAdd ιA ιB<VAR>SMul R M<VAR>A : ιA → S<VAR>B : ιB → N<VAR>SetLike.GradedSMul A B<VAR>a : R<VAR>b : M<GOAL>SetLike.Homogeneous A a → SetLike.Homogeneous B b → SetLike.Homogeneous B (a • b)
<VAR>A : Type u<VAR>B : Type v<VAR>AddGroup A<VAR>AddGroup B<VAR>f : A →+ B<VAR>h : ∀ (u v : ↥f.ker →+ A), f.comp u = f.comp v → u = v<GOAL>f.ker = ⊥
<VAR>A : Type u<VAR>B : Type v<VAR>Group A<VAR>Group B<VAR>f : A →* B<VAR>h : ∀ (u v : ↥f.ker →* A), f.comp u = f.comp v → u = v<GOAL>f.ker = ⊥
<VAR>A : Type u<VAR>B : Type v<VAR>AddCommGroup A<VAR>AddCommGroup B<VAR>f : A →+ B<VAR>h : ∀ (u v : B →+ B ⧸ f.range), u.comp f = v.comp f → u = v<GOAL>f.range = ⊤
<VAR>A : Type u<VAR>B : Type v<VAR>CommGroup A<VAR>CommGroup B<VAR>f : A →* B<VAR>h : ∀ (u v : B →* B ⧸ f.range), u.comp f = v.comp f → u = v<GOAL>f.range = ⊤
<VAR>A B : Grp<VAR>f : A ⟶ B<VAR>CategoryTheory.Mono f<GOAL>MonoidHom.ker f = ⊥
<VAR>A B : AddGrp<VAR>f : A ⟶ B<VAR>CategoryTheory.Mono f<GOAL>AddMonoidHom.ker f = ⊥
<VAR>A B : AddGrp<VAR>f : A ⟶ B<GOAL>CategoryTheory.Mono f ↔ AddMonoidHom.ker f = ⊥
<VAR>A B : Grp<VAR>f : A ⟶ B<GOAL>CategoryTheory.Mono f ↔ MonoidHom.ker f = ⊥
<VAR>A B : Grp<VAR>f : A ⟶ B<GOAL>CategoryTheory.Mono f ↔ Function.Injective ⇑f
<VAR>A B : AddGrp<VAR>f : A ⟶ B<GOAL>CategoryTheory.Mono f ↔ Function.Injective ⇑f
<VAR>A B : Grp<VAR>f : A ⟶ B<VAR>b b' : ↑B<VAR>x : Grp.SurjectiveOfEpiAuxs.XWithInfinity f<GOAL>(b * b') • x = b • b' • x
<VAR>A B : Grp<VAR>f : A ⟶ B<VAR>x : Grp.SurjectiveOfEpiAuxs.XWithInfinity f<GOAL>1 • x = x
<VAR>A B : Grp<VAR>f : A ⟶ B<VAR>b : ↑B<VAR>hb : b ∈ MonoidHom.range f<GOAL>Grp.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset ⟨b • ↑(MonoidHom.range f), ⋯⟩ = Grp.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset ⟨↑(MonoidHom.range f), ⋯⟩
<VAR>A B : Grp<VAR>f : A ⟶ B<VAR>b : ↑B<VAR>hb : b ∉ MonoidHom.range f<GOAL>Grp.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset ⟨b • ↑(MonoidHom.range f), ⋯⟩ ≠ Grp.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset ⟨↑(MonoidHom.range f), ⋯⟩
<VAR>A B : Grp<VAR>f : A ⟶ B<GOAL>(Grp.SurjectiveOfEpiAuxs.tau f) Grp.SurjectiveOfEpiAuxs.XWithInfinity.infinity = Grp.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset ⟨↑(MonoidHom.range f), ⋯⟩
<VAR>A B : Grp<VAR>f : A ⟶ B<GOAL>(Grp.SurjectiveOfEpiAuxs.tau f) (Grp.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset ⟨↑(MonoidHom.range f), ⋯⟩) = Grp.SurjectiveOfEpiAuxs.XWithInfinity.infinity
<VAR>A B : Grp<VAR>f : A ⟶ B<VAR>x : ↑B<VAR>hx : x ∈ MonoidHom.range f<GOAL>(Grp.SurjectiveOfEpiAuxs.tau f) (Grp.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset ⟨x • ↑(MonoidHom.range f), ⋯⟩) = Grp.SurjectiveOfEpiAuxs.XWithInfinity.infinity
<VAR>A B : Grp<VAR>f : A ⟶ B<GOAL>(Equiv.symm (Grp.SurjectiveOfEpiAuxs.tau f)) (Grp.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset ⟨↑(MonoidHom.range f), ⋯⟩) = Grp.SurjectiveOfEpiAuxs.XWithInfinity.infinity
<VAR>A B : Grp<VAR>f : A ⟶ B<GOAL>(Equiv.symm (Grp.SurjectiveOfEpiAuxs.tau f)) Grp.SurjectiveOfEpiAuxs.XWithInfinity.infinity = Grp.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset ⟨↑(MonoidHom.range f), ⋯⟩
<VAR>A B : Grp<VAR>f : A ⟶ B<VAR>x : ↑B<VAR>y : ↑(Set.range fun x => x • ↑(MonoidHom.range f))<GOAL>((Grp.SurjectiveOfEpiAuxs.g f) x) (Grp.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset y) = Grp.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset ⟨x • ↑y, ⋯⟩
<VAR>A B : Grp<VAR>f : A ⟶ B<VAR>x : ↑B<GOAL>((Grp.SurjectiveOfEpiAuxs.g f) x) Grp.SurjectiveOfEpiAuxs.XWithInfinity.infinity = Grp.SurjectiveOfEpiAuxs.XWithInfinity.infinity
<VAR>A B : Grp<VAR>f : A ⟶ B<VAR>x : ↑B<VAR>hx : x ∈ MonoidHom.range f<GOAL>((Grp.SurjectiveOfEpiAuxs.h f) x) Grp.SurjectiveOfEpiAuxs.XWithInfinity.infinity = Grp.SurjectiveOfEpiAuxs.XWithInfinity.infinity
<VAR>A B : Grp<VAR>f : A ⟶ B<VAR>x : ↑B<GOAL>((Grp.SurjectiveOfEpiAuxs.h f) x) (Grp.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset ⟨↑(MonoidHom.range f), ⋯⟩) = Grp.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset ⟨↑(MonoidHom.range f), ⋯⟩
<VAR>A B : Grp<VAR>f : A ⟶ B<VAR>x b : ↑B<VAR>hb : b ∈ MonoidHom.range f<GOAL>((Grp.SurjectiveOfEpiAuxs.h f) x) (Grp.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset ⟨b • ↑(MonoidHom.range f), ⋯⟩) = Grp.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset ⟨b • ↑(MonoidHom.range f), ⋯⟩
<VAR>A B : Grp<VAR>f : A ⟶ B<VAR>x : ↑B<VAR>hx : x ∈ MonoidHom.range f<VAR>b : ↑B<VAR>hb : b ∉ MonoidHom.range f<GOAL>((Grp.SurjectiveOfEpiAuxs.h f) x) (Grp.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset ⟨b • ↑(MonoidHom.range f), ⋯⟩) = Grp.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset ⟨(x * b) • ↑(MonoidHom.range f), ⋯⟩
<VAR>A B : Grp<VAR>f : A ⟶ B<GOAL>↑(MonoidHom.range f) = {x | (Grp.SurjectiveOfEpiAuxs.h f) x = (Grp.SurjectiveOfEpiAuxs.g f) x}
<VAR>A B : Grp<VAR>f : A ⟶ B<GOAL>CategoryTheory.CategoryStruct.comp f (let_fun this := Grp.SurjectiveOfEpiAuxs.g f; this) = CategoryTheory.CategoryStruct.comp f (let_fun this := Grp.SurjectiveOfEpiAuxs.h f; this)
<VAR>A B : Grp<VAR>f : A ⟶ B<VAR>x : ↑B<VAR>hx : x ∉ MonoidHom.range f<GOAL>Grp.SurjectiveOfEpiAuxs.g f ≠ Grp.SurjectiveOfEpiAuxs.h f
<VAR>A B : Grp<VAR>f : A ⟶ B<VAR>CategoryTheory.Epi f<GOAL>Function.Surjective ⇑f
<VAR>A B : Grp<VAR>f : A ⟶ B<GOAL>CategoryTheory.Epi f ↔ Function.Surjective ⇑f
<VAR>A B : Grp<VAR>f : A ⟶ B<GOAL>CategoryTheory.Epi f ↔ MonoidHom.range f = ⊤
<VAR>A B : AddGrp<VAR>f : A ⟶ B<GOAL>CategoryTheory.Epi f ↔ Function.Surjective ⇑f
<VAR>A B : AddGrp<VAR>f : A ⟶ B<GOAL>CategoryTheory.Epi f ↔ AddMonoidHom.range f = ⊤
<VAR>A B : AddCommGrp<VAR>f : A ⟶ B<VAR>CategoryTheory.Mono f<GOAL>AddMonoidHom.ker f = ⊥
<VAR>A B : CommGrp<VAR>f : A ⟶ B<VAR>CategoryTheory.Mono f<GOAL>MonoidHom.ker f = ⊥
<VAR>A B : CommGrp<VAR>f : A ⟶ B<GOAL>CategoryTheory.Mono f ↔ MonoidHom.ker f = ⊥
<VAR>A B : AddCommGrp<VAR>f : A ⟶ B<GOAL>CategoryTheory.Mono f ↔ AddMonoidHom.ker f = ⊥
<VAR>A B : CommGrp<VAR>f : A ⟶ B<GOAL>CategoryTheory.Mono f ↔ Function.Injective ⇑f
<VAR>A B : AddCommGrp<VAR>f : A ⟶ B<GOAL>CategoryTheory.Mono f ↔ Function.Injective ⇑f
<VAR>A B : AddCommGrp<VAR>f : A ⟶ B<VAR>CategoryTheory.Epi f<GOAL>AddMonoidHom.range f = ⊤
<VAR>A B : CommGrp<VAR>f : A ⟶ B<VAR>CategoryTheory.Epi f<GOAL>MonoidHom.range f = ⊤
<VAR>A B : CommGrp<VAR>f : A ⟶ B<GOAL>CategoryTheory.Epi f ↔ MonoidHom.range f = ⊤
<VAR>A B : AddCommGrp<VAR>f : A ⟶ B<GOAL>CategoryTheory.Epi f ↔ AddMonoidHom.range f = ⊤
<VAR>A B : AddCommGrp<VAR>f : A ⟶ B<GOAL>CategoryTheory.Epi f ↔ Function.Surjective ⇑f
<VAR>A B : CommGrp<VAR>f : A ⟶ B<GOAL>CategoryTheory.Epi f ↔ Function.Surjective ⇑f
<VAR>R : Type u<VAR>CommSemiring R<VAR>S : Submonoid R<VAR>M : Type v<VAR>AddCommMonoid M<VAR>Module R M<GOAL>IsEquiv (M × ↥S) (LocalizedModule.r S M)
<VAR>R : Type u<VAR>CommSemiring R<VAR>S : Submonoid R<VAR>M : Type v<VAR>AddCommMonoid M<VAR>Module R M<VAR>m m' : M<VAR>s s' : ↥S<GOAL>LocalizedModule.mk m s = LocalizedModule.mk m' s' ↔ ∃ u, u • s' • m = u • s • m'
<VAR>R : Type u<VAR>CommSemiring R<VAR>S : Submonoid R<VAR>M : Type v<VAR>AddCommMonoid M<VAR>Module R M<VAR>β : LocalizedModule S M → Prop<VAR>h : ∀ (m : M) (s : ↥S), β (LocalizedModule.mk m s)<VAR>x : LocalizedModule S M<GOAL>β x
<VAR>R : Type u<VAR>CommSemiring R<VAR>S : Submonoid R<VAR>M : Type v<VAR>AddCommMonoid M<VAR>Module R M<VAR>β : LocalizedModule S M → LocalizedModule S M → Prop<VAR>h : ∀ (m m' : M) (s s' : ↥S), β (LocalizedModule.mk m s) (LocalizedModule.mk m' s')<VAR>x y : LocalizedModule S M<GOAL>β x y
<VAR>R : Type u<VAR>CommSemiring R<VAR>S : Submonoid R<VAR>M : Type v<VAR>AddCommMonoid M<VAR>Module R M<VAR>α : Type u_2<VAR>f : M × ↥S → α<VAR>wd : ∀ (p p' : M × ↥S), p ≈ p' → f p = f p'<VAR>m : M<VAR>s : ↥S<GOAL>(LocalizedModule.mk m s).liftOn f wd = f (m, s)
<VAR>R : Type u<VAR>CommSemiring R<VAR>S : Submonoid R<VAR>M : Type v<VAR>AddCommMonoid M<VAR>Module R M<VAR>α : Type u_2<VAR>f : M × ↥S → M × ↥S → α<VAR>wd : ∀ (p q p' q' : M × ↥S), p ≈ p' → q ≈ q' → f p q = f p' q'<VAR>m m' : M<VAR>s s' : ↥S<GOAL>(LocalizedModule.mk m s).liftOn₂ (LocalizedModule.mk m' s') f wd = f (m, s) (m', s')
<VAR>R : Type u<VAR>CommSemiring R<VAR>S : Submonoid R<VAR>M : Type v<VAR>AddCommMonoid M<VAR>Module R M<VAR>h : 0 ∈ S<GOAL>Subsingleton (LocalizedModule S M)
<VAR>R : Type u<VAR>CommSemiring R<VAR>S : Submonoid R<VAR>M : Type v<VAR>AddCommMonoid M<VAR>Module R M<VAR>s : ↥S<GOAL>LocalizedModule.mk 0 s = 0
<VAR>R : Type u<VAR>CommSemiring R<VAR>S : Submonoid R<VAR>M : Type v<VAR>AddCommMonoid M<VAR>Module R M<VAR>m1 m2 : M<VAR>s1 s2 : ↥S<GOAL>LocalizedModule.mk m1 s1 + LocalizedModule.mk m2 s2 = LocalizedModule.mk (s2 • m1 + s1 • m2) (s1 * s2)
<VAR>R : Type u<VAR>CommSemiring R<VAR>S : Submonoid R<VAR>M : Type v<VAR>AddCommMonoid M<VAR>Module R M<VAR>x y z : LocalizedModule S M<GOAL>x + y + z = x + (y + z)
<VAR>R : Type u<VAR>CommSemiring R<VAR>S : Submonoid R<VAR>M : Type v<VAR>AddCommMonoid M<VAR>Module R M<VAR>x y : LocalizedModule S M<GOAL>x + y = y + x
<VAR>R : Type u<VAR>CommSemiring R<VAR>S : Submonoid R<VAR>M : Type v<VAR>AddCommMonoid M<VAR>Module R M<VAR>x : LocalizedModule S M<GOAL>0 + x = x
<VAR>R : Type u<VAR>CommSemiring R<VAR>S : Submonoid R<VAR>M : Type v<VAR>AddCommMonoid M<VAR>Module R M<VAR>x : LocalizedModule S M<GOAL>x + 0 = x
<VAR>R : Type u<VAR>CommSemiring R<VAR>S : Submonoid R<VAR>M : Type v<VAR>AddCommMonoid M<VAR>Module R M<VAR>x : LocalizedModule S M<GOAL>0 • x = 0
<VAR>R : Type u<VAR>CommSemiring R<VAR>S : Submonoid R<VAR>M : Type v<VAR>AddCommMonoid M<VAR>Module R M<VAR>n : ℕ<VAR>x : LocalizedModule S M<GOAL>n.succ • x = n • x + x
<VAR>R : Type u<VAR>CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>m : M<VAR>s : ↥S<GOAL>LocalizedModule.mk (-m) s = -LocalizedModule.mk m s
<VAR>R : Type u<VAR>CommSemiring R<VAR>S : Submonoid R<VAR>A : Type u_2<VAR>Semiring A<VAR>Algebra R A<VAR>a₁ a₂ : A<VAR>s₁ s₂ : ↥S<GOAL>LocalizedModule.mk a₁ s₁ * LocalizedModule.mk a₂ s₂ = LocalizedModule.mk (a₁ * a₂) (s₁ * s₂)
<VAR>R : Type u<VAR>CommSemiring R<VAR>S : Submonoid R<VAR>M : Type v<VAR>AddCommMonoid M<VAR>Module R M<VAR>T : Type u_1<VAR>CommSemiring T<VAR>Algebra R T<VAR>IsLocalization S T<VAR>x : T<VAR>m : M<VAR>s : ↥S<GOAL>x • LocalizedModule.mk m s = LocalizedModule.mk ((IsLocalization.sec S x).1 • m) ((IsLocalization.sec S x).2 * s)
<VAR>R : Type u<VAR>CommSemiring R<VAR>S : Submonoid R<VAR>M : Type v<VAR>AddCommMonoid M<VAR>Module R M<VAR>T : Type u_1<VAR>CommSemiring T<VAR>Algebra R T<VAR>IsLocalization S T<VAR>r : R<VAR>m : M<VAR>s s' : ↥S<GOAL>IsLocalization.mk' T r s • LocalizedModule.mk m s' = LocalizedModule.mk (r • m) (s * s')
<VAR>R : Type u<VAR>CommSemiring R<VAR>S : Submonoid R<VAR>M : Type v<VAR>AddCommMonoid M<VAR>Module R M<VAR>r : R<VAR>m : M<VAR>s t : ↥S<GOAL>Localization.mk r s • LocalizedModule.mk m t = LocalizedModule.mk (r • m) (s * t)
<VAR>R : Type u<VAR>CommSemiring R<VAR>S : Submonoid R<VAR>M : Type v<VAR>AddCommMonoid M<VAR>Module R M<VAR>T : Type u_1<VAR>CommSemiring T<VAR>Algebra R T<VAR>IsLocalization S T<VAR>p : LocalizedModule S M<GOAL>1 • p = p
<VAR>R : Type u<VAR>CommSemiring R<VAR>S : Submonoid R<VAR>M : Type v<VAR>AddCommMonoid M<VAR>Module R M<VAR>T : Type u_1<VAR>CommSemiring T<VAR>Algebra R T<VAR>IsLocalization S T<VAR>x y : T<VAR>p : LocalizedModule S M<GOAL>(x * y) • p = x • y • p
<VAR>R : Type u<VAR>CommSemiring R<VAR>S : Submonoid R<VAR>M : Type v<VAR>AddCommMonoid M<VAR>Module R M<VAR>T : Type u_1<VAR>CommSemiring T<VAR>Algebra R T<VAR>IsLocalization S T<VAR>x : T<VAR>p q : LocalizedModule S M<GOAL>x • (p + q) = x • p + x • q
<VAR>R : Type u<VAR>CommSemiring R<VAR>S : Submonoid R<VAR>M : Type v<VAR>AddCommMonoid M<VAR>Module R M<VAR>T : Type u_1<VAR>CommSemiring T<VAR>Algebra R T<VAR>IsLocalization S T<VAR>x : T<GOAL>x • 0 = 0
<VAR>R : Type u<VAR>CommSemiring R<VAR>S : Submonoid R<VAR>M : Type v<VAR>AddCommMonoid M<VAR>Module R M<VAR>T : Type u_1<VAR>CommSemiring T<VAR>Algebra R T<VAR>IsLocalization S T<VAR>x y : T<VAR>p : LocalizedModule S M<GOAL>(x + y) • p = x • p + y • p
<VAR>R : Type u<VAR>CommSemiring R<VAR>S : Submonoid R<VAR>M : Type v<VAR>AddCommMonoid M<VAR>Module R M<VAR>T : Type u_1<VAR>CommSemiring T<VAR>Algebra R T<VAR>IsLocalization S T<VAR>p : LocalizedModule S M<GOAL>0 • p = 0
<VAR>R : Type u<VAR>CommSemiring R<VAR>S : Submonoid R<VAR>M : Type v<VAR>AddCommMonoid M<VAR>Module R M<VAR>s' s : ↥S<VAR>m : M<GOAL>LocalizedModule.mk (s' • m) (s' * s) = LocalizedModule.mk m s
<VAR>R : Type u<VAR>CommSemiring R<VAR>S : Submonoid R<VAR>M : Type v<VAR>AddCommMonoid M<VAR>Module R M<VAR>s : ↥S<VAR>m : M<GOAL>LocalizedModule.mk (s • m) s = LocalizedModule.mk m 1
<VAR>R : Type u<VAR>CommSemiring R<VAR>S : Submonoid R<VAR>M : Type v<VAR>AddCommMonoid M<VAR>Module R M<VAR>s s' : ↥S<VAR>m : M<GOAL>LocalizedModule.mk (s' • m) (s * s') = LocalizedModule.mk m s
<VAR>R : Type u<VAR>CommSemiring R<VAR>S : Submonoid R<VAR>M : Type v<VAR>AddCommMonoid M<VAR>Module R M<VAR>r : R<VAR>s : ↥S<VAR>m : M<GOAL>r • LocalizedModule.mk m s = LocalizedModule.mk (r • m) s
<VAR>R : Type u<VAR>CommSemiring R<VAR>S : Submonoid R<VAR>T : Type u_1<VAR>CommSemiring T<VAR>Algebra R T<VAR>IsLocalization S T<VAR>A : Type u_2<VAR>Semiring A<VAR>Algebra R A<VAR>x : T<VAR>p₁ p₂ : LocalizedModule S A<GOAL>x • p₁ * p₂ = x • (p₁ * p₂)
<VAR>R : Type u<VAR>CommSemiring R<VAR>S : Submonoid R<VAR>T : Type u_1<VAR>CommSemiring T<VAR>Algebra R T<VAR>IsLocalization S T<VAR>A : Type u_2<VAR>Semiring A<VAR>Algebra R A<VAR>x : T<VAR>p₁ p₂ : LocalizedModule S A<GOAL>p₁ * x • p₂ = x • (p₁ * p₂)
<VAR>R : Type u<VAR>CommSemiring R<VAR>S : Submonoid R<VAR>T : Type u_1<VAR>CommSemiring T<VAR>Algebra R T<VAR>IsLocalization S T<VAR>A : Type u_2<VAR>Semiring A<VAR>Algebra R A<VAR>a : R<VAR>s : ↥S<GOAL>(algebraMap T (LocalizedModule S A)) (IsLocalization.mk' T a s) = LocalizedModule.mk ((algebraMap R A) a) s
<VAR>R : Type u<VAR>CommSemiring R<VAR>S : Submonoid R<VAR>A : Type u_2<VAR>Semiring A<VAR>Algebra R A<VAR>a : R<VAR>s : ↥S<GOAL>(algebraMap (Localization S) (LocalizedModule S A)) (Localization.mk a s) = LocalizedModule.mk ((algebraMap R A) a) s
<VAR>R : Type u<VAR>CommSemiring R<VAR>S : Submonoid R<VAR>M : Type v<VAR>AddCommMonoid M<VAR>Module R M<VAR>m : M<GOAL>(LocalizedModule.mkLinearMap S M) m = LocalizedModule.mk m 1
<VAR>R : Type u<VAR>CommSemiring R<VAR>S : Submonoid R<VAR>M : Type v<VAR>AddCommMonoid M<VAR>Module R M<VAR>s : ↥S<VAR>p : LocalizedModule S M<GOAL>(LocalizedModule.divBy s) p = p.liftOn (fun p => LocalizedModule.mk p.1 (p.2 * s)) ⋯
<VAR>R : Type u<VAR>CommSemiring R<VAR>S : Submonoid R<VAR>M : Type v<VAR>AddCommMonoid M<VAR>Module R M<VAR>s : ↥S<VAR>p : LocalizedModule S M<GOAL>(LocalizedModule.divBy s) (((algebraMap R (Module.End R (LocalizedModule S M))) ↑s) p) = p
<VAR>R : Type u<VAR>CommSemiring R<VAR>S : Submonoid R<VAR>M : Type v<VAR>AddCommMonoid M<VAR>Module R M<VAR>s : ↥S<VAR>p : LocalizedModule S M<GOAL>((algebraMap R (Module.End R (LocalizedModule S M))) ↑s) ((LocalizedModule.divBy s) p) = p
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>AddCommMonoid M<VAR>AddCommMonoid M'<VAR>Module R M<VAR>Module R M'<VAR>f : M →ₗ[R] M'<GOAL>IsLocalizedModule S f ↔ (∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M')) ↑x)) ∧ (∀ (y : M'), ∃ x, x.2 • y = f x.1) ∧ ∀ {x₁ x₂ : M}, f x₁ = f x₂ → ∃ c, c • x₁ = c • x₂
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>AddCommMonoid M<VAR>AddCommMonoid M'<VAR>Module R M<VAR>Module R M'<VAR>f : M →ₗ[R] M'<VAR>self : IsLocalizedModule S f<VAR>y : M'<GOAL>∃ x, x.2 • y = f x.1
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>AddCommMonoid M<VAR>AddCommMonoid M'<VAR>Module R M<VAR>Module R M'<VAR>f : M →ₗ[R] M'<VAR>self : IsLocalizedModule S f<VAR>x : ↥S<GOAL>IsUnit ((algebraMap R (Module.End R M')) ↑x)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>AddCommMonoid M<VAR>AddCommMonoid M'<VAR>Module R M<VAR>Module R M'<VAR>f : M →ₗ[R] M'<VAR>self : IsLocalizedModule S f<VAR>x₁ x₂ : M<GOAL>f x₁ = f x₂ → ∃ c, c • x₁ = c • x₂
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>AddCommMonoid M<VAR>AddCommMonoid M'<VAR>Module R M<VAR>Module R M'<VAR>f : M →ₗ[R] M'<VAR>IsLocalizedModule S f<VAR>y : M'<GOAL>∃ x, x.2 • y = f x.1
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>AddCommMonoid M<VAR>AddCommMonoid M'<VAR>Module R M<VAR>Module R M'<VAR>f : M →ₗ[R] M'<VAR>IsLocalizedModule S f<VAR>x₁ x₂ : M<GOAL>f x₁ = f x₂ ↔ ∃ c, c • x₁ = c • x₂
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>AddCommMonoid M<VAR>AddCommMonoid M'<VAR>AddCommMonoid M''<VAR>Module R M<VAR>Module R M'<VAR>Module R M''<VAR>f : M →ₗ[R] M'<VAR>e : M' ≃ₗ[R] M''<VAR>hf : IsLocalizedModule S f<GOAL>IsLocalizedModule S (↑e ∘ₗ f)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>R' : Type u_6<VAR>CommSemiring R'<VAR>Algebra R R'<VAR>IsLocalization S R'<VAR>Module R' M<VAR>IsScalarTower R R' M<GOAL>IsLocalizedModule S LinearMap.id
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>S : Submonoid R<VAR>A : Type u_6<VAR>Aₛ : Type u_7<VAR>CommSemiring A<VAR>Algebra R A<VAR>CommSemiring Aₛ<VAR>Algebra A Aₛ<VAR>Algebra R Aₛ<VAR>IsScalarTower R A Aₛ<GOAL>IsLocalizedModule S (IsScalarTower.toAlgHom R A Aₛ).toLinearMap ↔ IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>S : Submonoid R<VAR>R' : Type u_6<VAR>CommSemiring R'<VAR>Algebra R R'<GOAL>IsLocalizedModule S (Algebra.ofId R R').toLinearMap ↔ IsLocalization S R'
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M'' : Type u_4<VAR>AddCommMonoid M<VAR>AddCommMonoid M''<VAR>Module R M<VAR>Module R M''<VAR>g : M →ₗ[R] M''<VAR>h : ∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M'')) ↑x)<VAR>m : M<VAR>s : ↥S<GOAL>LocalizedModule.lift' S g h (LocalizedModule.mk m s) = ↑⋯.unit⁻¹ (g m)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M'' : Type u_4<VAR>AddCommMonoid M<VAR>AddCommMonoid M''<VAR>Module R M<VAR>Module R M''<VAR>g : M →ₗ[R] M''<VAR>h : ∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M'')) ↑x)<VAR>x y : LocalizedModule S M<GOAL>LocalizedModule.lift' S g h (x + y) = LocalizedModule.lift' S g h x + LocalizedModule.lift' S g h y
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M'' : Type u_4<VAR>AddCommMonoid M<VAR>AddCommMonoid M''<VAR>Module R M<VAR>Module R M''<VAR>g : M →ₗ[R] M''<VAR>h : ∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M'')) ↑x)<VAR>r : R<VAR>m : LocalizedModule S M<GOAL>r • LocalizedModule.lift' S g h m = LocalizedModule.lift' S g h (r • m)