ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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)<GOAL>LocalizedModule.lift S g h ∘ₗ LocalizedModule.mkLinearMap S M = g
<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>l : LocalizedModule S M →ₗ[R] M''<VAR>hl : l ∘ₗ LocalizedModule.mkLinearMap S M = g<GOAL>LocalizedModule.lift S g h = l
<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>m : M<VAR>s : ↥S<GOAL>IsLocalizedModule.fromLocalizedModule' S f (LocalizedModule.mk m s) = ↑⋯.unit⁻¹ (f m)
<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 y : LocalizedModule S M<GOAL>IsLocalizedModule.fromLocalizedModule' S f (x + y) = IsLocalizedModule.fromLocalizedModule' S f x + IsLocalizedModule.fromLocalizedModule' S f y
<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>r : R<VAR>x : LocalizedModule S M<GOAL>r • IsLocalizedModule.fromLocalizedModule' S f x = IsLocalizedModule.fromLocalizedModule' S f (r • 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>m : M<VAR>s : ↥S<GOAL>(IsLocalizedModule.fromLocalizedModule S f) (LocalizedModule.mk m s) = ↑⋯.unit⁻¹ (f m)
<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<GOAL>Function.Injective ⇑(IsLocalizedModule.fromLocalizedModule S f)
<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<GOAL>Function.Surjective ⇑(IsLocalizedModule.fromLocalizedModule S f)
<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<GOAL>Function.Bijective ⇑(IsLocalizedModule.fromLocalizedModule S f)
<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<GOAL>∀ (a : LocalizedModule S M), (IsLocalizedModule.iso S f) a = IsLocalizedModule.fromLocalizedModule' S f a
<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<GOAL>∀ (a : M'), (IsLocalizedModule.iso S f).symm a = (Equiv.ofBijective ⇑(IsLocalizedModule.fromLocalizedModule S f) ⋯).symm a
<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>m : M<VAR>s : ↥S<GOAL>(IsLocalizedModule.iso S f) (LocalizedModule.mk m s) = ↑⋯.unit⁻¹ (f m)
<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>m : M'<GOAL>(IsLocalizedModule.iso S f).symm m = LocalizedModule.mk ⋯.choose.1 ⋯.choose.2
<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>m : M'<VAR>a : M<VAR>b : ↥S<VAR>eq1 : b • m = f a<GOAL>(IsLocalizedModule.iso S f).symm m = LocalizedModule.mk a b
<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<GOAL>↑(IsLocalizedModule.iso S f).symm ∘ₗ f = LocalizedModule.mkLinearMap S M
<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>IsLocalizedModule S f<VAR>g : M →ₗ[R] M''<VAR>h : ∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M'')) ↑x)<GOAL>IsLocalizedModule.lift S f g h ∘ₗ f = g
<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>IsLocalizedModule S f<VAR>g : M →ₗ[R] M''<VAR>h : ∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M'')) ↑x)<VAR>x : M<GOAL>(IsLocalizedModule.lift S f g h) (f x) = g 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>IsLocalizedModule S f<VAR>g : M →ₗ[R] M''<VAR>h : ∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M'')) ↑x)<VAR>l : M' →ₗ[R] M''<VAR>hl : l ∘ₗ f = g<GOAL>IsLocalizedModule.lift S f g h = l
<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>IsLocalizedModule S f<VAR>g : M →ₗ[R] M''<GOAL>(∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M'')) ↑x)) → ∃! l, l ∘ₗ f = g
<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>IsLocalizedModule S f<VAR>map_unit : ∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M'')) ↑x)<VAR>j k : M' →ₗ[R] M''<VAR>h : j ∘ₗ f = k ∘ₗ f<GOAL>j = k
<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>s : ↥S<GOAL>Function.Injective fun m => s • m
<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>s : ↥S<VAR>m₁ m₂ : M'<GOAL>s • m₁ = s • m₂ ↔ m₁ = m₂
<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>r : R<VAR>m : M<VAR>s : ↥S<GOAL>IsLocalizedModule.mk' f (r • m) s = r • IsLocalizedModule.mk' f m s
<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>m₁ m₂ : M<VAR>s₁ s₂ : ↥S<GOAL>IsLocalizedModule.mk' f m₁ s₁ + IsLocalizedModule.mk' f m₂ s₂ = IsLocalizedModule.mk' f (s₂ • m₁ + s₁ • m₂) (s₁ * s₂)
<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>s : ↥S<GOAL>IsLocalizedModule.mk' f 0 s = 0
<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>m : M<GOAL>IsLocalizedModule.mk' f m 1 = f m
<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>m : M<VAR>s : ↥S<GOAL>IsLocalizedModule.mk' f (s • m) s = f m
<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>m : M<VAR>s : ↥S<GOAL>s • IsLocalizedModule.mk' f m s = f m
<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>m : M<VAR>s₁ s₂ : ↥S<GOAL>IsLocalizedModule.mk' f (s₁ • m) (s₁ * s₂) = IsLocalizedModule.mk' f m s₂
<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>m : M<VAR>s₁ s₂ : ↥S<GOAL>IsLocalizedModule.mk' f (s₂ • m) (s₁ * s₂) = IsLocalizedModule.mk' f m s₁
<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>m₁ m₂ : M<VAR>s : ↥S<GOAL>IsLocalizedModule.mk' f (m₁ + m₂) s = IsLocalizedModule.mk' f m₁ s + IsLocalizedModule.mk' f m₂ s
<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>m₁ m₂ : M<VAR>s₁ s₂ : ↥S<GOAL>IsLocalizedModule.mk' f m₁ s₁ = IsLocalizedModule.mk' f m₂ s₂ ↔ ∃ s, s • s₁ • m₂ = s • s₂ • m₁
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>AddCommGroup M<VAR>AddCommGroup M'<VAR>Module R M<VAR>Module R M'<VAR>f : M →ₗ[R] M'<VAR>IsLocalizedModule S f<VAR>m : M<VAR>s : ↥S<GOAL>IsLocalizedModule.mk' f (-m) s = -IsLocalizedModule.mk' f m s
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>AddCommGroup M<VAR>AddCommGroup M'<VAR>Module R M<VAR>Module R M'<VAR>f : M →ₗ[R] M'<VAR>IsLocalizedModule S f<VAR>m₁ m₂ : M<VAR>s : ↥S<GOAL>IsLocalizedModule.mk' f (m₁ - m₂) s = IsLocalizedModule.mk' f m₁ s - IsLocalizedModule.mk' f m₂ s
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>AddCommGroup M<VAR>AddCommGroup M'<VAR>Module R M<VAR>Module R M'<VAR>f : M →ₗ[R] M'<VAR>IsLocalizedModule S f<VAR>m₁ m₂ : M<VAR>s₁ s₂ : ↥S<GOAL>IsLocalizedModule.mk' f m₁ s₁ - IsLocalizedModule.mk' f m₂ s₂ = IsLocalizedModule.mk' f (s₂ • m₁ - s₁ • m₂) (s₁ * s₂)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>Semiring M<VAR>Semiring M'<VAR>Module R M<VAR>Algebra R M'<VAR>f : M →ₗ[R] M'<VAR>hf : ∀ (m₁ m₂ : M), f (m₁ * m₂) = f m₁ * f m₂<VAR>IsLocalizedModule S f<VAR>m₁ m₂ : M<VAR>s₁ s₂ : ↥S<GOAL>IsLocalizedModule.mk' f m₁ s₁ * IsLocalizedModule.mk' f m₂ s₂ = IsLocalizedModule.mk' f (m₁ * m₂) (s₁ * s₂)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>Semiring M<VAR>Semiring M'<VAR>Algebra R M<VAR>Algebra R M'<VAR>f : M →ₐ[R] M'<VAR>IsLocalizedModule S f.toLinearMap<VAR>m₁ m₂ : M<VAR>s₁ s₂ : ↥S<GOAL>IsLocalizedModule.mk' f.toLinearMap m₁ s₁ * IsLocalizedModule.mk' f.toLinearMap m₂ s₂ = IsLocalizedModule.mk' f.toLinearMap (m₁ * m₂) (s₁ * s₂)
<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>m : M<VAR>s : ↥S<VAR>m' : M'<GOAL>IsLocalizedModule.mk' f m s = m' ↔ f m = s • m'
<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>m : M<VAR>s : ↥S<GOAL>IsLocalizedModule.mk' f m s = 0 ↔ f m = 0
<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>m : M<VAR>s : ↥S<GOAL>IsLocalizedModule.mk' f m s = 0 ↔ ∃ s', s' • m = 0
<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>s : ↥S<VAR>m : M<GOAL>LocalizedModule.mk m s = IsLocalizedModule.mk' (LocalizedModule.mkLinearMap S M) m s
<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>A : Type u_5<VAR>CommSemiring A<VAR>Algebra R A<VAR>Module A M'<VAR>IsLocalization S A<VAR>Module R M<VAR>Module R M'<VAR>IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>IsLocalizedModule S f<VAR>x : R<VAR>m : M<VAR>s t : ↥S<GOAL>IsLocalization.mk' A x s • IsLocalizedModule.mk' f m t = IsLocalizedModule.mk' f (x • m) (s * t)
<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>m : M<GOAL>f m = 0 ↔ ∃ s', s' • m = 0
<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<GOAL>Function.Surjective (Function.uncurry (IsLocalizedModule.mk' f))
<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>N : Type u_6<VAR>N' : Type u_7<VAR>AddCommGroup N<VAR>AddCommGroup N'<VAR>Module R N<VAR>Module R N'<VAR>g : N →ₗ[R] N'<VAR>IsLocalizedModule S g<VAR>h : M →ₗ[R] N<GOAL>(IsLocalizedModule.map S f g) h ∘ₗ f = g ∘ₗ h
<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>N : Type u_6<VAR>N' : Type u_7<VAR>AddCommGroup N<VAR>AddCommGroup N'<VAR>Module R N<VAR>Module R N'<VAR>g : N →ₗ[R] N'<VAR>IsLocalizedModule S g<VAR>h : M →ₗ[R] N<VAR>x : M<GOAL>((IsLocalizedModule.map S f g) h) (f x) = g (h 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>N : Type u_6<VAR>N' : Type u_7<VAR>AddCommGroup N<VAR>AddCommGroup N'<VAR>Module R N<VAR>Module R N'<VAR>g : N →ₗ[R] N'<VAR>IsLocalizedModule S g<VAR>h : M →ₗ[R] N<VAR>x : M<VAR>s : ↥S<GOAL>((IsLocalizedModule.map S f g) h) (IsLocalizedModule.mk' f x s) = IsLocalizedModule.mk' g (h x) s
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<GOAL>IsLocalizedModule.iso S (LocalizedModule.mkLinearMap S M) = LinearEquiv.refl R (LocalizedModule S M)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>S : Submonoid R<VAR>M₀ : Type u_6<VAR>AddCommGroup M₀<VAR>Module R M₀<VAR>M₁ : Type u_7<VAR>AddCommGroup M₁<VAR>Module R M₁<VAR>g : M₀ →ₗ[R] M₁<VAR>m : M₀<VAR>s : ↥S<GOAL>((IsLocalizedModule.map S (LocalizedModule.mkLinearMap S M₀) (LocalizedModule.mkLinearMap S M₁)) g) (LocalizedModule.mk m s) = LocalizedModule.mk (g m) s
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>S : Submonoid R<VAR>M₀ : Type u_6<VAR>M₀' : Type u_9<VAR>AddCommGroup M₀<VAR>AddCommGroup M₀'<VAR>Module R M₀<VAR>Module R M₀'<VAR>f₀ : M₀ →ₗ[R] M₀'<VAR>IsLocalizedModule S f₀<VAR>M₁ : Type u_7<VAR>M₁' : Type u_8<VAR>AddCommGroup M₁<VAR>AddCommGroup M₁'<VAR>Module R M₁<VAR>Module R M₁'<VAR>f₁ : M₁ →ₗ[R] M₁'<VAR>IsLocalizedModule S f₁<VAR>g : M₀ →ₗ[R] M₁<GOAL>(IsLocalizedModule.map S f₀ f₁) g ∘ₗ ↑(IsLocalizedModule.iso S f₀) = ↑(IsLocalizedModule.iso S f₁) ∘ₗ (IsLocalizedModule.map S (LocalizedModule.mkLinearMap S M₀) (LocalizedModule.mkLinearMap S M₁)) g
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>S : Submonoid R<VAR>M₀ : Type u_6<VAR>AddCommGroup M₀<VAR>Module R M₀<VAR>M₁ : Type u_7<VAR>AddCommGroup M₁<VAR>Module R M₁<VAR>M₂ : Type u_8<VAR>AddCommGroup M₂<VAR>Module R M₂<VAR>g : M₀ →ₗ[R] M₁<VAR>h : M₁ →ₗ[R] M₂<VAR>ex : Function.Exact ⇑g ⇑h<GOAL>Function.Exact ⇑((IsLocalizedModule.map S (LocalizedModule.mkLinearMap S M₀) (LocalizedModule.mkLinearMap S M₁)) g) ⇑((IsLocalizedModule.map S (LocalizedModule.mkLinearMap S M₁) (LocalizedModule.mkLinearMap S M₂)) h)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>S : Submonoid R<VAR>M₀ : Type u_6<VAR>M₀' : Type u_9<VAR>AddCommGroup M₀<VAR>AddCommGroup M₀'<VAR>Module R M₀<VAR>Module R M₀'<VAR>f₀ : M₀ →ₗ[R] M₀'<VAR>IsLocalizedModule S f₀<VAR>M₁ : Type u_7<VAR>M₁' : Type u_10<VAR>AddCommGroup M₁<VAR>AddCommGroup M₁'<VAR>Module R M₁<VAR>Module R M₁'<VAR>f₁ : M₁ →ₗ[R] M₁'<VAR>IsLocalizedModule S f₁<VAR>M₂ : Type u_8<VAR>M₂' : Type u_11<VAR>AddCommGroup M₂<VAR>AddCommGroup M₂'<VAR>Module R M₂<VAR>Module R M₂'<VAR>f₂ : M₂ →ₗ[R] M₂'<VAR>IsLocalizedModule S f₂<VAR>g : M₀ →ₗ[R] M₁<VAR>h : M₁ →ₗ[R] M₂<VAR>ex : Function.Exact ⇑g ⇑h<GOAL>Function.Exact ⇑((IsLocalizedModule.map S f₀ f₁) g) ⇑((IsLocalizedModule.map S f₁ f₂) h)
<VAR>R : Type u_6<VAR>S : Type u_7<VAR>S' : Type u_8<VAR>CommRing R<VAR>CommRing S<VAR>CommRing S'<VAR>Algebra R S<VAR>Algebra R S'<VAR>M : Submonoid R<VAR>f : S →ₐ[R] S'<VAR>h₁ : ∀ x ∈ M, IsUnit ((algebraMap R S') x)<VAR>h₂ : ∀ (y : S'), ∃ x, x.2 • y = f x.1<VAR>h₃ : ∀ (x : S), f x = 0 → ∃ m, m • x = 0<GOAL>IsLocalizedModule M f.toLinearMap
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>S : Submonoid R<VAR>m : M<GOAL>m ∈ LinearMap.ker (LocalizedModule.mkLinearMap S M) ↔ ∃ r ∈ S, r • m = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>S : Submonoid R<GOAL>Subsingleton (LocalizedModule S M) ↔ LinearMap.ker (LocalizedModule.mkLinearMap S M) = ⊤
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>S : Submonoid R<GOAL>Subsingleton (LocalizedModule S M) ↔ ∀ (m : M), ∃ r ∈ S, r • m = 0
<VAR>R : Type u<VAR>CommRing R<GOAL>(AlgebraCat.toModuleCatBraidedFunctor R).toMonoidalFunctor = AlgebraCat.toModuleCatMonoidalFunctor R
<VAR>R A B : Type u<VAR>CommRing R<VAR>CommRing A<VAR>CommRing B<VAR>Algebra R A<VAR>Algebra R B<GOAL>(CommRingCat.pushoutCocone R A B).inl = Algebra.TensorProduct.includeLeftRingHom
<VAR>R A B : Type u<VAR>CommRing R<VAR>CommRing A<VAR>CommRing B<VAR>Algebra R A<VAR>Algebra R B<GOAL>(CommRingCat.pushoutCocone R A B).inr = Algebra.TensorProduct.includeRight.toRingHom
<VAR>R A B : Type u<VAR>CommRing R<VAR>CommRing A<VAR>CommRing B<VAR>Algebra R A<VAR>Algebra R B<GOAL>(CommRingCat.pushoutCocone R A B).pt = CommRingCat.of (A ⊗[R] B)
<VAR>X : CommRingCat<VAR>hX : CategoryTheory.Limits.IsTerminal X<GOAL>Subsingleton ↑X
<VAR>A B : CommRingCat<GOAL>(A.prodFan B).pt = CommRingCat.of (↑A × ↑B)
<VAR>ι : Type u<VAR>R : ι → CommRingCat<GOAL>(CommRingCat.piFan R).pt = CommRingCat.of ((i : ι) → ↑(R i))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>self : PresheafOfModules R<VAR>X Y : Cᵒᵖ<VAR>f : X ⟶ Y<VAR>r : ↑(R.obj X)<VAR>x : ↑(self.presheaf.obj X)<GOAL>(self.presheaf.map f) (r • x) = (R.map f) r • (self.presheaf.map f) x
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>P : PresheafOfModules R<VAR>X Y : Cᵒᵖ<VAR>f : X ⟶ Y<VAR>x : ↑(P.obj X)<GOAL>(P.map f) x = (P.presheaf.map f) x
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>P : PresheafOfModules R<VAR>X : Cᵒᵖ<GOAL>P.map (𝟙 X) = LinearMap.id'
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>P : PresheafOfModules R<VAR>X Y Z : Cᵒᵖ<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>P.map (f ≫ g) = (P.map g).comp (P.map f)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>P Q : PresheafOfModules R<VAR>self : P.Hom Q<VAR>X : Cᵒᵖ<VAR>r : ↑(R.obj X)<VAR>x : ↑(P.presheaf.obj X)<GOAL>(self.hom.app X) (r • x) = r • (self.hom.app X) x
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>P : PresheafOfModules R<GOAL>(𝟙 P).hom = 𝟙 P.presheaf
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>P Q T : PresheafOfModules R<VAR>f : P ⟶ Q<VAR>g : Q ⟶ T<GOAL>(f ≫ g).hom = f.hom ≫ g.hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>P Q T : PresheafOfModules R<VAR>f : P ⟶ Q<VAR>g : Q ⟶ T<VAR>X : Cᵒᵖ<GOAL>PresheafOfModules.Hom.app (f ≫ g) X = PresheafOfModules.Hom.app g X ∘ₗ PresheafOfModules.Hom.app f X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>P Q : PresheafOfModules R<VAR>f g : P ⟶ Q<VAR>w : ∀ (X : Cᵒᵖ), PresheafOfModules.Hom.app f X = PresheafOfModules.Hom.app g X<GOAL>f = g
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>P Q : PresheafOfModules R<VAR>X : Cᵒᵖ<GOAL>PresheafOfModules.Hom.app 0 X = 0
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>P Q : PresheafOfModules R<VAR>f g : P ⟶ Q<VAR>X : Cᵒᵖ<GOAL>PresheafOfModules.Hom.app (f + g) X = PresheafOfModules.Hom.app f X + PresheafOfModules.Hom.app g X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>P Q : PresheafOfModules R<VAR>f g : P ⟶ Q<VAR>X : Cᵒᵖ<GOAL>PresheafOfModules.Hom.app (f - g) X = PresheafOfModules.Hom.app f X - PresheafOfModules.Hom.app g X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>P Q : PresheafOfModules R<VAR>f : P ⟶ Q<VAR>X : Cᵒᵖ<GOAL>PresheafOfModules.Hom.app (-f) X = -PresheafOfModules.Hom.app f X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>P Q : PresheafOfModules R<VAR>f : P ⟶ Q<VAR>X Y : Cᵒᵖ<VAR>g : X ⟶ Y<VAR>x : ↑(P.obj X)<GOAL>(PresheafOfModules.Hom.app f Y) ((P.map g) x) = (Q.map g) ((PresheafOfModules.Hom.app f X) x)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>P : PresheafOfModules R<GOAL>(PresheafOfModules.toPresheaf R).obj P = P.presheaf
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>P Q : PresheafOfModules R<VAR>f : P ⟶ Q<VAR>X : Cᵒᵖ<GOAL>((PresheafOfModules.toPresheaf R).map f).app X = (PresheafOfModules.Hom.app f X).toAddMonoidHom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>X : Cᵒᵖ<VAR>M : PresheafOfModules R<GOAL>(PresheafOfModules.evaluation R X).obj M = M.obj X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>X : Cᵒᵖ<GOAL>∀ {X_1 Y : PresheafOfModules R} (f : X_1 ⟶ Y), (PresheafOfModules.evaluation R X).map f = PresheafOfModules.Hom.app f X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>X Y : Cᵒᵖ<VAR>f : X ⟶ Y<VAR>M : PresheafOfModules R<VAR>x : ↑(M.obj X)<GOAL>(PresheafOfModules.restrictionApp f M) x = (M.map f) x
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>X Y : Cᵒᵖ<VAR>f : X ⟶ Y<VAR>M : PresheafOfModules R<GOAL>(PresheafOfModules.restriction R f).app M = PresheafOfModules.restrictionApp f M