Model: taterowney/informal_proof_to_informal_statement_premise_selector
Author: taterowney
Pipeline: sentence-similarity
Library: sentence-transformers
Tags: sentence-transformers, safetensors, qwen3, sentence-similarity, feature-extraction, generated_from_trainer, dataset_size:1796, loss:MultipleNegativesRankingLoss, arxiv:1908.10084, arxiv:1705.00652, base_model:Qwen/Qwen3-Embedding-0.6B, base_model:finetune:Qwen/Qwen3-Embedding-0.6B, endpoints_compatible, region:us
Base models (finetune): id: Qwen/Qwen3-Embedding-0.6B
Card metadata: tags: sentence-transformers, sentence-similarity, feature-extraction, generated_from_trainer, dataset_size:1796, loss:MultipleNegativesRankingLoss
base_model: Qwen/Qwen3-Embedding-0.6B
widget: source_sentence: I have the following sketch of a mathematical proof: 

The proof begins by leveraging the fact that affine open sets form a basis for the Zariski topology on a scheme. For a given point \( x \) in scheme \( X \), we first select an affine open neighborhood \( U \) of \( x \), and similarly, for \( f(x) \) in \( Y \), we choose an affine open neighborhood \( V \) that is the image of \( U \) under \( f \).

1. **Obtaining Affine Open Neighborhoods:** We start by finding an affine open set \( U \) in \( X \) that contains \( x \), and an affine open set \( V \) in \( Y \) that contains \( f(x) \) and is the image of \( U \) under \( f \). This utilizes the property that affine opens form a basis for the Zariski topology on schemes.

2. **Rewriting with Isomorphisms:** Using the isomorphisms provided by the properties of affine open sets (`IsAffineOpen.fromSpecStalk`), we rewrite the relevant maps to simplify the expressions. Specifically, we use the fact that the stalk of the structure sheaf at a point can be identified with the ring of germs of regular functions at that point.

3. **Applying Associativity and Composition:** By applying the associativity of the composition of maps (`Spec.map_comp_assoc`), we rearrange the composition to match the desired form. This step directly applies the categorical properties of the `Spec.map` function to ensure that the composition behaves as expected.

4. **Equating the Maps:** Through a series of equalities induced by the properties of the maps involved (`Hom.app_eq_appLE` and `Hom.appLE_map`), we establish that the map induced by \( f \) on the stalk at \( x \) is indeed equal to the composition of the pullback map along \( f \) with the map induced by the affine open neighborhood \( U \).

5. **Final Conclusion:** Finally, by using the specific properties of affine open sets (`IsAffineOpen.Spec_map_appLE_fromSpec`), we conclude the proof, showing the required equality holds.

This step-by-step approach ensures that the abstract categorical constructions are grounded in the concrete properties of schemes and their sheaves, thereby establishing the desired result.

Here is a helpful lemma for this proof: 
sentences: For any element \( x \) of a type \( \alpha \), \( x \) belongs to the universal set of \( \alpha \)., For any given type of elements, a set is defined as a function that assigns a truth value (true or false) to each element, indicating whether the element is a member of the set or not., For any elements \( a_1 \) and \( a_2 \) in a set \( M \) and any scalar \( b \) in a module \( \alpha \), the scalar multiplication is associative in the sense that \( a_1 \cdot (a_2 \cdot b) = (a_1 \cdot a_2) \cdot b \). In other words, multiplying scalars successively in either order yields the same result., source_sentence: I have the following sketch of a mathematical proof: 

Assume \( A \) is a finite free \( R \)-algebra and \( f \in A \).

1. **Forward Direction (\( \Rightarrow \))**:
   - Suppose \( f \) is nilpotent on \( \kappa(\mathfrak{p}) \otimes A \). 
   - Then, in \( \kappa(\mathfrak{p}) \otimes A \), some power \( f^k \) equals zero.
   - Considering the structure of \( A \) as a free \( R \)-module, we can express \( f \) in terms of a basis.
   - The characteristic polynomial of \( f \) over \( R \) has coefficients that, when reduced modulo \( \mathfrak{p} \), must align with the nilpotent property in the tensor product.
   - Specifically, the non-leading coefficients, which correspond to lower-degree terms in the polynomial, must vanish modulo \( \mathfrak{p} \), implying they lie in \( \mathfrak{p} \).

2. **Reverse Direction (\( \Leftarrow \))**:
   - Assume every non-leading coefficient of \( f \)'s characteristic polynomial lies in \( \mathfrak{p} \).
   - Tensoring \( A \) with \( \kappa(\mathfrak{p}) \) effectively reduces these coefficients to zero.
   - The resulting operator \( f \otimes 1 \) in \( \kappa(\mathfrak{p}) \otimes A \) then satisfies a polynomial equation where all non-leading terms have been eliminates.
   - This reduction implies \( f \otimes 1 \) is nilpotent, as its characteristic polynomial becomes \( x^n \) for some \( n \), indicating that \( f^k \) is zero for \( k = n \).

Here is a helpful lemma for this proof: 
sentences: If a function \( f: \mathbb{R} \to \mathbb{R} \) is differentiable on a convex set \( s \) and its derivative satisfies \( |f'(x)| \leq C \) for all \( x \in s \) and some constant \( C \), then for any two points \( x, y \in s \), the following inequality holds:
\[
|f(y) - f(x)| \leq C |y - x|
\]
This implies that \( f \) is Lipschitz continuous on \( s \) with Lipschitz constant \( C \)., We define a function `vectorSpan` that takes a set `s` of vectors in a vector space `V` and returns the span of `s - s`, denoted as `s -_{V} s`, which is the smallest subspace of `V` containing all the vectors in `s - s`., For a ring homomorphism \( f \) and an element \( r \), \( r \) is in the kernel of \( f \) if and only if \( f(r) = 0 \)., source_sentence: I have the following sketch of a mathematical proof: 

We aim to prove that:
\[
(X f) \circ (\mathcal{L} I g) = X (f \circ (\mathcal{L} I g))
\]
**Proof:**

1. **Start with the Left-Hand Side (LHS):**
   \[
   (X f) \circ (\mathcal{L} I g)
   \]
   This represents the composition of two morphisms: \( X f \) and \( \mathcal{L} I g \).

2. **Apply the Definition of Composition for Continuous m-Differential Maps:**
   Using the property `ContMDiffMap.comp_apply`, we can expand the composition:
   \[
   (X f) \circ (\mathcal{L} I g) = X f ( \mathcal{L} I g )
   \]
   
3. **Understand the Pullback Operation:**
   The term \( \mathcal{L} I g \) involves the pullback of \( g \) along \( I \), which relates to how \( g \) is transformed using \( I \). This step assumes properties of the pullback that allow us to manipulate its application within compositions.

4. **Evaluate at a Point:**
   Using the property `L_apply`, we can evaluate the expression at a point:
   \[
   X f ( \mathcal{L} I g ) = X f ( \mathcal{L} I g )
   \]
   This step simplifies the notation, showing that the evaluation at a point holds.

5. **Apply the Sheaf Differential:**
   The sheaf \( X \) is applied to the composition \( f \circ \mathcal{L} I g \). Using the properties `hfdifferential_apply` and `fdifferential_apply`, we can express the differential of \( X \) applied to the composition:
   \[
   X (f \circ \mathcal{L} I g) = (X f) \circ (\mathcal{L} I g)
   \]
   
6. **Conclude Equality:**
   By expanding both sides using the properties of sheaf operations and composition, we arrive at:
   \[
   (X f) \circ (\mathcal{L} I g) = X (f \circ (\mathcal{L} I g))
   \]
   Thus, the composition and the sheaf operation commute as required.

This completes the proof, demonstrating that the composition of \( X f \) with \( \mathcal{L} I g \) is equal to \( X \) applied to the composition of \( f \) with \( \mathcal{L} I g \). The key steps involved understanding the properties of sheaf differentials and continuous m-differential maps, applying evaluation at points, and carefully expanding the expressions to show equality.

Here is a helpful lemma for this proof: 
sentences: For any `C^n`-function `f` from `M''` to `M'` and any `C^n`-function `g` from `M` to `M'`, the composition of `f` and `g` evaluated at any point `x` in `M` is equal to applying `f` to the result of `g(x)`. In other words, `(f ∘ g)(x)` is the same as `f(g(x))`., If a set \( s \) is an element of a non-trivial (non-bottom) filter \( f \) on a set \( \alpha \), then \( s \) is nonempty., If a set \( s \) has a greatest element \( a \), then \( s \) is bounded above, meaning there exists an upper bound for all elements in \( s \)., source_sentence: I have the following sketch of a mathematical proof: 

Assume that γ is an integral curve of the vector field v at the point t₀. By definition of an integral curve, γ satisfies the differential equation γ'(t) = v(γ(t)) in a neighborhood around t₀.

Consider the chart extChartAt evaluated at γ(t₀). The composition of this chart with γ, denoted as extChartAt(γ(t₀))∘γ, represents the trajectory of γ in the coordinate system defined by the chart.

To show that this composition has a derivative, we use the fact that both γ and the chart are differentiable. Since γ is an integral curve, it is differentiable, and the chart is smooth, hence the composition is differentiable.

The derivative of extChartAt(γ(t₀))∘γ at a point t near t₀ involves the derivative of γ at t, which is governed by the vector field v along γ. Specifically, the derivative can be expressed using the tangent coordinate change associated with the vector field v evaluated at γ(t).

Thus, in a neighborhood around t₀, the composition extChartAt(γ(t₀))∘γ is differentiable, and its derivative is precisely the tangent coordinate change along γ involving the vector field v.

Here is a helpful lemma for this proof: 
sentences: An element \( x \) in a ring \( A \) is called integral over a subring \( R \) of \( A \) if there exists a monic polynomial with coefficients in \( R \) such that \( x \) is a root of that polynomial. The function \( \text{IsIntegral}(x) \) checks whether \( x \) satisfies this condition., For any function \( f \) that respects scalar multiplication in a compatible algebraic structure, applying the function after scaling an input yields the same result as scaling the function's output by the same scalar. Formally, if \( c \cdot x \) represents scalar multiplication, then \( f(c \cdot x) = c \cdot f(x) \)., Given a non-unital subalgebra \( s \) of a non-unital algebra \( S \), the function `subtype` maps elements from \( s \) to another non-unital algebra \( A \) in a way that preserves the algebraic structure, specifically the star operation. This means that for every element in \( s \), the mapping ensures that the star operation is maintained appropriately in \( A \)., source_sentence: I have the following sketch of a mathematical proof: 

To prove that α equals β, we will show that the difference α - β is the zero morphism.

First, we note that α - β is a morphism, and we aim to demonstrate that it maps every object to zero. We consider the kernel of α - β, which consists of all elements that α - β sends to zero.

We then observe that the span of the image of the derivation d is contained within the kernel of α - β. This is because, for any element in the image of d, say d(b), we have (α - β)(d(b)) = α(d(b)) - β(d(b)) = 0, by the given condition that α and β agree on all d(b).

By showing that the image of d generates the entire domain (KaehlerDifferential f), we conclude that the kernel of α - β includes all such generated elements. This implies that α - β sends every element to zero, effectively making α - β the zero morphism.

Thus, α must be equal to β.

Here is a helpful lemma for this proof: 
sentences: For any three vectors \( p_1, p_2, p_3 \), the following vector identity holds:
\[
p_3 - p_2 - (p_3 - p_1) = p_1 - p_2
\], For a continuous linear map \( f: M \to M_2 \) between locally convex spaces, the kernel of \( f \) is the entire domain \( M \) if and only if \( f \) is the zero map., A function \( f: M \rightarrow M' \) is said to be continuously differentiable within a set \( s \subseteq M \) at all points \( x \in s \) and for a given differentiability order \( n \in \mathbb{N} \cup \{\infty\} \). The definition requires that for every \( x \) in \( s \), \( f \) satisfies the continuity of its derivatives up to order \( n \) within the set \( s \).
pipeline_tag: sentence-similarity
library_name: sentence-transformers
Likes: 0 | All-time downloads: 1416
Created: 2025-07-20 21:03:59